Developing correct, efficient and available distributed systems is a major challenge. In practice, strong consistency often has to be sacrificed, which makes the task of programmers extremely hard. A central problem is to determine an adequate level of consistency for a given application: a level that requires as little synchronization as possible, but is strong enough to ensure the correctness of the application behavior. The goal of this project is to provide a principled and automated approach for the co-design of an application with its adequate consistency model. Our approach combines programming languages techniques, formal program verification and synthesis, and distributed protocol design. More specifically we propose to develop methods for program verification and synthesis under relaxed consistency, exploit these methods to provide language support for the design of programs that are both correct and efficient (having good availability and performance properties), and demonstrate the applicability of our framework by developing practical systems (a 5G+ management infrastructure and an IoT application).
Monsieur Ahmed Bouajjani (Institut de Recherche en Informatique Fondamentale)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
ARM / ARM
IRIF Institut de Recherche en Informatique Fondamentale
LIP6 Laboratoire d'informatique de Paris 6
ORANGE / TGI/OLN/CNC
Help of the ANR 523,422 euros
Beginning and duration of the scientific project: September 2019 - 48 Months