Tags:
create new tag
view all tags
<table border=2><tr valign=top><td width="80%"> ---++ Concurrent Systems (prof. Gorla) - AA 2022-2023 | *Teacher* | Daniele Gorla ||| | *Phone* | 06-49255431 ||| | *Office* | Viale Regina Elena 295, 2nd floor, room 205 ||| | *Email* | gorla@di.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). <center> | *Timetable* | *Lecture room* | | mon 8:15 - 11:00 | Aula T1 (Viale Regina Elena, building E, ground floor) | | tue 8:15 - 10:00 | Aula T1 (Viale Regina Elena, building E, ground floor) | </center> ---- ---++ Text books First part: * M. Raynal: <I>Concurrent Programming: Algorithms, Principles and Foundations</I>. Springer, 2013. (chapters 1, 2, 3, 4, 5, 10, 14, 16 and part of 17). Second part: * R. Milner. <I>Communicating and Mobile Systems.</I> 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. <I>Process Algebra.</I> 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. <I>Equivalence and Preorder Checking for Finite-State Systems.</I> 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: * J. Parrow. <I>An Introduction to the pi-Calculus.</I> In Handbook of Process Algebra, pages 479-543. Elsevier, 2001. Available at http://user.it.uu.se/~joachim/intro.ps * R. Milner. <I>The Polyadic pi-Calculus: A Tutorial.</I> In Logic and Algebra of Specification. Springer-Verlag, 1993. Available at http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps * D. Sangiorgi, D. Walker. <I>The Pi-Calculus - A Theory of Mobile Processes.</I> Cambridge University Press, 2001. The reference book on the pi-calculus; maybe, quite difficult for a master student. * http://www.cs.unibo.it/~zavattar/Publication/icalp03.ps. Comparison of recursion and replication in process calculi. * http://www.cs.unibo.it/~sangio/DOC_public/pi.ps.gz. The classical notion of subtyping in the pi-calculus. * http://www.cs.unibo.it/~zavattar/Publication/tcs00.ps. A comparison of three different kinds of output actions in a CCS-like language. * http://lucacardelli.name/Papers/Mobility%20and%20Security.A4.pdf. A nice survey on a calculus very trend a few years ago. There are two logically distinct parts: I+II+III and IV+V. * http://lucacardelli.name/Papers/Brane%20Calculi.pdf. A funny work on a formalism for bio-inspired computing. * https://www.cs.bham.ac.uk/~mdr/research/papers/pdf/11-applied-pi.extended.pdf. A survey on one of the best known cryptographic versions of the pi-calculus. ---- ---++ 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). <b><font color="#008000">Feb 20th, 2023 </font>([R]: chapt.1, excluding sect.1.2.5; 2.1.1, 2.1.2, 2.1.3, 2.1.4): </b> 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. <b><font color="#008000">Feb 21st, 2023 </font>([R]: 2.1.5 - only the idea, no algo, no proofs; 2.1.6; 2.1.7; 2.2.2):</b> 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. <b><font color="#008000">Feb 27th, 2023 </font>([R]: 2.2; 2.3.1, 2.3.2, 2.3.3): </b> Mutex with specialized HW primitives (test&set; swap; compare&set; fetch&add). Safe registers: Lamport's Bakery algorithm and Aravind's bounded algorithm. <b><font color="#008000">Feb 28th, 2023 </font>([R]: 3.1, 3.2.1, 3.2.2, 3.2.4, 3.3.1, 3.3.2, 3.3.4, 3.3.5. ): </b> 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. Readers/writers through monitors. <b><font color="#008000">March 6th, 2023 </font>([R]: 10.1, 10.2, 10.3, 10.5): </b> 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). <b><font color="#008000">March 7th, 2023 </font>([R]: chap. 4): </b> Atomicity: formal definition and compositionality; possible variants and their non-composability. <b><font color="#008000">March 14th, 2023 </font>([R]: 5.1, 5.2.1, 5.2.2, 5.2.5, 5.2.6. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_8.pdf][Lecture Notes]]): </b> 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. <b><font color="#008000">March 15th, 2023 </font>([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. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_9.pdf][Lecture Notes]]): </b> 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. <b><font color="#008000">March 20th, 2023 </font>([R]: 14.1, 14.2, 14.3, 14.5. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_10.pdf][Lecture Notes]]): </b> Universal object and consensus object; universality of consensus (unbounded wait-free construction). Binary vs multivalued consensus. <b><font color="#008000">March 21st, 2023 </font>([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. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_11.pdf][Lecture Notes]]): </b> Consensus number (for atomic R/W registers, test&set, swap, fetch&add, compare&swap) and consensus hierarchy. <b><font color="#008000">March 27th, 2023 </font>: </b> 1st classwork <b><font color="#008000">March 28th, 2023 </font>([CCS]: chapters 1 and 2.[[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_12.pdf][Lecture Notes]] and [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_13.pdf][Lecture Notes]]): </b> 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. <b><font color="#008000">April 17th, 2023 </font>([CCS]: chapter 3.1, 3.2, 3.3. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_13.pdf][Lecture Notes]]): </b> 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. Congruence of Bisimilarity. <b><font color="#008000">April 18th, 2023</font>([CCS]: 4.3. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_14.pdf][Lecture Notes]]): </b> Weak bisimilarity: basic properties, comparison with strong bisimilarity and fundamental laws. <b><font color="#008000">May 9th, 2023 </font>([CCS]: 5.1. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_15.pdf][Lecture Notes]]): </b> Examples using weak bisimilarity: the factory, the lottery and the scheduler. <!-- <b><font color="#008000">May 15th, 2023 </font>([CCS]: 5.3. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_16.pdf][Lecture Notes]]): </b> 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. <b><font color="#008000">May 16th, 2023 </font>([CCS]: 5.2. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_17.pdf][Lecture Notes]]): </b> The Kennelakis and Smolka Algorithm for bisimulation on finite state LTSs; soundness and complexity. <b><font color="#008000">May 29th, 2023 </font>([CCS]: 5.2. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_17.pdf][Lecture Notes]]): </b> 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. <b><font color="#008000">May 30th, 2023 </font>: </b> 2nd classwork. <b><font color="#008000">May 18th, 2022 </font>([PI]: Chapt.1. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_18.pdf][Lecture Notes]]): </b> The pi-calculus: from CCS, through value-passing CCS; syntax and reduction semantics; implementing recursive parametric definitions through replication. <b><font color="#008000">May 20th, 2022 </font>([PI]: Chapter 2.1, 2.2, 2.3. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_19.pdf][Lecture Notes]]): </b> 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. The higher-order calculus, encoding replication and encoding HOpi in the first order paradigm. <b><font color="#008000">May 25th, 2022 </font>([PI]: Chapt. 4. [[https://twiki.di.uniroma1.it/pub/TC/WebHome/lez_21.pdf][Lecture Notes]]): </b> Encoding the lazy lambda-calculus and an object-oriented calculus. <b><font color="#008000">May 27th, 2022</font>: </b> Fourth classwork. <b><font color="#008000">March 16th, 2020 </font>([R]: chapter 2): </b> First classwork. <b><font color="#008000">March 30th, 2020 </font>([R]: chapters 3, 4 and 10): </b> Second classwork. <b><font color="#008000">April 20th, 2020 </font>([R]: chapts 5, 14 and 16): </b> Third classwork. <b><font color="#008000">May 13th, 2020 </font>([CCS]: chapters 1-5): </b> Fourth classwork. <b><font color="#008000">May 27th, 2020 </font>([PI]: chapters 1, 2, 3): </b> Fifth classwork. <b><font color="#008000">May 27th, 2022 </font>([PI]: Chapt. 3): </b> A labelled transition system for the pi-calculus; bisimilarity and bisimulation congruence; weak bisimilarity. --> ---- ---++ 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 3 over 5 classworks. There will be 3 classworks for the first part and 2 for the second+third part; students must pass at least 2 from the first part and 1 from the second part of the course. The final mark will be the average of the 3 better marks in such classworks (FEASIBILITY OF THIS MODALITY NEEDS TO BE CHECKED, ACCORDING TO THE CURRENT COVID REGULATIONS) * First modality (better suited for students who regularly attend the classes): homeworks, one every week, to be presented during the Wednesday class. On Friday afternoon, I'll send in the googlegroup the text of 3/4 exercises on the topics presented during the classes of the week. You have time to solve the exercises on your own and send them to me your solutions by email. Every week, 3 or 4 students will present their solutions and publicly discuss them with me and the class. The policy for selecting the students is two-fold: FIFO (who arrives first in sending me the email gets the opportunity to present) and number of presentations already done (if you have done few presentations, you've the priority). Every discussion will have a mark (REMARK: not only on the solution itself that you propose, but mostly on the way in which you present it and on how you reply to my questions -- that can also be on topics that I explained during the course). To pass the exam, you must present your solutions at least 4 times during the term (2 times on the first part of the course, and 2 times on the second one). The final mark will be obtained as the average of the 4 best marks obtained at every presentation. --> * First modality (better suited for students who regularly attend the classes): 2 classworks. * Second modality: written and oral exam on all the topics presented during the classes. ---- </td><td width="20%"> %INCLUDE{"News"}% %FINE% </td></tr> </table> <!-- * Set ALLOWTOPICCHANGE = Users.DocentiGroup --> -- Users.DanieleGorla - 03 Mar 2005
E
dit
|
A
ttach
|
Watch
|
P
rint version
|
H
istory
: r199
<
r198
<
r197
<
r196
<
r195
|
B
acklinks
|
V
iew topic
|
Ra
w
edit
|
M
ore topic actions
Topic revision: r199 - 2023-04-13
-
DanieleGorla
Log In
or
Register
TC Web ...
TC Web
TC Web Home
Users
Groups
Index
Search
Changes
Notifications
Statistics
Preferences
User Reference ...
User Reference
ATasteOfTWiki
TextFormattingRules
TWikiVariables
FormattedSearch
TWikiDocGraphics
TWikiSkinBrowser
InstalledPlugins
ChangeEmailAddress
ChangePassword
ResetPassword
Prenotazioni esami
Laurea Triennale ...
Laurea Triennale
Algebra
Algoritmi
Introduzione agli algoritmi
Algoritmi 1
Algoritmi 2
Algoritmi per la
visualizzazione
Architetture
Prog. sist. digitali
Architetture 2
Basi di Dati
Basi di Dati 1 Inf.
Basi di Dati 1 T.I.
Basi di Dati (I modulo, A-L)
Basi di Dati (I modulo, M-Z)
Basi di Dati 2
Calcolo
Calcolo differenziale
Calcolo integrale
Calcolo delle Probabilitą
Metodi mat. per l'inf. (ex. Logica)
canale AD
canale PZ
Programmazione
Fond. di Programmazione
Metodologie di Programmazione
Prog. di sistemi multicore
Programmazione 2
AD
EO
PZ
Esercitazioni Prog. 2
Lab. Prog. AD
Lab. Prog. EO
Lab. Prog. 2
Prog. a Oggetti
Reti
Arch. di internet
Lab. di prog. di rete
Programmazione Web
Reti di elaboratori
Sistemi operativi
Sistemi Operativi (12 CFU)
Anni precedenti
Sistemi operativi 1
Sistemi operativi 2
Lab. SO 1
Lab. SO 2
Altri corsi
Automi, Calcolabilitą
e Complessitą
Apprendimento Automatico
Economia Aziendale
Elaborazione Immagini
Fisica 2
Grafica 3D
Informatica Giuridica
Laboratorio di Sistemi Interattivi
Linguaggi di Programmazione 3° anno Matematica
Linguaggi e Compilatori
Sistemi Informativi
Tecniche di Sicurezza dei Sistemi
ACSAI ...
ACSAI
Computer Architectures 1
Programming
Laurea Magistrale ...
Laurea Magistrale
Percorsi di studio
Corsi
Algoritmi Avanzati
Algoritmica
Algoritmi e Strutture Dati
Algoritmi per le reti
Architetture degli elaboratori 3
Architetture avanzate e parallele
Autonomous Networking
Big Data Computing
Business Intelligence
Calcolo Intensivo
Complessitą
Computer Systems and Programming
Concurrent Systems
Crittografia
Elaborazione del Linguaggio Naturale
Estrazione inf. dal web
Fisica 3
Gamification Lab
Information Systems
Ingegneria degli Algoritmi
Interazione Multi Modale
Metodi Formali per il Software
Methods in Computer Science Education: Analysis
Methods in Computer Science Education: Design
Prestazioni dei Sistemi di Rete
Prog. avanzata
Internet of Things
Sistemi Centrali
Reti Wireless
Sistemi Biometrici
Sistemi Distribuiti
Sistemi Informativi Geografici
Sistemi operativi 3
Tecniche di Sicurezza basate sui Linguaggi
Teoria della
Dimostrazione
Verifica del software
Visione artificiale
Attivitą complementari
Biologia Computazionale
Design and development of embedded systems for the Internet of Things
Lego Lab
Logic Programming
Pietre miliari della scienza
Prog. di processori multicore
Sistemi per l'interazione locale e remota
Laboratorio di Cyber-Security
Verifica e Validazione di Software Embedded
Altri Webs ...
Altri Webs
Dottorandi
Commissioni
Comm. Didattica
Comm. Didattica_r
Comm. Dottorato
Comm. Erasmus
Comm. Finanziamenti
Comm. Scientifica
Comm Scientifica_r
Corsi esterni
Sistemi Operativi (Matematica)
Perl e Bioperl
ECDL
Fondamenti 1
(NETTUNO)
Tecniche della Programmazione 1° modulo
(NETTUNO)
Seminars in Artificial Intelligence and Robotics: Natural Language Processing
Informatica generale
Primo canale
Secondo canale
II canale A.A. 10-11
Informatica
Informatica per Statistica
Laboratorio di Strumentazione Elettronica e Informatica
Progetti
Nemo
Quis
Remus
TWiki ...
TWiki
Tutto su TWiki
Users
Main
Sandbox
Home
Site map
AA web
AAP web
ACSAI web
AA2021 web
Programming web
AA2021 web
AN web
ASD web
Algebra web
AL web
AA1112 web
AA1213 web
AA1920 web
AA2021 web
MZ web
AA1112 web
AA1213 web
AA1112 web
AA1314 web
AA1415 web
AA1516 web
AA1617 web
AA1819 web
Old web
Algo_par_dis web
Algoreti web
More...
TC Web
Create New Topic
Index
Search
Changes
Notifications
RSS Feed
Statistics
Preferences
View
Raw View
Print version
Find backlinks
History
More topic actions
Edit
Raw edit
Attach file or image
Edit topic preference settings
Set new parent
More topic actions
Account
Log In
Register User
Questo sito usa cookies, usandolo ne accettate la presenza. (
CookiePolicy
)
Torna al
Dipartimento di Informatica
E
dit
A
ttach
Copyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki?
Send feedback