Séminaire Recherche d'Octobre

Abstract:

Cloud applications provide increasingly complex services on a global scale. To achieve the quality of service demanded by users, a common technique is to maintain copies of the application’s shared data across geographically dispersed locations closer to end users. To this end, it has become increasingly popular to develop applications that rely on weak consistency models where operations requested by a client are executed locally without any coordination with other replicas and immediately returned to the client. 

These operations are later propagated in the background, leading to different replicas’ execution orders and, potentially, divergent replica states. Replicated Data Types (RDTs) that resemble sequential data types (e.g. sets, maps) guarantee convergence by design by providing efficient and deterministic data reconciliation solutions. However, designing new RDTs is challenging. In fact, even experienced researchers may miss subtle corner cases when designing RDTs for simple data structures. In this talk, I will give an overview of techniques for checking the correctness of RDTs and deriving correct-by-construction RDTs.

Short bio:

Carla Ferreira received a PhD from the University of Southampton (2003). She is a Full Professor at NOVA University Lisbon and a researcher at the NOVA LINCS research centre in Portugal. She currently coordinates TaRDIS - a Horizon Europe project on programming tools for decentralised swarms. Her research is concerned with developing formal calculi, techniques, and tools to express and reason about concurrent and distributed systems, with the overall goal of helping programmers build trustworthy systems. She has published in top-tier venues, including POPL, VLDB, EuroSys, OOPSLA, ESOP, MODELS, and CONCUR.