Dirección de investigación : Marc SHAPIRO

Leveraging formal specification to implement a database backend

onceptually, a database storage backend is just a map of keys to values. However, to provide performance and reliability, a modern store is a complex, concurrent software system, opening many opportunities for bugs.
This thesis reports on our journey from formal specification of a store to its implementation. The specification is terse and unambiguous, and helps reason about correctness. Read as pseudocode, the specification provides a rigorous grounding for implementation.
The specification describes a store as a simple transactional shared memory, with two (behaviourally equivalent) variants, map- and journal-based.We implement these two basic variants verbatim in Java. We specify the features of a modern store, such as a write-ahead log with checkpointing and truncation, as a dynamic composition of instances of the two basic variants.
Our experimental evaluation of an implementation has acceptable performance, while our rigorous methodology increases confidence in its correctness.

Publicaciones 2020-2024