Consistency in concurrent and distributed systems
This project addresses the issue of formalizing and verifying consistency in concurrent and distributed systems. The project focuses on systems which provide services in a geographically distributed network. Due to communication delays and possible network failures, clients using such services might observe anomalies. In the past decades, a large spectrum of consistency criteria, including Causal Consistency and Eventual Consistency, have been considered for such systems, intended to capture different kind of anomalies that can be observed.
Then, the objectives of this project are:
1. First, the project will aim at defining a uniform and general framework for reasoning about the notions of correctness that are needed for various classes of systems and categories of clients. Indeed, the correctness criteria mentioned above, their properties and the guarantees they ensure, are still not well understood and need deep investigation.
2. Second, verifying automatically that a distributed service satisfies a given criterion. Writing distributed services is known to be very difficult and error prone, and proofs of correctness are usually done on paper, if at all. Automatic verification of correctness criteria for distributed systems such as eventual consistency and causal consistency is a hard problem that still needs to be investigated. Our goal is to develop techniques which can be deployed on distributed implementations to efficiently check their correctness.
Publications
Recent news
Team members
