   8 Pages
English

# Concurrency : Shared memory atomicity

Learn all about the services we offer Description

. .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 eﬃciency, but Amdahl’s lawNConclusion :S =b∗N +(1−b)(S =speedup, b =sequential part, N ...

Subjects

##### IT systems

Informations

Exrait

.
.
Concurrency
Shared
1
Memory
JeanJacquesL´evy(INRIARocq)
MPRI concurrency course with :
PierreLouis Curien (PPS) Eric Goubault (CEA) James Leifer (INRIA  Rocq) Catuscia Palamidessi (INRIA  Futurs)
Why
concurrency ?
1.Programs for multiprocessors 2.Drivers for slow devices 3.Human users are concurrent 4.Distributed systems with multiple clients
5.Reduce lattency 6.Increase eﬃciency, but Amdahl’s law
N S= bN+ (1b) (S=speedup,b=sequential part,Nprocessors)
1
2
.
.
MPRI
concurrency
course
0930 JJL shared memoryatomicity, SOS 1007 JJL shared memoryreaders/writers, 5 philosophers 1012PLC CCSchoice, strong bisim. 1021 PLC CCSweak bisim., examples 1028 PLC CCSobs. equivalence, HennessyMilner logic 1104 PLC CCSexamples of proofs 1116JLπcalculussyntax, lts, examples, strong bisim. 1125 JLπcalculusred. semantics, weak bisim., congruence 1202 JLπcalculusextensions for mobility 1209 JL/CPπcalculusencodings :λcalculus, arithm., lists 1216 CPπcalculusexpressivity 0106 CPπcalculusstochastic models 0113 CPπcalculussecurity 0120 EG true concurrencyconcurrency and causality 0127 EG true concurrencyPetri nets, events struct., async. trans. 0203 EG true concurrencyother models 0210 all exercices 0217 exam http://pauillac.inria.fr/~leifer/teaching/mpriconc urrency2004/
Concurrency
nondeterminism
Supposexis a global variable. At beginning,x= 0
Consider
S= [x]:= 1; T= [x:= 2; ]
AfterS||T, thenx∈ {1,2}
Conclusion :
Result is not unique.
Concurrent programs are not described by functions.
3
4
.
.
Implicit
Communication
Supposexis a global variable. At beginning,x= 0
Consider
S= [x:=x+ 1;x:=x+ 1||x:= 2x]
T= [x:=x+ 1;x:=x+ 1||wait(x= 1);x:= 2x]
AfterS, thenx∈ {2,3,4} AfterT, thenx∈ {3,4} Tmay be blocked
Conclusion
InSandT, interaction viax
Inputoutput
Supposexis a global variable.
Consider
S= [x:= 1] T= [x:= 0;x:=x+ 1]
behaviour
SandTsame functions on memory state.
ButS||SandT||Sare diﬀerent “functions” on memory state.
Interaction is important.
A process is an “atomic” action, followed by a process. Ie.
action×P P 'Null+ 2
Part of the concurrency course gives sense to this equation.
5
6
.
.
Atomicity
Supposexis a global variable. At beginning,x= 0
Consider S= [x:=x+ 1||x:=x+ 1] AfterS, thenx= 2.
However if [x:=x+ 1]compiled into[A:=x+ 1;x:=A]
Then S= [A:=x+ 1;x:=A]||[B:=x+ 1;x:=B] AfterS, thenx∈ {1,2}.
Conclusion 1.[x:=x+ 1]was ﬁrstly considered atomic 2.Atomicity is important
Critical
section
Mutual
LetP0= [∙ ∙ ∙;C0;∙ ∙ ∙]andP1= [∙ ∙ ∙;C1;∙ ∙ ∙]
exclusion
C0andC1are critical sections (ie should not be executed simultaneously).
Solution 1At beginning,turn= 0.
P0 :∙ ∙ ∙ whileturn != 0do ; C0; turn := 1; ∙ ∙ ∙ P0privileged, unfair.
P1 :∙ ∙ ∙ whileturn != 1do ; C1; turn := 0; ∙ ∙ ∙
7
8
Mutual
1965)
(CACM
exclusion
P0 :∙ ∙ ∙ a0 :=true; turn := 1; whilea1 && turn != 0do ; C0; a0 :=false; ∙ ∙ ∙
At beginning,a0=a1=false,turn∈ {0,1}
. Peterson’s
Algorithm
9
(IPL
Algorithm
Algorithm
Dekker’s
Solution 3At beginning,a0=a1=false. P0 :∙ ∙ ∙P1 :∙ ∙ ∙ a0 :=true:=; a1 true; whilea1do whilea0do ; ; C0;C1; a0 :=false:=; a1 false; ∙ ∙ ∙ ∙ ∙ ∙ Deadlock. BothP0andP1blocked.
Solution 2At beginning,a0=a1=false. P0 :∙ ∙ ∙P1 :∙ ∙ ∙ whilea1do whilea0do ; ; a0 :=true:=; a1 true; C0;C1; a0 :=false:=; a1 false; ∙ ∙ ∙ ∙ ∙ ∙ False.
June 81) (2/5)
11
∙ ∙ ∙ ∙ ∙ ∙ a0c06= 2} {¬a1c16= 2} 1 a0 :=truea1 :=; c0 := 2; true; c1 := 2; {a0c0= 2} {a1c1= 2} 2 turn := 1; c0 := 1; turn := 0; c1 := 1; {a0c06= 2} {a1c16= 2} 3whilea1 && turn != 0do whilea0 && turn != 1do . ; ; {a0c06= 2(¬a1turn= 0c1= 2)} {a1c16= 2(¬a1turn= 1c0= 2)} .C0;C1; 5 a0 :=false:=; a1 false; a0c06= 2} {¬a1c16= 2} ∙ ∙ ∙ ∙ ∙ ∙
12
June 81) (1/5)
10
P1 :∙ ∙ ∙ a1 :=true; whilea0do ifturn != 1 begin a1 :=false; whileturn != 1do ; a1 :=true; end; C1; turn := 0; a1 :=false; ∙ ∙ ∙
.
(IPL
c0,c1program counters forP0andP1. At beginningc0=c1= 1
At beginning,a0=a1=false,turn∈ {0,1}
P0 :∙ ∙ ∙ a0 :=true; whilea1do ifturn != 0 begin a0 :=false; whileturn != 0do ; a0 :=true; end; C0; turn := 1; a0 :=false; ∙ ∙ ∙
Exercice 1Trouver Dekker pournprocessus[Dijkstra 1968].
. Peterson’s
P1 :∙ ∙ ∙ a1 :=true; turn := 0; whilea0 && turn != 1do ; C1; a0 :=false; ∙ ∙ ∙
.
Critical
section
. Peterson’s
Algorithm
(IPL
June 81) (3/5)
(turn= 0turn= 1) a0c06= 2(¬a1turn= 0c1= 2)a1c16= 2(¬a0turn= 1c0= 2) (turn= 0turn= 1)tour= 0tour= 1Impossible
. Peterson’s
Algorithm
c0,c1program counters forP0andP1. At beginningc0=c1= 1
(IPL
13
June 81) (4/5)
∙ ∙ ∙ ∙ ∙ ∙ a0c06= 2} {¬a1c16= 2} 1 a0 :=truea1 :=; c0 := 2; true; c1 := 2; {a0c0= 2} {a1c1= 2} 2 turn := 1; c0 := 1; turn := 0; c1 := 1; {a0c06= 2} {a1c16= 2} 3whilea1 && turn != 0do whilea0 && turn != 1do . ; ; {a0c06= 2(¬a1turn= 0c1= 2)} {a1c16= 2(¬a1turn= 1c0= 2)} .C0;C1; 5 a0 :=false; a1 :=false; a0c06= 2} {¬a1c16= 2} ∙ ∙ ∙ ∙ ∙ ∙
14
. Peterson’s
.
Algorithm
(IPL
June 81) (5/5)
(turn= 0turn= 1) a0c06= 2(¬a1turn= 0c1= 2)a1c16= 2(¬a0turn= 1c0= 2) (turn= 0turn= 1)tour= 0tour= 1Impossible
Synchronization
Concurrent/Distributed algorithms
1.. .Lamport : barber, baker, . 2.Dekker’s algorithm forP0,P1,PN(Dijsktra 1968) 3.Peterson is simpler and can be generalised toNprocesses 4.? In temporal logic? With assertions By model checking Proofs ? (eg Lamport’s TLA) ? 5.Dekker’s algorithm is too complex 6.Dekker’s algorithm uses busy waiting 7.Fairness acheived because of fair scheduling
Need for higher constructs in concurrent programming.
Exercice 2Try to deﬁne fairness.
15
16
0 0 σ(e) =truehP, σi → hP , σi 0 0 hawaitedoP, σi → hP , σi
semantics
part)
release(s): If some process is suspended ons, wake it up Otherwises:=s+ 1.
σ(e) =true hwaite, σi → h, σi
Semaphores
19
Ageneralised semaphoresis integer variable with 2 operations
Operational
.
0 hP, σi → h, σi 0 hP;Q, σi → hQ, σi
0 0 hQ, σi → hQ , σi 0 0 hP||Q, σi → hP||Q , σi
20
σ[v/x](y) =σ(y)ify6=x
Exercice 3Other deﬁnition for semaphore : acquire(s): Ifs >0thens:=s1. Otherwise restart. release(s): Dos:=s+ 1.
Exercice 4Complete SOS foreandv Exercice 5Find SOS for boolean semaphores. Exercice 6Avoid spurious silent steps inif,whileand||.
.
0 0 hP, σi → hP , σi 0 0 hP||Q, σi → hP||Q, σi
h || , σi → h, σi
acquire(s): Ifs >0thens:=s1 Otherwise be suspended ons.
At beginning,s= 1. Then
Now mutual exclusion is easy :
σ[v/x](x) =v
σVariables7→Values
We write hP0, σ0i → hPn, σniwhenn0, + hP0, σ0i → hPn, σniwhenn >0.
18
(parallel
P, Q::=. . .|P||Q|waitb|awaitbdoP
.
Are these deﬁnitions equivalent ?
Semantics (SOS)
Language
::= ::=
P, Q e
Operational
σ(e) =false hwaite, σi → hwaitb, σi
0 0 hP, σi → hP , σi 0 0 hP;Q, σi → hP;Q, σi
0 (P6=)
σ(e) =true hifethenPelseQ, σi → hP, σi
hP0, σ0i → hP1, σ1i → hP2, σ2i → ∙ ∙ ∙ hPn, σni →
reductions
Remark that in our system, we have no rule such as
Ie no busy waiting. Reductions may block. (Same remark for awaitedoP).
Language
Semantics (SOS)
Notations
σ(e) =false hwhileedoP, σi → h, σi
SOS
skip|x:=e|ifbthenPelseQ|P;Q|whilebdoP|  expression
part)
(seq.
[∙ ∙ ∙;acquire(s);A;release(s);∙ ∙ ∙]||[∙ ∙ ∙;acquire(s);B;release(s);∙ ∙ ∙]
σ(e) =true hwhileedoP, σi → hP;whileedoP, σi
σ(e) =false hifethenPelseQ, σi → hQ, σi
semantics
hx:=e, σi → h, σ[σ(e)/x]i
hskip, σi → h, σi
17
.
.
.
Atomic
statements
Exercice 7If we make following extension
P, Q::=. . .| {P}
(Exercices)
what is the meaning of following rule ? +0 hP, σi → h, σi 0 h{P}, σi → h, σi
Exercice 8ShowawaitedoP≡ {waite;P}
Exercice 9Code generalized semaphores in our language.
Exercice 10Meaning of{do skipwhile true }? Find simpler equivalent statement.
Exercice 11Try to add procedure calls to our SOS semantics.
Producer
Consumer
21
22
.
A
typical
TYPE T <: ROOT; Mutex = MUTEX; Condition <: ROOT;
package.
Modula3
A Thread.T is a handle on a thread. A Mutex is locked by some thread, or unlocked. A Condition is a set of waiting threads. A newlyallocated Mutex is unlocked ; a newlyallocated Condition is empty. It is a checked runtime error to pass the NIL Mutex, Condition, or T to any procedure in this interface.
. PROCEDURE Acquire(m: Mutex);
Wait until m is unlocked and then lock it.
PROCEDURE Release(m: Mutex);
The calling thread must have m locked. Unlocks m.
PROCEDURE Wait(m: Mutex; c: Condition);
23
The calling thread must have m locked. Atomically unlocks m and waits on c. Then relocks m and returns.
PROCEDURE Signal(c: Condition);
One or more threads waiting on c become eligible to run.
All threads waiting on c become eligible to run.
24
.
.
Locks
A LOCK statement has the form :
LOCK mu DO S END
where S is a statement and mu is an expression. It is equivalent to :
WITH m = mu DO Thread.Acquire(m); TRY S FINALLY Thread.Release(m) END END
where m stands for a variable that does not occur in S.
A statement of the form :
Try
TRY S_1 FINALLY S_2 END
Finally
25
executes statementS1and then statementS2. If the outcome ofS1is normal, the TRY statement is equivalent toS1;S2. If the outcome ofS1 is an exception and the outcome ofS2is normal, the exception fromS1 is reraised afterS2is executed. If both outcomes are exceptions, the outcome of the TRY is the exception fromS2.
26
.
.
Concurrent
Popping in a stack :
stack
Pushing into a stack :
LOCK m DO p = newElement(v, p); Thread.Signal (nonEmpty); END;
Caution :WHILEis safer thanIFin Pop.
Concurrent
table
VAR table := ARRAY [0..999] of REFANY {NIL, ...}; VAR i:[0..1000] := 0;
PROCEDURE Insert (r: REFANY) = BEGIN IF r <> NIL THEN
table[i] := r; i := i+1;
END; END Insert;
Exercice 12Complete previous program to avoid lost values.
27
28
.
.
Simple stragegy for semaphore controls
Respect a partial order between semaphores. For example,AandBuses m1andm2in same order.
Conditions
and
semaphores
Semaphores are stateful ; conditions are stateless.
Wait (m, c) : release(m); acquire(csem); acquire(m);
Signal (c) : release(csem);
Exercice 13?Is this translation correct Exercice 14What happens inWaitandSignalif it does not atomically unlockmand wait onc.
29
30
.
Exercices
Exercice 15Readers and writers. A buﬀer may be read by several processes at same time. But only one process may write in it. Write procedures StartRead, EndRead, StartWrite, EndWrite.
Exercice 16Give SOS for operations on conditions.
31