Concurrency : Shared memory atomicity

. .MPRI concurrency course09-30 JJL shared memory atomicity, SOS10-07 JJL shared memory readers/writers, 5 philosophersConcurrency 110-12 PLC CCS choice, strong bisim.10-21 PLC CCS weak bisim., examples10-28 PLC CCS obs. equivalence, Hennessy-Milner logic11-04 PLC CCS examples of proofsShared Memory11-16 JL π-calculus syntax, lts, examples, strong bisim.11-25 JL π-calculus red. semantics, weak bisim., congruence12-02 JL π-calculus extensions for mobilityJean-Jacques L´evy (INRIA - Rocq)12-09 JL/CP π-calculus encodings : λ-calculus, arithm., lists12-16 CP π-calculus expressivityMPRI concurrency course with :01-06 CP π-calculus stochastic modelsPierre-Louis Curien (PPS)01-13 CP π-calculus securityEric Goubault (CEA)01-20 EG true concurrency concurrency and causalityJames Leifer (INRIA - Rocq) 01-27 EG true concurrency Petri nets, events struct., async. trans.02-03 EG true concurrency other modelsCatuscia Palamidessi (INRIA - Futurs)02-10 all exercices02-17 examhttp://pauillac.inria.fr/~leifer/teaching/mpri-concurrency-2004/1 3. .Why concurrency? Concurrency⇒ non-determinismSuppose x is a global variable. At beginning, x = 01. Programs for multi-processorsConsider2. Drivers for slow devicesS = [x := 1;]3. Human users are concurrentT = [x := 2;]4. Distributed systems with multiple clientsAfter S ||T, then x∈{1,2}5. Reduce lattency6. Increase efficiency, but Amdahl’s lawNConclusion :S =b∗N +(1−b)(S =speedup, b =sequential part, N ...