Concurrency : Shared memory atomicity

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

Informations

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

Extrait

.

.

Concurrency

Shared

1

Memory

JeanJacquesL´evy(INRIARocq)

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 efficiency, but Amdahl’s law

N S= b∗N+ (1−b) (S=speedup,b=sequential part,Nprocessors)

1

2

.

.

MPRI

concurrency

course

0930 JJL shared memory atomicity, SOS 1007 JJL shared memory readers/writers, 5 philosophers 1012PLC CCS choice, strong bisim. 1021 PLC CCS weak bisim., examples 1028 PLC CCS obs. equivalence, HennessyMilner logic 1104 PLC CCS examples of proofs 1116JLπcalculus syntax, lts, examples, strong bisim. 1125 JLπcalculus red. semantics, weak bisim., congruence 1202 JLπcalculus extensions for mobility 1209 JL/CPπcalculus encodings : λ calculus, arithm., lists 1216 CPπcalculus expressivity 0106 CPπcalculus stochastic models 0113 CPπcalculus security 0120 EG true concurrency concurrency and causality 0127 EG true concurrency Petri nets, events struct., async. trans. 0203 EG true concurrency other 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:= 2∗x]

T= [x:=x+ 1;x:=x+ 1||wait(x= 1);x:= 2∗x]

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 different “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 firstly considered atomic 2.Atomicity is important

Critical

section

–

Mutual

LetP 0 = [∙ ∙ ∙;C 0 ;∙ ∙ ∙]andP 1 = [∙ ∙ ∙;C 1 ;∙ ∙ ∙]

exclusion

C 0 andC 1 are critical sections (ie should not be executed simultaneously).

Solution 1At beginning,turn= 0.

P0 :∙ ∙ ∙ whileturn != 0do ; C 0 ; turn := 1; ∙ ∙ ∙ P 0 privileged, unfair.

P1 :∙ ∙ ∙ whileturn != 1do ; C 1 ; turn := 0; ∙ ∙ ∙

7

8

Mutual

1965)

(CACM

exclusion

P0 :∙ ∙ ∙ a0 :=true; turn := 1; whilea1 && turn != 0do ; C 0 ; a0 :=false; ∙ ∙ ∙

At beginning,a 0 =a 1 =false,turn∈ {0,1}

. Peterson’s

Algorithm

9

(IPL

Algorithm

Algorithm

Dekker’s

Solution 3At beginning,a 0 =a 1 =false. P0 :∙ ∙ ∙P1 :∙ ∙ ∙ a0 :=true:=; a1 true; whilea1do whilea0do ; ; C 0 ;C 1 ; a0 :=false:=; a1 false; ∙ ∙ ∙ ∙ ∙ ∙ Deadlock. BothP 0 andP 1 blocked.

Solution 2At beginning,a 0 =a 1 =false. P0 :∙ ∙ ∙P1 :∙ ∙ ∙ whilea1do whilea0do ; ; a0 :=true:=; a1 true; C 0 ;C 1 ; a0 :=false:=; a1 false; ∙ ∙ ∙ ∙ ∙ ∙ False.

June 81) (2/5)

11

∙ ∙ ∙ ∙ ∙ ∙ {¬a 0 ∧c 0 6= 2} {¬a 1 ∧c 1 6= 2} 1 a0 :=truea1 :=; c0 := 2; true; c1 := 2; {a 0 ∧c 0 = 2} {a 1 ∧c 1 = 2} 2 turn := 1; c0 := 1; turn := 0; c1 := 1; {a 0 ∧c 0 6= 2} {a 1 ∧c 1 6= 2} 3whilea1 && turn != 0do whilea0 && turn != 1do . ; ; {a0∧c 0 6= 2∧(¬a 1 ∨turn= 0∨c 1 = 2)} {a1∧c 1 6= 2∧(¬a 1 ∨turn= 1∨c 0 = 2)} .C 0 ;C 1 ; 5 a0 :=false:=; a1 false; {¬a 0 ∧c 0 6= 2} {¬a 1 ∧c 1 6= 2} ∙ ∙ ∙ ∙ ∙ ∙

12

June 81) (1/5)

10

P1 :∙ ∙ ∙ a1 :=true; whilea0do ifturn != 1 begin a1 :=false; whileturn != 1do ; a1 :=true; end; C 1 ; turn := 0; a1 :=false; ∙ ∙ ∙

.

