Concurrent Systems (prof. Gorla)  AA 20212022
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 waitfree 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, nondeterminism, 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.
Timetable2nd semester (end of February > end of May).
Text booksFirst part:
Second part:
Third part:
Detailed ProgramThe course is split into 3 parts:
DiaryHere, [R] denotes Raynal's book; [CCS] and [PI] denote teacher's lecture notes on CCS and picalculus (that are a unified and coherent presentation of the texts for the second and the third part of the course listed above).
Feb 23rd, 2022 ([R]: chapt.1, excluding sect.1.2.5; 2.1.1, 2.1.2, 2.1.3. Lecture Notes): Sequential vs Multiprocess Program; process synchronization (competition and cooperation); the mutual exclusion problem; safety and liveness properties; a hierarchy of liveness properties (bounded bypass; starvation freedom; deadlock freedom). Atomic read/write registers; mutex for 2 processes (Peterson algorithm). Feb 25th, 2022 ([R]: 2.1.4; 2.1.5  only the idea, no algo, no proofs; 2.1.6; 2.1.7. Lecture Notes): Generalizing Peterson's algorithm to n processes. Algorithms with better performances when no concurrency is present: with a tournament tree of 2processes competitions (O(log n)); Lamport's fast mutex algorithm (with constant time when there is no contention). March 2nd, 2022 ([R]: 2.2 and 5.2.3; 2.3.1, 2.3.2. Lecture Notes  Lecture Notes): From Deadlock freedom to Starvation freedom using atomic r/wregisters; mutex with specialized HW primitives (test&set; swap; compare&set; fetch&add); the ABA problem with the compare&set. Safe registers: Lamport's Bakery algorithm March 4th, 2022 ([R]: 2.3.3. Lecture Notes): Aravind's bounded algorithm. March 9th, 2022 ([R]: 3.1, 3.2.1, 3.2.2, 3.2.4. Lecture Notes): Concurrent objects. Semaphores and their implementation. Use of semaphores in the producer/consumer problem (both for single producer/consumer and for multiple ones) and in the readers/writers problem (both with weak/strong priority to the readers and with weak priority to the writers). March 11th, 2022 ([R]: 3.3.1, 3.3.2, 3.3.4, 3.3.5. Lecture Notes1, Lecture Notes2): Monitors: concept and implementation through semaphores; implementing rendezvous through monitors. Readers/writers through monitors. The problem of the "Dining Philosophers": solutions that break symmetry (through semaphores) and a symmetric solution (through monitors). March 16th, 2022 : First classwork. March 18th, 2022 ([R]: chap. 4. Lecture Notes): Atomicity: formal definition and compositionality; possible variants and their noncomposability. March 23rd, 2022 ([R]: 10.1, 10.2, 10.3, 10.5. Lecture Notes): Software Transactional Memory. Opacity and a Logical clockbased STM system (TL2). Virtual World Consistency and a vector clockbased STM system (REMARK: to better understand the difference between virtual world consistency and opacity, look at this paper: https://www.sciencedirect.com/science/article/pii/S0304397512004021/pdf?md5=78dd63551d097b6a3212285669d20ff8&pid=1s2.0S0304397512004021main.pdf, sections 2.6 and 3.2). March 25th, 2021 ([R]: 5.1, 5.2.1, 5.2.2, 5.2.5, 5.2.6. Lecture Notes): Mutexfree concurrency: problems of mutex and notion of mutexfreedom, progress conditions. Examples: splitter, timestamp generator and stack (based on swap plus fetch&add; based on compare&set); progress conditions for these examples. March 30th, 2022 ([R]: 5.3.1, 5.3.2, 5.3.3, 5.3.4; 17.7, 17.7.1, 17.7.2  only the idea, not the formal protocol. Lecture Notes): From obstructionfreedom to nonblocking through failure detector Omega_X; hints on the implementation of Omega_X. From obstructionfreedom to waitfreedom through failure detector Diamond_P; hints on the implementation of Diamond_P.
April 1st, 2022 ([R]: 14.1, 14.2, 14.3, 14.5. Lecture Notes): Universal object and consensus object; universality of consensus (unbounded waitfree construction). April 6th, 2021 ([R]: 16.1, 16.2, 16.3, 16.4.1, 16.4.3, 16.4.4, 16.4.5  adapted to test&set  16.5.1, 16.6. Lecture Notes): Binary vs multivalued consensus. Consensus number (for atomic R/W registers, test&set, swap, fetch&add, compare&swap) and consensus hierarchy. April 8th, 2022 ([CCS]: chapters 1 and 2. Lecture Notes): Automata for describing process behaviors (notion of LTS); inadequacy of trace equivalence for equating nondeterministic processes; simulation, double simulation and bisimulation. Properties of bisimilarity. April 13th, 2022 : Second classwork. April 20th, 2022 ([CCS]: chapters 1 and 2.Lecture Notes and Lecture Notes): Syntax for nondeterministic processes: from LTS to the syntax and vice versa. Examples: counter and queue. Process interaction, parallel composition and name restriction. April 22nd, 2022 ([CCS]: chapter 3.1, 3.2, 3.3. Lecture Notes): A first proof technique for proving properties of LTSs: the case of imagefiniteness. A second proof technique for proving properties of LTSs: the case of closure under substitutions. A simple example that uses bisimilarity for proving an implementation equivalent to its specification. April 27th, 2022([CCS]: 3.4, 4.1, 4.2. Lecture Notes): Congruence of Bisimilarity. Weak bisimilarity: basic properties, comparison with strong bisimilarity and fundamental laws. April 29th, 2022([CCS]: 4.3. Lecture Notes): Examples using weak bisimilarity: the factory, the lottery and the scheduler. May 4th, 2022: Third classwork. May 6th, 2022 ([CCS]: 5.1. Lecture Notes): An inference system for strong bisimilarity: soundness and completeness for finite processes. The tau laws for weak bisimilarity. Verifying the equivalence of a specification and an implementation through the inference system. May 11th, 2022 ([CCS]: 5.3. Lecture Notes): The Kennelakis and Smolka Algorithm for bisimulation on finite state LTSs; soundness and complexity. May 13th, 2022 ([CCS]: 5.2. Lecture Notes): A logical characterization of bisimilarity and its use to show process inequivalences; sublogics for double simulation and for trace equivalence; a logic for weak bisimilarity. May 18th, 2022 ([PI]: Chapt.1. Lecture Notes): The picalculus: from CCS, through valuepassing CCS; syntax and reduction semantics; implementing recursive parametric definitions through replication. May 20th, 2022 ([PI]: Chapter 2.1, 2.2. Lecture Notes): The polyadic version of the calculus and a type system for correct communications. Encoding the polyadic version of the calculus in the monadic version. The asynchronous calculus and the encoding of synchrony into asynchrony. May 25th, 2022 ([PI]: Chapt. 2.3, 4. Lecture Notes): The higherorder calculus, encoding replication and encoding HOpi in the first order paradigm. Encoding the lazy lambdacalculus and an objectoriented calculus. May 27th, 2022: Fourth classwork.
Exam modalitiesThere are two possible ways to pass the exam:

NewsCourse Material and Googlegroup Students can have access to all text books and lecture notes by sending an email to the teacher and ask to be included in the googlegroup of the curse. The first posts of this group contain in attachment all what you need for studying. Please, register with the email address that you most frequently access, because important and urgent news about the course will be primarily posted on this group. Furthermore, you'll receive all information for remotely attending the classes on such googlegroup (zoom meeting number and password). Of course, students can also come in presence, by following Sapienza's rules.  DanieleGorla  20 Jan 2016

 DanieleGorla  03 Mar 2005
I  Attachment  History  Action  Size  Date  Who  Comment 

diningphilosophers.pdf  r1  manage  112.3 K  20220308  07:36  DanieleGorla  
lez_1.pdf  r1  manage  1473.6 K  20220222  08:38  DanieleGorla  
lez_10.pdf  r1  manage  5373.8 K  20220222  08:38  DanieleGorla  
lez_11.pdf  r1  manage  4924.2 K  20220222  08:39  DanieleGorla  
lez_12.pdf  r1  manage  367.2 K  20220222  08:39  DanieleGorla  
lez_13.pdf  r1  manage  1103.1 K  20220222  08:39  DanieleGorla  
lez_14.pdf  r1  manage  1526.9 K  20220222  08:39  DanieleGorla  
lez_15.pdf  r1  manage  892.4 K  20220222  08:39  DanieleGorla  
lez_16.pdf  r1  manage  270.9 K  20220222  08:39  DanieleGorla  
lez_17.pdf  r1  manage  586.8 K  20220222  08:39  DanieleGorla  
lez_18.pdf  r1  manage  586.0 K  20220222  08:39  DanieleGorla  
lez_19.pdf  r1  manage  724.6 K  20220222  08:39  DanieleGorla  
lez_2.pdf  r1  manage  1049.8 K  20220222  08:38  DanieleGorla  
lez_20.pdf  r1  manage  1420.8 K  20220222  08:39  DanieleGorla  
lez_21.pdf  r1  manage  637.5 K  20220222  08:40  DanieleGorla  
lez_3.pdf  r1  manage  4236.6 K  20220222  08:38  DanieleGorla  
lez_4.pdf  r1  manage  4872.0 K  20220222  08:38  DanieleGorla  
lez_5.pdf  r1  manage  884.5 K  20220222  08:38  DanieleGorla  
lez_6.pdf  r1  manage  3557.7 K  20220222  08:38  DanieleGorla  
lez_7.pdf  r1  manage  4991.0 K  20220222  08:38  DanieleGorla  
lez_8.pdf  r1  manage  5092.2 K  20220222  08:38  DanieleGorla  
lez_9.pdf  r1  manage  5861.8 K  20220222  08:38  DanieleGorla 