Tags:
create new tag
view all tags

Concurrent Systems (prof. Gorla) - AA 2017-2018

Teacher Daniele Gorla
Phone 06-4991 8434
Office Via Salaria 113, 3rd floor, room 310
Email gorla@diNOSPAM.uniroma1.it

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 wait-free 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, non-determinism, 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.


Timetable

2nd semester (end of February --> end of May).

Orario Aula
mon 10:30 (actually, 10.40) - 13:00 Aula Alfa (Via Salaria)
thu 8:00 (actually, 8.15) - 10:30 Aula Alfa (Via Salaria)


Text books

First part:

  • M. Raynal: Concurrent Programming: Algorithms, Principles and Foundations. Springer, 2013. (chapters 1, 2, 3, 4, 5, 10, 14, 16 and part of 17).

Second part:

  • R. Milner. Communicating and Mobile Systems. Cambridge University Press, 1999. (chapters: 1, 2 (no 2.3), 3, 4 (no 4.1, 4.4, 4.5 and 4.6), 5 (no prop. 5.2, ex 5.3, lemma 5.4/5.5, theor. 5.6, def. 5.17, prop. 5.18, prop. 5.23), 6 (no 6.3) and 7 (only 7.2 and 7.3).
  • R. Cleaveland and S. Smolka. Process Algebra. In Encyclopedia of Electrical Engineering, John Wiley & Sons, 1999. Available at http://www.cs.umd.edu/~rance/publications/papers/ee99.ps.gz. (sect. 3.2, 4.1 and 4.2).
  • R. Cleaveland and O. Sokolsky. Equivalence and Preorder Checking for Finite-State Systems. In "Handbook of Process Algebra," pp. 391-424, Elsevier, 2001. Available at http://www.cis.upenn.edu/~sokolsky/PAhandbook.pdf. (sect. 3.1).

Third part:


Detailed Program

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


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 above).

March 1st, 2018 ([R]: chapt.1, excluding sect.1.2.5; 2.1.1, 2.1.2, 2.1.3): 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).

March 8th, 2018 ([R]: 2.1.4; 2.1.5 - only the idea, no algo, no proofs; 2.1.6; 2.1.7 - no proofs): Generalizing Peterson's algorithm to n processes. Algorithms with better performances when no concurrency is present: with a tournament tree of 2-processes competitions (O(log n)); algorithms with constant time (Lamport).

March 12th, 2018 ([R]: 2.1.8; 2.2 and 5.2.3): Another algorithm with constant time (but with timing assumptions). From Deadlock freedom to Starvation freedom using atomic r/w-registers; mutex with specialized HW primitives (test&set; swap; compare&set; fetch&add); the ABA problem with the compare&set.

March 15th, 2018 ([R]: 2.3.1, 2.3.2, 2.3.3): Safe registers: Lamport's Bakery algorithm and Aravind's bounded algorithm.

March 19th, 2018 ([R]: chapter 2): First classwork.

March 22nd, 2018 ([R]: 3.1, 3.2.1, 3.2.2, 3.2.4, 3.3.1, 3.3.2, 3.3.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). Monitors: concept and implementation through semaphores; implementing rendez-vous through monitors.

March 26th, 2018 ([R]: 3.3.5, 10.1, 10.2, 10.3, 10.5): 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 this paper: https://www.sciencedirect.com/science/article/pii/S0304397512004021/pdf?md5=78dd63551d097b6a3212285669d20ff8&pid=1-s2.0-S0304397512004021-main.pdf, sections 2.6 and 3.2).

April 5th, 2018 ([R]: chap. 4): Atomicity: formal definition and compositionality; possible variants and their non-composability.

April 9th, 2018 ([R]: chapters 3, 4 and 10): Second classwork.

April 12th, 2018 ([R]: 5.1, 5.2.1, 5.2.2, 5.2.6, 5.3.1, 5.3.2, 5.3.3; 17.7, 17.7.1, 17.7.2 -- only the idea, not the formal protocol): 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); progress conditions for these examples. From obstruction-freedom to non-blocking through failure detector Omega_X; hints on the implementation of Omega_X.

April 16th, 2018 ([R]: 5.3.4; 14.1, 14.2, 14.3): From obstruction-freedom to wait-freedom through failure detector Diamond_P; hints on the implementation of Diamond_P. Universal object and consensus object; universality of consensus (unbounded wait-free construction).

April 19th, 2018 ([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 23th, 2018 ([R]: chapts 5, 14 and 16): Third classwork.

April 26th, 2018 ([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. Examples: counter and queue.

May 2nd, 2018 ([CCS]: chapter 3.1, 3.2, 3.3): 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. A simple example that uses bisimilarity for proving an implementation equivalent to its specification.

May 3rd, 2018([CCS]: 3.4, 4.1, 4.2, 4.3.2): Congruence of Bisimilarity. Weak bisimilarity: basic properties, comparison with strong bisimilarity and fundamental laws. An example using weak bisimilarity: the lottery.

May 7th, 2018 ([CCS]: chapters 1 to 4): Fourth classwork.

May 10th, 2018 ([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 17th, 2018 ([CCS]: 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 21st, 2018 ([CCS]: 5.3): The Kennelakis and Smolka Algorithm for bisimulation on finite state LTSs; soundness and complexity.

May 24th, 2018 ([PI]: Chapt.1, 2.1): The pi-calculus: from CCS, through value-passing CCS; syntax and reduction semantics; implementing recursive parametric definitions through replication. The polyadic version of the calculus and a type system for correct communications.

May 28th, 2018 ([PI]: 2.2, 2.3, 3.1- only sketched - and 3.2): Encoding the polyadic version of the calculus in the monadic version. The asynchronous calculus and the encoding of synchrony into asynchrony. The higher-order calculus. Encoding an object-oriented calculus.

May 31st, 2018 ([CCS]: chapt. 5; [PI]: chapters 1, 2, 3): Fifth classwork.


Exam modalities

There are two possible ways to pass the exam:

  • First modality (better suited for students who regularly attend the classes): classworks, approx one every two weeks. Students should pass 4 over 6 classworks. The final mark will be the average of the 4 better marks in such classworks.
  • Second modality: oral exam on all the topics presented during the classes.


News

Monday, May 21st The class will take place in Aula Seminari (3rd floor).

Monday, May 14th The class will NOT take place.

Extra class on Wednesday 2/5 The class lost on Monday 30/4 will take place on Wednesday 2/5 (10.30--13) in aula seminari (Via Salaria 113, 3rd floor).

Monday, April 23rd Third classwork, on chapters 5, 14 and 16 of Raynal's book.

Monday, April 9th Second classwork, on chapters 3, 4 and 10 of Raynal's book.

Monday, March 19th First classwork, on chapter 2 of Raynal's book.

No classes on Monday 5th Due to elections in Italy, all university will be closed on March 5th, 2018.

Beginning of the classes Due to adverse weather forecasts, Classes will start on March 1st, 2018.

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

Edit | Attach | Watch | Print version | History: r127 < r126 < r125 < r124 < r123 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r127 - 2018-05-24 - DanieleGorla





 
Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2018 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback