Course Diary

Here, [R] denotes Raynal's book; [CCS] and [PI] denote teacher's lecture notes on CCS and pi-calculus (that are a unified and coherent presentation of the texts for the second and the third part of the course listed in the home page).

Feb 26th, 2024 ([R]: chapt.1, excluding sect.1.2.5; 2.1.1, 2.1.2, 2.1.3, 2.1.4): 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). Generalizing Peterson's algorithm to n processes.

Feb 27th, 2024 ([R]: 2.1.5 - only the idea, no algo, no proofs; 2.1.6; 2.1.7; 2.2.2): Algorithms with better performances when no concurrency is present: with a tournament tree of 2-processes competitions (O(log n)); Lamport's fast mutex algorithm (with constant time when there is no contention). From Deadlock freedom to Bounded bypass using atomic r/w-registers.

Mar 4th, 2024 ([R]: 2.2; 2.3.1, 2.3.2, 2.3.3): Mutex with specialized HW primitives (test&set; swap; compare&set; fetch&add). Safe registers: Lamport's Bakery algorithm and Aravind's bounded algorithm.

Mar 5th, 2024 ([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). 

Mar 11th, 2024 ([R]: 3.3.1, 3.3.2, 3.3.4, 3.3.5, 10.1, 10.2, 10.3, 10.5): Monitors: concept and implementation through semaphores; implementing rendez-vous through monitors. Readers/writers through monitors. The problem of the "Dining Philosophers": solutions that break symmetry (through semaphores) and a symmetric solution (through monitors). 

Software Transactional Memory. Opacity and a Logical clock-based STM system (TL2). Virtual World Consistency and a vector clock-based STM system (REMARK: to better understand the difference between virtual world consistency and opacity, look at the original paper (in the Moodle), sections 2.6 and 3.2).

Mar 12th, 2024 ([R]: chap. 4): Atomicity: formal definition and compositionality; possible variants and their non-composability.

Mar 18th, 2024 ([R]: 5.1, 5.2.1, 5.2.2, 5.2.5, 5.2.6): Mutex-free concurrency: problems of mutex and notion of mutex-freedom, progress conditions. Examples: splitter, timestamp generator and stack (based on swap plus fetch&add; based on compare&set); progress conditions for these examples.

Mar 19th, 2024 ([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): From obstruction-freedom to non-blocking through failure detector Omega_X; hints on the implementation of Omega_X. From obstruction-freedom to wait-freedom through failure detector Diamond_P; hints on the implementation of Diamond_P.

Mar 25th, 2024 ([R]: 14.1, 14.2, 14.3, 14.5): Universal object and consensus object; universality of consensus (unbounded wait-free construction). Binary vs multivalued consensus. 

Mar 26th, 2024 ([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): Consensus number (for atomic R/W registers, test&set, swap, fetch&add, compare&swap) and consensus hierarchy.

Apr 8th, 2024: First classwork

Apr 9th, 2024 ([CCS]: chapters 1 and 2): Automata for describing process behaviors (notion of LTS); inadequacy of trace equivalence for equating non-deterministic processes; simulation, double simulation and bisimulation. Properties of bisimilarity. Syntax for non-deterministic processes: from LTS to the syntax and vice versa. 

Apr 15th, 2024 ([CCS]: chapters 2 and 3): Examples: counter and queue. Process interaction, parallel composition and name restriction. A first proof technique for proving properties of LTSs: the case of image-finiteness. A second proof technique for proving properties of LTSs: the case of closure under substitutions. 

Apr 16th, 2024 ([CCS]: chapters 3 and 4): A simple example that uses bisimilarity for proving an implementation equivalent to its specification. Congruence of Bisimilarity. Weak bisimilarity: basic properties, comparison with strong bisimilarity and fundamental laws. 

Apr 22nd, 2024 ([CCS]: chapter 4): Examples using weak bisimilarity: the factory, the lottery and the scheduler.

Apr 23rd, 2024 ([CCS]: chapter 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 6th, 2024 ([CCS]: chapter 5.2): A logical characterization of bisimilarity and its use to show process inequivalences; sub-logics for double simulation and for trace equivalence; a logic for weak bisimilarity.

May 7th, 2024 ([CCS]: chapter 5.3): The Kennelakis and Smolka Algorithm for bisimulation on finite state LTSs; soundness and complexity.

May 13th, 2024 ([PI]: chapters 1 and 3): Pi-calculus: motivation, syntax, reduction semantics and labelled semantics. Bisimilarity in pi-calculus and the problem of input prefixes. Bisimulation congruence.

May 14th, 2024 ([PI]: chapter 2): Polyadic Pi-calculus: syntax, reduction semantics and problem of arity mismatch. A type system for correct communications. Encoding in the monadic pi-calculus. Asynchronous Pi-Calculus: syntax, possible semantics, and encoding the synchronous pi-calculus.

May 20th, 2024 ([PI]: chapter 2 and 4): Higher-Order Pi-calculus: syntax, reduction semantics and encoding in the first order. Encoding Lambda-calculus in Pi-calculus. Encoding an Object-Oriented language in pi-calculus.

May 27th, 2024: second classwork