Concurrency 1 : Shared Memory

Description

.Concurrency 1Shared MemoryJean-Jacques L¶evy (INRIA - Rocq)MPRI concurrency course with :Pierre-Louis Curien (PPS)Eric Goubault (CEA)James Leifer (INRIA - Rocq)Catuscia Palamidessi (INRIA - Futurs)1.Why concurrency?1. Programs for multi-processors2. Drivers for slow devices3. Human users are concurrent4. Distributed systems with multiple clients5. Reduce lattency6. Increase e–ciency, but Amdahl’s lawNS =b∗N +(1−b)(S =speedup, b=sequential part, N processors)2.MPRI concurrency course09-30 JJL shared memory atomicity, SOS10-07 JJL sharedry readers/writers, 5 philosophers10-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 proofs11-16 JL π-calculus syntax, lts, examples, strong bisim.11-25 JL π red. semantics, weak bisim., congruence12-02 JL π-calculus extensions for mobility12-09 JL/CP π encodings : λ-calculus, arithm., lists12-16 CP π-calculus expressivity01-06 CP π stochastic models01-13 CP π-calculus security01-20 EG true concurrency concurrency and causality01-27 EG true Petri nets, events struct., async. trans.02-03 EG true other models02-10 all exercices02-17 examhttp://pauillac.inria.fr/~leifer/teaching/mpri-concurrency-2004/3.Concurrency ⇒ non-determinismSuppose x is a global variable. At beginning, x=0ConsiderS =[x:=1;]T =[x:=2;]After S||T, then x∈{1,2}Conclusion :Result is not unique.Concurrent programs are not ...

Informations

• Publié par: Kahej
• Nombre de lectures: 19
• Langue: English

Extrait

.

Concurrency

1

Shared Memory

Jean-JacquesLe´vy(INRIA-Rocq)

MPRI concurrency course with :

Pierre-Louis Curien (PPS) Eric Goubault (CEA) James Leifer (INRIA - Rocq) Catuscia Palamidessi (INRIA - Futurs)

1

.

.

.

.

.

.

.

.

.

.