Master Internship: Data intensive management systems concurrency control mechanization
General Context

Current data management applications and systems involve increasingly massive data volumes. Surprisingly, while the amount of data stored and managed by data engines has drastically increased, little attention has been devoted to ensure that those are reliable. Obtaining strong guarantees requires the use of formal methods and mature tools. A very promising approach consists in using proof assistants such as Coq [1,2]. Our purpose is to prove that existing systems conform to their specifications and to verify that programs that make intensive use of database queries and transactions are correct. This internship leads to a PhD if the candidate demonstrates the expected skills.

Research program

Concurency control is one of cornerstone of database systems as it is at the heart of transaction processing management. Many different concurency models and protocols have been proposed over the last decades. None of them have been formally specified nor been proven correct. Building on the work in [3] and based on the specification given in [4], the candidate will formalize in Coq different concurrency models (semantics and properties) and verify the corresponding algorithms and/protocols.

Bibliography
  1. Xavier Leroy. A formally verified compiler back-end. J. Autom. Reasoning, 43(4):363--446, 2009.
  2. Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Toward a verified relational database management system. In ACM International Conference on Principles of Programming Languages (POPL), 2010.
  3. V. Benzaken, E. Contejean, S. Dumbrava, A Coq Formalization of the Relational Data Model, European Symposium on Programming - ETAPS, (ESOP), 2014.
  4. Ph. Bernstein, V. Hadzilacos, N. Goodman, Concurrency Control and Recovery in Database Systems available here
Prerequisite

The candidate should have a very strong background in theoretical computer science with emphasis in logic as well as a concrete practical experience of functional programming in OCaml-like programming languages. A very good knowledge of Coq is mandatory.