Title: Modelling and Verifying a Database Backend
Abstract:
Although key-value storage conceptually just writes and reads data in a shared memory, modern stores have high internal complexity for performance and fault tolerance. Several are based on unfamiliar data types, supporting incremental and/or concurrent updates (e.g., CRDTs). This paper studies a correct-by-design approach based on formal specifications. An execution is abstracted as a trace, a partial order of transactional events, whose valuation specifies the expected value of a key at each event. We show that both eager, random-access maps and lazy, sequential-access journals conform to the valuation. We prove that the transaction semantics is equivalent to the trace semantics. Our safety results extend naturally to systems with stronger guarantees.