(IPL

c 0 ,c 1 program counters forP 0 andP 1 . At beginningc 0 =c 1 = 1

At beginning,a 0 =a 1 =false,turn∈ {0,1}

P0 :∙ ∙ ∙ a0 :=true; whilea1do ifturn != 0 begin a0 := false; whileturn != 0do ; a0 :=true; end; C 0 ; turn := 1; a0 :=false; ∙ ∙ ∙

Exercice 1 Trouver Dekker pournprocessus[Dijkstra 1968].

. Peterson’s

P1 :∙ ∙ ∙ a1 :=true; turn := 0; whilea0 && turn != 1do ; C 1 ; a0 :=false; ∙ ∙ ∙

.

Critical

–

section

. Peterson’s

∧ ≡

Algorithm

(IPL

June 81) (3/5)

(turn= 0∨turn= 1) a 0 ∧c 0 6= 2∧(¬a 1 ∨turn= 0∨c 1 = 2)∧a 1 ∧c 1 6= 2∧(¬a 0 ∨turn= 1∨c 0 = 2) (turn= 0∨turn= 1)∧tour= 0∧tour= 1Impossible

. Peterson’s

Algorithm

c 0 ,c 1 program counters forP 0 andP 1 . At beginningc 0 =c 1 = 1

(IPL

13

June 81) (4/5)

∙ ∙ ∙ ∙ ∙ ∙ {¬a 0 ∧c 0 6= 2} {¬a 1 ∧c 1 6= 2} 1 a0 :=truea1 :=; c0 := 2; true; c1 := 2; {a 0 ∧c 0 = 2} {a 1 ∧c 1 = 2} 2 turn := 1; c0 := 1; turn := 0; c1 := 1; {a 0 ∧c 0 6= 2} {a 1 ∧c 1 6= 2} 3whilea1 && turn != 0do whilea0 && turn != 1do . ; ; {a0∧c 0 6= 2∧(¬a 1 ∨turn= 0∨c 1 = 2)} {a1∧c 1 6= 2∧(¬a 1 ∨turn= 1∨c 0 = 2)} .C 0 ;C 1 ; 5 a0 :=false; a1 :=false; {¬a 0 ∧c 0 6= 2} {¬a 1 ∧c 1 6= 2} ∙ ∙ ∙ ∙ ∙ ∙

14

. Peterson’s

.

∧ ≡

Algorithm

(IPL

June 81) (5/5)

(turn= 0∨turn= 1) a 0 ∧c 0 6= 2∧(¬a 1 ∨turn= 0∨c 1 = 2)∧a 1 ∧c 1 6= 2∧(¬a 0 ∨turn= 1∨c 0 = 2) (turn= 0∨turn= 1)∧tour= 0∧tour= 1Impossible

Synchronization

Concurrent/Distributed algorithms

1.. .Lamport : barber, baker, . 2.Dekker’s algorithm forP 0 ,P 1 ,P N (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 2 Try to define 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 3 Other definition for semaphore : acquire(s): Ifs >0thens:=s−1. Otherwise restart. release(s): Dos:=s+ 1.

Exercice 4 Complete SOS foreandv Exercice 5 Find SOS for boolean semaphores. Exercice 6 Avoid 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:=s−1 Otherwise be suspended ons.

At beginning,s= 1. Then

Now mutual exclusion is easy :

σ[v/x](x) =v

σ∈Variables7→Values

We write ∗ hP 0 , σ 0 i → hP n , σ n iwhenn≥0, + hP 0 , σ 0 i → hP n , σ n iwhenn >0.

18

(parallel

P, Q::=. . .|P||Q|waitb|awaitbdoP

.

Are these definitions 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

hP 0 , σ 0 i → hP 1 , σ 1 i → hP 2 , σ 2 i → ∙ ∙ ∙ hP n , σ n i →

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 7 If 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 8 ShowawaitedoP≡ {waite;P}

Exercice 9 Code generalized semaphores in our language.

Exercice 10 Meaning of{do skipwhile true }? Find simpler equivalent statement.

Exercice 11 Try to add procedure calls to our SOS semantics.

Producer



Consumer

21

22

.

A

typical

INTERFACE Thread;

thread

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.

PROCEDURE Broadcast(c: Condition);

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 statementS 1 and then statementS 2 . If the outcome ofS 1 is normal, the TRY statement is equivalent toS 1 ;S 2 . If the outcome ofS 1 is an exception and the outcome ofS 2 is normal, the exception fromS 1 is reraised afterS 2 is executed. If both outcomes are exceptions, the outcome of the TRY is the exception fromS 2 .

26

.

.

Concurrent

Popping in a stack :

VAR nonEmpty := NEW(Thread.Condition);

stack

LOCK m DO WHILE p = NIL DO Thread.Wait(m, nonEmpty) END; topElement := p.head; p := p.next; END; return topElement;

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 12 Complete previous program to avoid lost values.

27

28

.

.

Deadlocks

ThreadAlocks mutexm 1 ThreadBlocks mutexm 2 ThreadAtrying to lockm 2 ThreadBtrying to lockm 1

Simple stragegy for semaphore controls

Respect a partial order between semaphores. For example,AandBuses m 1 andm 2 in 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 14 What happens inWaitandSignalif it does not atomically unlockmand wait onc.

29

30

.

Exercices

Exercice 15 Readers and writers. A buffer may be read by several processes at same time. But only one process may write in it. Write procedures StartRead, EndRead, StartWrite, EndWrite.

Exercice 16 Give SOS for operations on conditions.

31