PhD topic 2023–2024: Verification for modular distributed programming

PhD topic 2023–2024: Verification for modular distributed programming

Keywords

Distributed systems; distributed programming; programming languages and verification

Background

Distributed systems are increasingly widespread and critical. On the positive side, a distributed system features independent modules that execute in parallel, that interact through clear protocols, and that scale elastically to match varying workload. However, programming a distributed system remains error-prone, because of concurrency, failures, and latency, and because its primitives are low level and do not compose well. Furthermore, programming a distributed system remains essentially manual and ad-hoc. Orchestration engines (e.g., Kubernetes) help to choreagraph arbitrary components, but lack high-level abstractions. Programming languages such as Orleans or Flink are single-purpose and restrictive, whereas PlusCal supports high-level reasoning but is not modular.

Our group aims to develop a programming environment that both leverages the strengths of distributed computing (i.e., modularity, protocols, elasticity and flexible deployment), and helps to reason tackle its issues (e.g., correctness of composition, concurrency, failures). Such an environment should enable the developer to reason about components and about the behaviour of their composition, while preserving programmer control over performance and other non-functional properties.

Our Varda framework supports compositional distributed programming. It is designed for building safe distributed systems with good performance, bridging the gap between system builders and the programming language/verification community. A Varda program specifies a system as an architecture of individual components (typically developed outside of Varda). Each component has a well-specified protocol interface and high-level safety constraints. Furthermore, the developer programs the system’s orchestration, i.e., how components are created, destroyed, where they are located, how they interact globally, and what global invariants must be maintained. Varda uses interception as a general-purpose tool for incrementally extending the system, transparently, without modifying its components.

The Varda compiler generates the glue that interconnects and choreographs components in a safe manner. Currently, it performs a limited repertoire of static verifications (e.g., session types), and inserts dynamic assertions for some others (e.g., preconditions and postconditions). Hooks can be used to extend the compiler, e.g., with other kinds of static verification.

Research topic

Varda is under active development. The aim of the proposed PhD is to extend Varda with advanced verification capabilities and to advance the state of the art in verification of distributed programs . This should not come at the expense of performance and of the ability to control important non-functional properties, such as fine-grain placement and elasticity.

The following directions are considered particularly in demand of verification support:

  • Using the Varda compiler hooks to extract a formal model that can be fed to TLA+ or Coq, in order to ensure dependability of the system.
  • Reasoning over shared state, thanks to rely-guarantee or separation logics.
  • Add security statements to the Varda language, and the corresponding static and dynamic checks; harden the Varda implementation to isolate malicious components.

The research has both a fundamental and an applied aspect, and aims for practical results. The applicant shall be expected, both to study the necessary theory, and to implement and evaluate a practical programming environment complete with compelling use cases.

Requirements and application

The PhD research will be advised by Ahmed Bouajjani, of IRIF and Marc Shapiro, of Sorbonne-Université and Inria. It will take place in Paris, France. Speaking French is not required.

Candidates should hold a Masters in Computer Science/Informatics or a related field. They should have an excellent academic record and should be knowledgeable and motivated in distributed systems, distributed databases, and/or verification tools. In addition, any prior industrial or research experience, development and experimental skills, and teamwork and communication skills will be considered.

Please contact the advisors Marc Shapiro <marc.shapiro@acm.org> and Ahmed Bouajjani <abou@irif.fr>, with the following information:

  • A resume or Curriculum Vitæ.
  • A motivation letter.
  • A list of courses and grades of the last two years of study (an informal transcript is OK).
  • Names and contact details of three references (people who can recommend you), whom we will contact directly.

Also, let us know if you have publications and/or open-source developments.

Comments are closed.