Languages for Concurrency and Distribution

Master's Degree In Computer Science - University of Padua
A.Y. 2021/2022

Aim

The widespread diffusion of concurrent, distributed and mobile systems makes the classical programming and specification paradigms inadequate and opens up complex and fascinating challenges. A rethinking appears necessary, starting from the foundations and adopting a rigorous, formal and disciplined approach. The aim of the course is to introduce the student to themes of interest in the area, using as tools type systems, process calculi and modelling languages in general. Starting from topics which are by now classical (like the Calculus of Communicating Systems and pi-calculus that center the study around some basic concepts like processes, composition and communication mechanisms), we will reach some advanced issues of the research in the area. Some languages that implement the theoretical developments discussed are presented, including advanced languages for concurrency and distribution like Google Go, Erlang, Elixir, Clojure, Jolie, Rust, along with the corresponding programming techniques.

Program

The structure and themes of the course will be as follows:
  1. The "Calculus of Communicating Systems" (CCS), a core language for the description of concurrent systems. Process equivalence: transition systems and bisimulation.
  2. Hennessy-Milner logic and tools for verification. Mutual exclusion, deadlock, fairness. Safety and liveness properties. Systems with dynamic topology and mobility: pi-calculus. Verification tools (Concurrency Workbench, Caal, PseuCo).
  3. From specification languaes to programming langauges: Google Go, Erlang, Elixir, Clojure, Rust, Jolie, ORC.

Schedule

This is a course unit of the Master's Degree In Computer Science, University of Padua, and it is held in the 2nd semester for the A.Y. 2021/2022, with a schedule to be defined.

Exam

The exam consists of two parts: exercises and a deepening/project (see below), to be prepared off-line and then presented in an oral discussion/seminar.

  1. EXERCISES
    You should do two exercises in the section Exercises in the following page
  2. DEEPENING/PROJECT
    You can choose among various possibilities including (1) a mini-project consisting in the specification / implementation / verification of a system and its formal properties (2) the study of advanced verification tools (3) study of research papers about formal models, verification techniques, programming languages related to the themes of the course. Again, some ideas can be found at the following the page.
in both cases, the list of suggestions is not exhaustive. The student can propose different project ideas that better fit her/his personal interests (including different exercises, for example chosen from the book). In any case, the choice must be discussed with the instructor, approved and defined in the details (the description is often sketchy).

Material

The course has a Moodle where additional material can be found. For the foundational part we will use the following book

The material concerning the part on programming languages will be distributed via the moodle.

Useful links

Some advanced tools