Rigorous development of database backends

Using a verification-based approach for database storage backends has the potential to avoid such bugs, but specifying the complexity of a modern backend upfront is a daunting task. To decompose the problem into smaller pieces, we base our approach on the following insights: (1) There are two broad classes of backends: eager, state-based maps, vs. lazy, operation-based journals. (2) We can write a high-level, abstract specification that accounts for both. (3) We can prove correctness and equivalence properties from the high-level specification. (4) The specification provides a kind of pseudocode for the implementation. (5) A similar high-level specification accounts for the composition of primitive stores. (6) We can express the complex internal architecture of a modern backend as such a composition.

An initial goal of the internship is to perform an experimental study (of performance and fault tolerance) of the implementation. The focus of the work will tackle items 5 and 6. The intern will design and implement a composition framework, and will use composition to mimic the functionality of an modern backend such as RocksDB. The research objective is to evaluate the backend designed following our rigorous approach, against comparable backends designed in an ad-hoc manner.

Faculty Supervisor:

Ivan Beschastnikh

Student:

Partner:

Université Paris Cité;Sorbonne Université

Discipline:

Computer science

Sector:

Information and Communications Technology

University:

The University of British Columbia

Program: