Languages for Concurrency and Distribution

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.

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 languages to programming languages: Google Go, Erlang, Elixir, Clojure, Rust, Jolie, ORC.

This is a course unit of the Master's Degree in Computer Science, University of Padua, held in the 2nd semester for the A.Y. 2025/2026, with the following schedule. Adjustments are possible if there are common requests by the participants.

• Monday, 12:30 - 14:00, room 1BC/50
• Tuesday, 12:30 - 14:00, room 1BC/50

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

1. Exercises
   You should do two exercises from the Exercises section of the exam 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 on the exam page.

In both cases, the list of suggestions is not exhaustive. The student can propose different project ideas that better fit their personal interests (including different exercises, for example chosen from the book). In any case, the student's choices need to be discussed with the instructor, approved and defined in the details (the descriptions above are often sketchy).

During the exam, which will last indicatively one hour, the student will solve the exercises (typically, using the blackboard) and present the deepening/project part (for this part, a slide-based presentation is typically useful).

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

L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba — Reactive Systems
Cambridge University Press, 2007 (Chap. 1-7, except 6.4)

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

• Caal — a web version of the concurrency workbench. This works on the most common browsers.
• PseuCo — an interactive tool for defining and simulating processes written in a concurrent language (a sort of simplified Go language), which has an immediate translation into CCS.
• Edinburgh Concurrency Workbench — an interactive tool for the definition, simulation and verification of properties of CCS processes (and of various CCS extensions).
  • Linux binaries are available (unfortunately 32-bit)
  • Can be compiled using SML New Jersey (tested with Version 110.99.8; 64-bit). For convenience, the sources with a build file are available here.
  • It can be used in emacs (suggested), following the instructions here.
  • Syntax highlighting for cwb (based on the package generic-x): cwb-highlight.el
• Bisimulation game and CCS simulator — allows one to visualise and simulate the behaviour of a process, given its transition graph as produced by the Concurrency Workbench, and to play with behavioural equivalences.
• Concurrency Workbench of the New Century — offers functionalities similar to the Edinburgh Concurrency Workbench. It supports various languages like CCS, CCS with priorities, timed CCS, CSP, Basic Lotos.
• SLMC (spatial logic model checker) — a tool for the verification of spatial properties of concurrent processes.

Some advanced tools

• mCRL2 (micro Common Representation Language 2)
• PRISM (probabilistic model checker)
• CADP (Construction and Analysis of Distributed Processes)
• PAT (Process Analysis Toolkit — an enhanced simulator, model checker and refinement checker for concurrent and real-time systems)
• UPPAAL, an integrated tool environment for modeling, validation and verification of real-time systems