Planche 1
Concurrency 1
Shared Memory
Jean-Jacques Lévy (INRIA - Rocq)

MPRI concurrency course with:
Pierre-Louis Curien (PPS)
Eric Goubault (CEA)
James Leifer (INRIA - Rocq)
Catuscia Palamidessi (INRIA - Futurs)

 Planche 2

## 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
S=
N
b*N + (1-b)
(S = speedup, b = sequential part, N processors)

 Planche 3

## MPRI concurrency course

 09-30 JJL shared memory atomicity, SOS 10-07 JJL shared memory readers/writers, 5 philosophers 10-12 PLC 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-16 JL p-calculussyntax, lts, examples, strong bisim. 11-25 JL p-calculusred. semantics, weak bisim., congruence 12-02 JL p-calculusextensions for mobility 12-09 JL/CP p-calculusencodings: l-calculus, arithm., lists 12-16 CP p-calculusexpressivity 01-06 CP p-calculusstochastic models 01-13 CP p-calculussecurity 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-concurrency-2004/
 Planche 4

## Concurrency Þ non-determinism

Suppose x is a global variable. At beginning, x=0

Consider
S = [x := 1; ]
T = [x := 2; ]

After S
|| T, then x Î {1,2}

Conclusion:
Result is not unique.

Concurrent programs are not described by functions.

 Planche 5

## Implicit Communication

Suppose x is 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 ]
After S, then x Î {2,3,4}
After T, then x Î {3,4}
T may be blocked

Conclusion

In S and T, interaction via x

 Planche 6

## Input-output behaviour

Suppose x is a global variable.

Consider
S = [x := 1 ]
T = [x := 0; x := x+1 ]

S and T same functions on memory state.

But S
|| S and T || S are different ``functions'' on memory state.

Þ Interaction is important.

A process is an ``atomic'' action, followed by a process. Ie.
P » Null +  2action× P

Part of the concurrency course gives sense to this equation.

 Planche 7

## Atomicity

Suppose x is a global variable. At beginning, x=0

Consider
S = [x := x+1
|| x := x+1]

After S, then x=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]

After S, then x Î {1,2}.

Conclusion
1. [x := x+1] was firstly considered atomic
2. Atomicity is important
 Planche 8

## Critical section -- Mutual exclusion

Let P0 = [···; C0; ···] and P1 = [···; C1; ···]

C
0 and C1 are critical sections (ie should not be executed simultaneously).

Solution 1 At beginning, turn = 0.
 P0 : ···   while turn != 0 do     ;   C0;   turn := 1;   ··· P1 : ···   while turn != 1 do     ;   C1;   turn := 0;   ···

P
0 privileged, unfair.

 Planche 9

## Critical section -- Mutual exclusion

Solution 2 At beginning, a0 = a1 = false .
 P0 : ···   while a1 do     ;   a0 := true;   C0;   a0 := false;   ··· P1 : ···   while a0 do     ;   a1 := true;   C1;   a1 := false;   ···

False.

Solution 3 At beginning, a
0 = a1 = false .
 P0 : ···   a0 := true;   while a1 do     ;   C0;   a0 := false;   ··· P1 : ···   a1 := true;   while a0 do     ;   C1;   a1 := false;   ···

Deadlock. Both P0 and P1 blocked.
 Planche 10

## Dekker's Algorithm (CACM 1965)

At beginning, a0 = a1 = false , turnÎ{0,1}
 P0 : ···   a0 := true;   while a1 do     if turn != 0 begin       a0 := false;       while turn != 0 do         ;       a0 := true;     end;   C0;   turn := 1; a0 := false;   ··· P1 : ···   a1 := true;   while a0 do     if turn != 1  begin       a1 := false;       while turn != 1 do         ;       a1 := true;     end;   C1;   turn := 0; a1 := false;   ···

Exercice 1 Trouver Dekker pour n processus [Dijkstra 1968].

 Planche 11

## Peterson's Algorithm (IPL June 81) (1/5)

At beginning, a0 = a1 = false , turnÎ{0,1}
 P0 : ···   a0 := true;   turn := 1;   while a1 && turn != 0 do     ;   C0;   a0 := false;   ··· P1 : ···   a1 := true;   turn := 0;   while a0 && turn != 1 do     ;   C1;   a0 := false;   ···

 Planche 12

