31 Pages
English
Learn all about the services we offer

# Concurrency 1 : Shared Memory

Learn all about the services we offer
31 Pages
English

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 ...

Subjects

##### IT systems

Informations

Exrait

.
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
.
.
.
.
.
.
.
.
.
.