Computer Science - Informatica

DANIELE GORLA

Obiettivi generali:
Capire i concetti base dei sistemi concorrenti e le metodologie adottate nella soluzione dei problemi da essi posti

Obiettivi specifici:
Mutua esclusione, diverse proprietà di liveness, semafori, monitor, transazioni, atomicità, concorrenza senza mutua esclusione, altre proprietà di liveness, oggetto universale e consenso. Sistemi di transizioni etichettate, semantica a interleaving, sincronizzazione, simulazione e bisimulazione, tecniche di verifica, passaggio di nomi, sistemi di tipo.

Conoscenza e comprensione:
Capire the problematiche di base dei sistemi concorrenti e le relative soluzioni possibili, i principi fondazionali dei linguaggi di programmazione concorrente e le relative tecniche di verifica

Applicare conoscenza e comprensione:
essere in grado di risolvere problematiche basilari di semplici sistemi concorrenti

Capacità critiche e di giudizio:
capire vantaggi e svantaggi delle varie possibili soluzioni a problematiche di sistemi concorrenti

Capacità comunicative:
sviluppare un linguaggio tecnico e formale in grado di spiegare le soluzioni ideate e i relativi meriti

Capacità di apprendimento:
comprendere scenari di programmazione complessi e le relative soluzioni, anche sofisticate

Comprendere i concetti base della concorrenza, quali sincronizzazione, mutex, lock/unlock, semafori, monitor, STM, consensus, failure detectors. Utilizzo di automi come descrittori di comportamenti non-deterministici. Nozioni di equivalenze e meccanismi per la loro verifica.

Conoscenze di base di algoritmi, complessità, programmazione, automi, logica

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.

Lezioni in aula

Frequenza fortemente consigliata

Esoneri nel corso delle lezioni o esame orale finale

Esercizi svolti e da svolgere in classe