## Peterson's Algorithm (IPL June 81) (2/5)

c0, c1 program counters for P0 and P1.
At beginning c
0 = c1 = 1
 ···       {¬ a0 Ù c0¹ 2 } 1    a0 := true; c0 := 2;       {a0 Ù c0 = 2} 2    turn := 1; c0 := 1;       {a0 Ù c0 ¹ 2} 3    while a1 && turn != 0 do .      ;       {a0 Ù c0¹ 2 Ù (¬ a1 Ú turn= 0 Ú c1 = 2)} .    C0; 5    a0 := false;       {¬ a0Ù c0¹ 2}      ··· ··· {¬ a1 Ù c1¹ 2 } a1 := true; c1 := 2; {a1 Ù c1 = 2} turn := 0; c1 := 1; {a1 Ù c1 ¹ 2} while a0 && turn != 1 do   ; {a1 Ù c1¹ 2 Ù (¬ a1 Ú turn= 1 Ú c0 = 2)} C1; a1 := false; {¬ a1Ù c1¹ 2} ···

 Planche 13

## Peterson's Algorithm (IPL June 81) (3/5)

 (turn= 0 Ú turn= 1) Ù a0  Ù  c0¹ 2  Ù  (¬ a1 Ú turn= 0 Ú c1 = 2) Ù a1  Ù  c1¹ 2  Ù  (¬ a0 Ú turn= 1 Ú c0 = 2) º (turn= 0 Ú turn= 1) Ù tour = 0 Ù tour = 1 Impossible

 Planche 14

## Peterson's Algorithm (IPL June 81) (4/5)

c0, c1 program counters for P0 and P1.
At beginning c
0 = c1 = 1
 ···       {¬ a0 Ù c0¹ 2 } 1    a0 := true; c0 := 2;       {a0 Ù c0 = 2} 2    turn := 1; c0 := 1;       {a0 Ù c0 ¹ 2} 3    while a1 && turn != 0 do .      ;       {a0 Ù c0¹ 2 Ù (¬ a1 Ú turn= 0 Ú c1 = 2)} .    C0; 5    a0 := false;       {¬ a0Ù c0¹ 2}      ··· ··· {¬ a1 Ù c1¹ 2 } a1 := true; c1 := 2; {a1 Ù c1 = 2} turn := 0; c1 := 1; {a1 Ù c1 ¹ 2} while a0 && turn != 1 do   ; {a1 Ù c1¹ 2 Ù (¬ a1 Ú turn= 1 Ú c0 = 2)} C1; a1 := false; {¬ a1Ù c1¹ 2} ···

 Planche 15

## Peterson's Algorithm (IPL June 81) (5/5)

 (turn= 0 Ú turn= 1) Ù a0  Ù  c0¹ 2  Ù  (¬ a1 Ú turn= 0 Ú c1 = 2) Ù a1  Ù  c1¹ 2  Ù  (¬ a0 Ú turn= 1 Ú c0 = 2) º (turn= 0 Ú turn= 1) Ù tour = 0 Ù tour = 1 Impossible

 Planche 16

## Synchronization

