CobbleDB: Modelling Levelled Storage by Composition
We present a composition-based approach to building correct-by-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.
Authors
- E. Ma (ORCID: https://orcid.org/0009-0005-3322-0805)
- Annette Bieniusa (ORCID: https://orcid.org/0000-0002-1654-6118)
- Ayush Pandey (ORCID: https://orcid.org/0000-0001-8011-5411)
- Marc Shapiro
Institutions
- Télécom Paris (FR)
- Institut national de recherche en sciences et technologies du numérique (FR)
- University of British Columbia (CA)
- University of Kaiserslautern (DE)
- University of Koblenz and Landau (DE)
- Sorbonne Université (FR)
- Institut Polytechnique de Paris (FR)
- Télécom SudParis (FR)
Publication Details
- Published
- 2026-04-23
- DOI
- https://doi.org/10.1145/3806077.3806696
- Primary Topic
- Advanced Data Storage Technologies
- Type
- article
- Field-Weighted Citation Impact
- 0.00