CONCURRENT SYSTEMS

Obiettivi formativi

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

Canale 1
DANIELE GORLA Scheda docente

Programmi - Frequenza - Esami

Programma
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/
Prerequisiti
Conoscenze di base di algoritmi, complessità, programmazione, automi, logica
Testi di riferimento
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.
Frequenza
Frequenza fortemente consigliata
Modalità di esame
Esoneri nel corso delle lezioni o esame orale finale
Modalità di erogazione
Lezioni in aula
  • Codice insegnamento1047619
  • Anno accademico2024/2025
  • CorsoComputer Science - Informatica
  • CurriculumCurriculum unico
  • Anno1º anno
  • Semestre2º semestre
  • SSDINF/01
  • CFU6
  • Ambito disciplinareAttività formative affini o integrative