0.82074 Concurrency 1_{Shared Memory} Catuscia Palamidessi INRIA Futurs and LIX - Ecole Polytechnique The other lecturers for this course: Jean-Jacques Lévy (PPS) James Leifer (INRIA - Rocq) Eric Goubault (CEA) http://pauillac.inria.fr/˜ leifer/teaching/mpri-concurrency-2004/^{Motivation Overview of the course Concurrency in Shared Memory: Effects and Issues Critical Sections and Mutual Exclusion} 0.82074 Outline 1 Motivation1 2Overview of the course1 3Concurrency in Shared Memory: Effects and Issues2 4Critical Sections and Mutual Exclusion3 4.1 Some attempts to implement a critical section3 4.2 Some famous algorithms4 4.3 Semaphores6 4.4 The dining philosophers7 4.5 Exercises7^{Motivation Overview of the course Concurrency in Shared Memory: Effects and Issues Critical Sections and Mutual Exclusion} 0.82074 Motivation_{Why Concurrency?} Programs for multi-processors Drivers for slow devices Human users are concurrent Distributed systems with multiple clients Reduce latency Increase efficiency, but Amdahl’s law S = \frac{N}{b ∗ N + (1 − b)} (S = speedup , b = sequential part, N processors)^{Motivation Overview of the course Concurrency in Shared Memory: Effects and Issues Critical Sections and Mutual Exclusion} 0.82074 Overview of the course_{09-28  CP  Shared memory: atomicity 10-05  CP/JJL  Shared memory: verification, report on Ariane 501 10-12  CP  CCS: syntax and transitions, coinduction 10-19  CP  CCS: weak and strong bisimulations, axiomatization 10-26  CP  CCS: examples, Hennessy-Milner logic 11-02  JL  π-calculus: syntax; reduction, transitions, strong bisimulation 11-09  JL  π-calculus: sum, abstractions, data structures, bisimulation proofs 11-16  JL  π-calculus: bisimulation “up to”, congruence, barbed bisimulation 11-23  Review 11-30  MT exam 12-07  JL  π-calculus: comparison between equivalences 12-14  JJL  Expressivity of the pi-calculus and its variants 12-21  vacation 12-28  vacation 01-04  JJL  Distributed pi-calculus 01-11  JJL  Problems with distributed implementation 01-18  EG  True concurrency versus interleaving semantics 01-25  EG  Event structures and Petri nets 02-01  EG  Application to the semantics of CCS 02-08  EG  Comparison of the expressiveness of different models 02-15  Review 02-22  Final exam}^{Motivation Overview of the course Concurrency in Shared Memory: Effects and Issues Critical Sections and Mutual Exclusion}