Search papers, labs, and topics across Lattice.
This paper presents a composition-based approach to building database backing stores with correctness guarantees. They leverage formally verified store equivalences to compose performance features, enabling the construction of complex systems from simpler, verified components. The authors demonstrate the approach by reimplementing RocksDB's levelled storage in Java, resulting in CobbleDB.
Formally verified composition lets you build complex, high-performance databases like RocksDB from simpler, provably correct components.
We present a composition-based approach to building correctby-construction database backing stores. In previous work, we specified the behaviour of several store variants and proved their correctness and equivalence. Here, we derive a Java implementation: the simplicity of the specification makes manual construction straightforward. We leverage spec-guaranteed store equivalence to compose performance features, then demonstrate practical value with CobbleDB, a reimplementation of RocksDB's levelled storage.
