Post-doc 2023–2024: A programming and verification environment for distributed computing
Distributed systems; distributed programming; programming languages and verification; composition; system architecture
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.
Varda is under active development and opens several research opportunities, both to ensure Varda is a useful tool for developing practical, efficient systems, and to help developers reason at a high level about the behaviour and correctness of their system. Some possible directions follow.
- Dependability – Explore how to improve the dependability of distributed system using Varda by adding information flow checking, enriching the type system or extracting a formal model (e.g. in TLA+ or Coq) to do verification.
- System – Integrate Varda with a popular orchestration engine (e.g., Kubernetes), encoding Varda abstractions into the corresponding Kubernetes entities, and, vice-versa, exposing relevant Kubernetes abstractions as first-class values in Varda; add the capability to program the deployment and elasticity of components.
- Expressiveness – Add the capability to implement, to manage and to access shared objects, e.g., via replication and persistence; add support for transactions; enable system developers to ensure specific consistency guarantees.
- Security – integrate security consideration inside Varda architecture description and harden the Varda implementation to contain 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
Candidates to this position should hold a PhD in Computer Science/Informatics or a related field. They should have an excellent academic record and experience in distributed systems, distributed databases, and/or verification tools. In addition to research experience, he or she should be a good developer and experimenter at large scale, and have teamwork and communication skills. Industrial experience is a plus.
- 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).
- A list of your top publications and/or open-source developments.
- Names and contact details of three references (people who can recommend you), whom we will contact directly.