Course program
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)
- 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
WEBPAGE OF THE COURSE: https://sites.google.com/uniroma1.it/conc-sys/
Prerequisites
Basic notions of algorithms, complexity, programming, automata, logics
Books
M. Raynal: Concurrent Programming: Algorithms, Principles and Foundations. Springer, 2013.
R. Milner. Communicating and Mobile Systems. Cambridge University Press, 1999.
R. Cleaveland and S. Smolka. Process Algebra. In Encyclopedia of Electrical Engineering, John Wiley & Sons, 1999.
R. Cleaveland and O. Sokolsky. Equivalence and Preorder Checking for Finite-State Systems.
J. Parrow. An Introduction to the pi-Calculus. In Handbook of Process Algebra, pages 479-543. Elsevier, 2001.
R. Milner. The Polyadic pi-Calculus: A Tutorial. In Logic and Algebra of Specification. Springer-Verlag, 1993.
Frequency
Attendance is strongly suggested
Exam mode
Mid-term exams during the classes or final oral exam
Lesson mode
Lessons in class
