SCQ1098228 - LANGUAGES FOR CONCURRENCY AND DISTRIBUTION 2023-2024
Attività settimanale
-
For a general description of the course unit and of the corresponding exam, consult the course web page.
This moodle will contain the course diary, additional material and other "dynamic" information. In the description of the topics, RSBook identifies the recommended text "Reactive Systems", Aceto, Ingolfsdottir, Larsen, Srba, that covers the first part of the course.
Lessons will be delivered in person in room 1BC50 (Torre Archimede). They will start on Tuesday Feb 27 (hence there will be no lesson on Monday Feb 26).
-
- Lesson 1
- Introduction to the course [RSBook Chap. 1]
-
- Lesson 2
- The language CCS, informally [RSBook Section 2.1]
- Lesson 3
- The language CCS: formal syntax and operational semantics [RSBook 2.2.1, 2.2.2]
- Lesson 2
-
- Lesson 4
- Examples in CAAL (Mutex, Dining Philosophers, Peterson Algorithm - sources available here).
- The need of a notion of program equivalence.
- Lesson 5
- Value passing CCS [RSBook 2.2.3]
Exercises:
- RSBook Ex. 2.7. Build the transition system of the process \(\mathit{Office}\) defined as follows:
\(\mathit{Office} = (CS | CM) \setminus \{\mathit{coin},\mathit{coffee}\}\)
\(CS = \overline{pub}. \overline{coin}. \mathit{coffee}. CS\)
\(CM = \mathit{coin}. \overline{\mathit{coffee}}. CM\)
- RSBook Es. 2.8. Let \(A = b.a.B\). Prove that the following transitions exist/do not exist:
\((A | \bar{b}.0) \setminus \{b\} \stackrel{\tau}{\to} (a.B | 0) \setminus \{b\}\)
\((A | \bar{b}.0) \setminus \{a\} \stackrel{b}{\to} (a.B | \bar{b}.0) \setminus \{a\}\)
\((A | \bar{b}.a.B) + (\bar{b}.A)[a/b] \stackrel{\bar{b}}{\to} (A | a.B)\)
\((A | \bar{b}.a.B) + (\bar{b}.A)[a/b] \stackrel{\bar{a}}{\to} (A | a.B)\)
\(A + a.B \not \stackrel{c}{\to}\)
- Using
the process \(Sem\) as defined during the lesson, implement a semaphore
\(Sem_2\) which allows for two processes to enter the critical section,
as indicated by the following specification:
\(\mathit{Sem}_2 = p. \mathit{Sem}_1\)
\(\mathit{Sem}_1 = p. \mathit{Sem}_0 + v. \mathit{Sem}_2\)
\(\mathit{Sem}_0 = v. \mathit{Sem}_1\)
- Exercise (Buffer)
Solve the exercise at the following link.
-
- Lesson 6
- (Strong) Bisimilarity [RSBook 3.3]
- Lesson 7
- (Strong) Bisimilarity and its game-theoretical characterization [RSBook 3.5]
- Properties of bisimilarity: largest bisimulation and equivalence [RSBook 3.3]
- Finite CCS (exercise)
Exercises:
Solve exercises 3.3 and 3.5 in [RSBook] -
- Lesson 8
- Properties of bisimilarity: exercises and compositionality [RSBook 3.3]
- Lesson 9
- Weak bisimilarity: definition [RSBook 3.4]
- Weak bisimilarity: definition [RSBook 3.4]
Exercises:
- Exercise 3.15 in RSBook (Barrier)
- Exercise (Up-to bisimulation): A bisimulation up-to bisimilarity is a relation \(\mathbf{R} \subseteq \mathit{Proc} \times \mathit{Proc}\) such that, whenever \(P \mathbf{R} Q\) it holds that
- for all \(P \stackrel{\alpha}{\to} P'\) there exists \(Q \stackrel{\alpha}{\to} Q'\) with \(P' \sim P'' \mathbf{R} Q'' \sim Q'\)
- for all \(Q \stackrel{\alpha}{\to} Q'\) there exists \(P \stackrel{\alpha}{\to} P'\) with \(P' \sim P'' \mathbf{R} Q'' \sim Q'\)
Show that if \( \mathbf{R}\) is a bisimulation up-to bisimilarity then \(P \mathbf{R} Q \) implies \( P \sim Q \).
-
-
- (Lesson 10)
- Weak bisimilarity: properties [RSBook 3.4]
- Weak bisimilarity: properties [RSBook 3.4]
- (Lesson 11)
- Fixed point theory [RSBook 4.1, 4.2, limited to powerset lattices]
- Bisimilarity as a fixpoint [RSBook 4.3
Assignment: Exercises 3.27, 3.28, 3.29 in [RSBook] - (Lesson 10)
-
- (Lesson 12)
- Hennessy-Milner logic [RSBook 5, 5.1]
- (Lesson 13)
- Logic with recursion: introduction, example of properties, syntax and semantics [RSBook 6, 6.1]
- (Lesson 12)
-
- (Lesson 14)
- Verifying properties with the Edimburgh CWB: mutual exclusion, fairness, liveness, deadlock freedom, etc.
[CWB examples] - (Lesson 15)
- Pi-calculus
- From modelling to programming languages [slides]
- (Lesson 14)
-
-
- Lesson 18
- Google Go: Concurrency. Part 2.
- using select and timeouts
- concurrency and shared memory
- channels of channels: server, task splitting, replication, pipeline idioms.
- Google Go: Concurrency. Part 2.
- Lesson 19
- Google Go: Concurrency. Part 3:
- Low level concurrency and memory model
- The scheduler
- Concluding remarks
- Erlang: Some basic ideas
- Google Go: Concurrency. Part 3:
- Lesson 18
-
-