Varda : un langage pour la programmation de systèmes distribués par composition
Laurent Prosperi · theses.fr (ABES) · 2023
Large distributed systems are often built by assembling off-the-shelf (OTS) components, e.g., components, services, processes, etc., developed independently. The current approach is to interconnect their APIs manually. This is ad hoc, complex, tedious, and error-prone. Programming languages offer a promising approach to addressing this problem. First, they could help reduce the occurrence of bugs. The programmer specifies the system using well-defined entities and constraints. Then, the compiler a correct-by-construction implementation providing various guarantees (e.g., that communications are correctly ordered). Furthermore, languages could help improve programmers’ productivity. The code generation offloads the boilerplate plumbing to the compiler. In addition, the compiler might perform optimizations leveraging its knowledge of the system. In this thesis, we propose a new language, Varda, at the intersection between programming and specification languages. A Varda program describes how to compose components into a coherent architecture. To ensure safety, the programmer isolates an OTS component behind a Varda shield. The shield restricts the component’s behaviour by specifying its interface, its protocol (i.e., what it may send or receive, and in what order), and pre- and post-conditions. Components can be logically nested, to provide encapsulation. An outer component orchestrates its inner components, spawning or killing component instances, interconnecting them, and supervising error conditions; it can intercept and manipulate communication, and more generally compute over components and messages. Varda provides strong guarantees (e.g., isolation between components), enforcing the specification by static analysis, by run-time checks, and by sandboxing. At the same time, to be useful for the development of real, practical distributed systems, Varda takes a pragmatic approach. A shield can contain non-Varda adaptor code (e.g., Java) in order to incorporate black-box OTS components. Varda provides control over non-functional properties that are relevant for performance and fault tolerance, for instance elasticity, placement, and inlining. The Varda compiler automates the generation of boilerplate glue code to make components work together. Varda supports non-stop execution, thanks to supervision mechanisms. We demonstrate the expressiveness and the ergonomic of Varda by encoding classical distributed patterns (e.g., sharding and access control). To illustrate how Varda helps build a real distributed system, we implement a clone of the AntidoteDB geo-replicated datastore. Varda applications are compact, and exhibit modular and reusable design. Our experiments show that the run-time overhead is modest, thanks to compile-time verification andoptimizations.