Author: lmvadm

[June 2024] The four-year For-CoaLa project is funded by ANR

Coordinator: Hélène Coulon, IMT Atlantique
Partners: IMT Atlantique (Stack Inria Team), Université d’Orléans (LIFO, LMV Team)

Large distributed software systems (applications or infrastructures) are now ubiquitous, with component-based systems (e.g., service-oriented architectures or microservices) offering a convenient way to structure large systems, in particular distributed systems deployed in the Cloud, in the core, or at the edge of the network. DevOps operations, that include system configurations and reconfigurations, are required to handle various kinds of scenarios such as fault tolerance, scalability, software updates, or various optimizations, etc. Such changes may lead to faults. A study of 597 unplanned outages that affected popular cloud services between 2009 and 2015 found that 16% of them were caused by a system upgrade.

On the one hand, many configuration tools and languages exist in the DevOps community, some of them being specific to the provisioning of resources in Cloud providers, packaging problems, containerized deployments, configuration of applications or infrastructures, etc. The main advantage of these tools is their full integration and adoption in the DevOps community. Their disadvantage is they lack both formal and textual specifications. Moreover, their contours are blurred. On the other hand, many initiatives have been studied in academia to contribute to the deployment, configuration, and reconfiguration of distributed software, bringing improvements such as expressivity, speed, safety, etc. Many come with precise and sometimes formal definitions. However, they lack the breadth of the mainstream DevOps tools.

The goal of For-CoaLa is twofold: (1) understand and bridge the gap between a popular tool from the DevOps community (Ansible) and a tool from academia (Concerto); (2) improve the understanding of these languages based on mechanized formal semantics and develop verified semantic-preserving cross-language transformations.

[March 2024] Armaël Gueneau’s talk

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël Gueneau (INRIA Saclay)
SR1, March 18, 2024, 14:00
In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this talk, I will present our first steps towards the goal of developing program logics for multi-language verification. Specifically, I will present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.