Concurrent Systems (prof. Gorla)  AA 20162017
The class is focused on the foundational aspects and on the formal/mathematical semantics of concurrent programming languages. 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).
Febr. 21st, 2017 ([R]: chapt.1, excluding sect.1.2.5): 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). Febr. 23rd, 2017 ([R]: 2.1.1, 2.1.2, 2.1.3, 2.1.4): Atomic read/write registers; mutex for 2 processes (Peterson algorithm); generalizing Peterson's algorithm to n processes. Febr 28th, 2017 ([R]: 2.1.5  only the idea, no algo, no proofs; 2.1.6; 2.1.7  no proofs; 2.1.8): Algorithms with better performances when no concurrency is present: with a tournament tree of 2processes competitions (O(log n)); algorithms with constant time (Lamport and with timing assumptions). March 2nd, 2017 ([R]: 2.2 and 5.2.3): 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. March 7th, 2017 ([R]: 2.3.1, 2.3.2, 2.3.3): Safe registers: Lamport's Bakery algorithm and Aravind's bounded algorithm. March 9th, 2017 ([R]: 3.1, 3.2.1, 3.2.2, 3.2.4): 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 14th, 2017 ([R]: 3.3.1, 3.3.2, 3.3.4, 3.3.5): 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, 2017 ([R]: 10.1, 10.2, 10.3, 10.5): Software Transactional Memory. Opacity and a Logical clackbased STM system (TL2). Virtual World Consistency and a vector clockbased STM system. March 21st, 2017 ([R]: chap. 4): Atomicity: formal definition and compositionality; possible variants and their noncomposability. March 23rd, 2016 ([R]: 5.1, 5.2.1, 5.2.2, 5.2.5, 5.2.6): Mutexfree concurrency: problems of mutex and notion of mutexfreedom, progress conditions. Examples: splitter, timestamp generator and stack (based on compare&swap and on swap plus fetch&add); progress conditions for these examples. March 28th, 2017 ([R]: 5.3; 17.7, 17.7.1, 17.7.2  only the idea, not the formal protocol): From obstructionfreedom to stronger liveness properties through failure detectors (Omega_X and Diamond_P); hints on the implementation of failure detectors. March 30th, 2017 ([R]: 14.1, 14.2, 14.3): Universal object and consensus object; universality of consensus (unbounded waitfree construction). April 4th, 2017 ([R]: 14.5; 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): Binary vs multivalued consensus. Consensus number (for atomic R/W registers, test&set, swap, fetch&add, compare&swap) and consensus hierarchy. April 6th, 2017 ([CCS]: 1; 2.1, 2.2): Automata for describing process behaviors (notion of LTS); inadequacy of trace equivalence for equating nondeterministic processes; simulation, double simulation and bisimulation. April 11th, 2017 ([CCS]: 2.3, 2.4, 2.5): Properties of bisimulation. Syntax for nondeterministic processes: from LTS to the syntax and vice versa. Examples: counter and queue. April 20th, 2017 ([CCS]: 3.1, 3.2): Process interaction, parallel composition and name restriction. A first proof technique for proving properties of LTSs: the case of imagefiniteness. April 27th, 2017 ([CCS]: 3.2, 3.4): A second proof technique for proving properties of LTSs: the case of closure under substitutions. Congruence of Bisimilarity. May 2nd, 2017([CCS]: 3.3, 4.1, 4.2, 4.3.1): A simple example that uses bisimilarity for proving an implementation equivalent to its specification. Some basic properties of bisimilarity. Weak bisimilarity: basic properties, comparison with strong bisimilarity and fundamental laws. May 4th, 2017 ([CCS]: 4.3.2, 4.3.3): Three sophisticated examples: the factory, the lottery and the scheduler. May 9th, 2017 ([CCS]: 5.1): 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, 2017 ([CCS]: 5.2): 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 16th, 2017 ([CCS]: 5.3): The Kennelakis and Smolka Algorithm for bisimulation on finite state LTSs; soundness and complexity. May 18th, 2017 ([PI]: Chapt.1): The picalculus: from CCS, through valuepassing CCS; syntax and reduction semantics; implementing recursive parametric definitions through replication. May 23rd, 2017 ([PI]: 2.1, 2.2): The polyadic version of the calculus: type system and encoding in the monadic version. The asynchronous calculus and the encoding of synchrony into asynchrony. May 25th, 2017 ([PI]: 2.3, 3.1  only sketched  3.2): The higherorder calculus; encoding lambdacalculus (sketch) and an objectoriented calculus.
Exam modalitiesThere are two possible ways to pass the exam:

NewsStarting Time Classes will start at 9am, both on Tuesdays and on Thursdays. Beginning of the classes Classes will regularly start on February 21st, 2017. Course 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.
 DanieleGorla  20 Jan 2016 
 DanieleGorla  03 Mar 2005
Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)

