Concurrent Systems

Teacher: Prof. Daniele Gorla

Schedule of classes: Every monday from 8(.15)am to 11am

      Every tuesday from 8(.15)am to 10am

Where: Aula T1, building E (Viale Regina Elena 295)

When: From Feb. 26th to May 28th, 2024

The class is focused on the foundational aspects and on the formal/mathematical semantics of concurrent systems. The class is structured in two main parts. The first part describes the main characteristics and the basilar problems of every concurrent system (mutual exclusion, synchronization, atomicity, deadlock/livelock/starvation, ...) and the relative solutions at the implementation level (semaphores, monitors, system primitives, ...). Furthermore, more evolute notions are shown, like: failure detectors, their implementation and their use to obtain wait-free implementations; universal object, consensus object and consensus number; transactional memory, ... The second part of the course describes the preliminary notions of a minimal concurrent language called CCS (execution of parallel processes through labelled transition systems, interleaving semantics, syntonization, non-determinism, process simulability) and presents a mathematical model, with different features for the specification and the analysis of systems written in such a language. 

In the time left, we shall have lectures in the form of seminars where more advanced programming mechanisms (like name creation and exchange, type systems for the verification of properties, cryptography, distribution, truly concurrent semantics) will be presented. 

The course integrates didactic parts to recent research problems.

The course is split into 3 parts: 

• The first part studies foundational problems of concurrent systems: 

  • sequential vs concurrent programs

  • Process synchronization (competition vs cooperation)

  • Safety and liveness properties; a hierarchy of liveness properties (deadlock freedom, starvation freedom, bounded bypass)

  • Mutual exclusion: atomic registers (algorithms by Peterson and Lamport; how to obtain a starvation free lock object from a deadlock free lock object), with specialized hardware primitives (test&set, compare&swap, fetch&add) and with non-atomic registers (Bakery algorithm).

  • Semaphores, monitors and their use for solving classical problems (producers-consumers, readers-writers, rendezvous, dining philosophers)

  • Software Transactional memory

  • Atomicity and its properties

  • mutex-free concurrency: liveness revisited (obstruction freedom, non-blocking and wait-freedom); mutex-free implementation of an unbounded stack; failure detectors Omega_X and Diamond_P, and the associated construction of non-blocking and wait-free implementations from an obstruction free implementation; hints on how to implement the Omega failure detector.

  • Universal object; consensus object and its universality; primitives hierarchy based on the consensus number.

• The second part is focused on CCS (Calculus of Communicating Systems [Milner:1980]): 

  • non-determinism

  • Labeled transition systems

  • recursion

  • parallel composition (interleaving semantics)

  • synchronization

  • restriction

  • bisimulation: strong vs weak, axiomatization, logical characterization, algorithmic verification.

• The third part will present possible enhancements of the previous material (every lecture will be on a different topic). By following the students' interests, some of the following topics can be presented: 

  • communication: name creation and passage

  • polyadic communication (type system for correct communications and encodability in the base calculus)

  • asynchronous communication and encodability of synchrony

  • higher-order communication and its encodability in the base calculus

  • encoding of the lambda-calcolus

  • a model for object-oriented languages

  • concurrent calculi with cryptography or distribution

  • truly concurrent semantics

First part: 

• M. Raynal: Concurrent Programming: Algorithms, Principles and Foundations. Springer, 2013. (chapters 1, 2, 3, 4, 5, 10, 14, 16 and part of 17).

Second part: 

• R. Milner. Communicating and Mobile Systems. Cambridge University Press, 1999. (chapters: 1, 2 (no 2.3), 3, 4 (no 4.1, 4.4, 4.5 and 4.6), 5 (no prop. 5.2, ex 5.3, lemma 5.4/5.5, theor. 5.6, def. 5.17, prop. 5.18, prop. 5.23), 6 (no 6.3) and 7 (only 7.2 and 7.3).

• R. Cleaveland and S. Smolka. Process Algebra. In Encyclopedia of Electrical Engineering, John Wiley & Sons, 1999. Available at http://www.cs.umd.edu/~rance/publications/papers/ee99.ps.gz. (sect. 3.2, 4.1 and 4.2).

• R. Cleaveland and O. Sokolsky.  Equivalence and Preorder Checking for Finite-State Systems. In "Handbook of Process Algebra," pp. 391-424, Elsevier, 2001. Available at  http://www.cis.upenn.edu/~sokolsky/PAhandbook.pdf. (sect. 3.1).

Third part: 

• J. Parrow. An Introduction to the pi-Calculus. In Handbook of Process Algebra, pages 479-543. Elsevier, 2001. Available at http://user.it.uu.se/~joachim/intro.ps

• R. Milner. The Polyadic pi-Calculus: A Tutorial. In Logic and Algebra of Specification. Springer-Verlag, 1993. Available at http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps

• D. Sangiorgi, D. Walker. The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, 2001. The reference book on the pi-calculus; maybe, quite difficult for a master student.

There are two possible ways to pass the exam:

• First modality (better suited for students who regularly attend the classes): 2 classworks. 

• Second modality: written and oral exam on all the topics presented during the classes.

In Sapienza's Moodle platform, you can find all the slides of the course, a lot of material, and a forum for discussing the topics of the classes (where you can post questions, ask for explanations, interact between you, and interact with me). I suggest you to register (with your studenti.uniroma1.it account) at https://elearning.uniroma1.it (look for «Concurrent Systems»). The pwd has been communicated in the first class of the course, or you can ask it to me by email. You're NOT authorized to distribute the material downloaded nor the credentials to access the site.