Computer Science

DANIELE GORLA
DANIELE GORLA

General goals:
Understanding the basic concepts of concurrent systems and the methodologies used for solving the problems they yield

Specific goals:
Mutual exclusion, different liveness properties, semaphores, monitors, transactions, mutex-free concurrency, other liveness properties, universal object and consensus. Labelled transitions systems, interleaving semantics, synchronization, simulation and bisimulation, verification techniques, name passing, type systems.

Knowledge and comprehension:
Understanding the basic issues of concurrent systems and their possible solutions, the foundational principles of a concurrent programming language and the possible verification techniques.

Applying knowledge and comprehension:
ability of solving basic problems of simple concurrent systems

Capabilities of critiquing and assessing:
understanding advantages and disadvantages of the different possible solutions of problems in concurrent systems

Communication skills:
developing a technical and formal language, able to explain the proposed solutions and their relative merits

Learning skills:
ability in understanding complex programming scenarios and the relative solutions, even complex

Learn the basic concepts of concurrency, like synchronization, mutex, lock/unlock, semaphores, monitors, STM, consensus, failure detectors. Use of automata as descriptors of non-deterministic behaviours. Notions of equivalences and mechanisms for checking them.

Basic notions of algorithms, complexity, programming, automata, logics

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/

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.

Lessons in class

Attendance is strongly suggested

Mid-term exams during the classes or final oral exam

Exercises with and without solutions in class