Concurrent/Distributed algorithms
1. Lamport: barber, baker, ...
2. Dekker's algorithm for P0, P1, PN (Dijsktra 1968)
3. Peterson is simpler and can be generalised to N processes
4. Proofs ? By model checking ? With assertions ? In temporal logic (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.

 Planche 17

## Semaphores

A generalised semaphore s is integer variable with 2 operations

acquire(s): If s > 0 then s := s-1
Otherwise be suspended on s.

release(s): If some process is suspended on s, wake it up
Otherwise s := s+1.

Now mutual exclusion is easy:

At beginning, s = 1. Then
[···; acquire(s) ;  A;   release(s); ···]  ||  [···; acquire(s) ;  B;   release(s); ···]

Exercice 3 Other definition for semaphore:
 acquire(s): If s > 0 then s := s-1. Otherwise restart. release(s): Do s := s+1.

Are these definitions equivalent?
 Planche 18

## Operational semantics (seq. part)

Language
 P,Q ::= skip  | x := e |  if  b  then  P  else  Q | P;Q | while  b  do  P | · e ::= expression

Semantics (SOS)
á skip ,  s ñ ® á ·s ñ á x := es ñ ® á ·s[s(e)/x] ñ
s(e) = true
á  if  e  then  P  else  Qs ñ ® á Ps ñ
s(e) = false
á  if  e  then  P  else  Qs ñ ® á Qs ñ
á Ps ñ ® á P',  s' ñ
á P;Qs ñ ® á P';Qs' ñ
(P' ¹ ·)
á Ps ñ ® á ·s' ñ
á P;Qs ñ ® á Qs' ñ
s(e) = true
á while  e  do  Ps ñ ® á P;while  e  do  Ps ñ
s(e) = false
á while  e  do  Ps ñ ® á ·s ñ

s Î Variables
|® Values s[v/x](x) = v s[v/x](y) = s(y) if y ¹ x
 Planche 19

## Operational semantics (parallel part)

Language
P,Q ::= ... | P || Q |  wait  b | await  b  do  P

Semantics (SOS)
á Ps ñ ® á P',  s' ñ
á P || Qs ñ ® á P' || Qs' ñ
á Qs ñ ® á Q',  s' ñ
á P || Qs ñ ® á P || Q',  s' ñ
á · || ·s ñ ® á ·s ñ
s(e) = true
á  wait  es ñ ® á ·s ñ
s(e) = true  á Ps ñ ® á P',  s' ñ
á await  e  do  Ps ñ ® á P',  s' ñ

Exercice 4 Complete SOS for e and v
Exercice 5 Find SOS for boolean semaphores.
Exercice 6 Avoid spurious silent steps in  if , while  and
||.
 Planche 20

## SOS reductions

Notations
á P0s0 ñ ® á P1s1 ñ ® á P2s2 ñ ® ··· á Pnsn ñ ®

We write
 á P0,  s0 ñ ®* á Pn,  sn ñ when n ³ 0, á P0,  s0 ñ ®+ á Pn,  sn ñ when n > 0.

Remark that in our system, we have no rule such as
s(e) = false
á  wait  es ñ ® á  wait  bs ñ

Ie no busy waiting. Reductions may block. (Same remark for await  e  do  P).
 Planche 21

## Atomic statements (Exercices)

Exercice 7 If we make following extension
P,Q ::= ... | { P }
what is the meaning of following rule?
á Ps ñ ®+ á ·s' ñ
á {P},  s ñ ® á ·s' ñ

Exercice 8 Show await  e  do  P ºwait  e; P }

Exercice 9 Code generalized semaphores in our language.

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

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

 Planche 22

## Producer - Consumer

 Planche 23

## A typical thread package. Modula-3

```

TYPE
T <: ROOT;
Mutex = MUTEX;
Condition <: ROOT;
```
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.
 Planche 24
```
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);
```
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.

 Planche 25

## 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
TRY S FINALLY Thread.Release(m) END
END
```
where m stands for a variable that does not occur in S.

 Planche 26

## Try Finally

A statement of the form:
```
TRY S_1 FINALLY S_2 END
```
executes statement S1 and then statement S2. If the outcome of S1 is normal, the TRY statement is equivalent to S1;S2. If the outcome of S1 is an exception and the outcome of S2 is normal, the exception from S1 is re-raised after S2 is executed. If both outcomes are exceptions, the outcome of the TRY is the exception from S2.

 Planche 27

## Concurrent stack

Popping in a stack:
```
VAR nonEmpty := NEW(Thread.Condition);

LOCK m DO
WHILE p = NIL DO Thread.Wait(m, nonEmpty) END;
p := p.next;
END;
```
Pushing into a stack:
```
LOCK m DO
p = newElement(v, p);
END;
```
Caution: `WHILE` is safer than `IF` in Pop.

 Planche 28

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

 Planche 29

Thread A locks mutex m1
Thread B locks mutex m
2
Thread A trying to lock m
2
Thread B trying to lock m
1

Simple stragegy for semaphore controls

Respect a partial order between semaphores. For example, A and B uses m
1 and m2 in same order.

 Planche 30

## 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 in Wait and Signal if it does not atomically unlock m and wait on c.

 Planche 31

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

This document was translated from LATEX by HEVEA.