CobbleDB: Modelling Levelled Storage by Composition
This work addresses database storage correctness for developers, but it is incremental as it builds on prior specifications and implementations.
The authors tackled the problem of building correct-by-construction database backing stores by deriving a Java implementation from proven specifications, resulting in CobbleDB, a reimplementation of RocksDB's levelled storage that demonstrates practical value.
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.