Planche 1

Concurrency 1
Shared Memory
Jean-Jacques Lévy
jeanjacqueslevy.net/dea

Planche 2

Why concurrency?

Programs for multi-processors
Drivers for slow devices
Human users are concurrent
Distributed systems with multiple clients
Reduce lattency
Increase efficiency, but Amdahl's law

S=

N

b*N + (1-b)

(S = speedup, b = sequential part, N processors)

Planche 3

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 (shared memory)

Planche 4

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

[x := x+1] was firstly considered atomic
Atomicity is important

Planche 5

Critical section -- Mutual exclusion

Let P₀ = [···; C₀; ···] and P₁ = [···; C₁; ···]

C₀ and C₁ are critical sections (ie should not be executed simultaneously).

Solution 1 At beginning, turn = 0.

P0 : ··· while turn != 0 do ; C₀; turn := 1; ···

P1 : ··· while turn != 1 do ; C₁; turn := 0; ···

P₀ privileged, unfair.

Planche 6

Critical section -- Mutual exclusion

Solution 2 At beginning, a₀ = a₁ = false .

P0 : ··· while a1 do ; a0 := true; C₀; a0 := false; ···

P1 : ··· while a0 do ; a1 := true; C₁; a1 := false; ···

False.

Solution 3 At beginning, a₀ = a₁ = false .

P0 : ··· a0 := true; while a1 do ; C₀; a0 := false; ···

P1 : ··· a1 := true; while a0 do ; C₁; a1 := false; ···

Deadlock. Both P₀ and P₁ blocked.

Planche 7

Dekker's Algorithm (CACM 1965)

At beginning, a₀ = a₁ = false , turnÎ{0,1}

P0 : ··· a0 := true; while a1 do if (turn != 0) { a0 := false; while (turn != 0) ; a0 := true; } C₀; turn := 1; a0 := false; ···

P1 : ··· a1 := true; while a0 do if (turn != 1) { a1 := false; while (turn != 1) ; a1 := true; } C₁; turn := 0; a1 := false; ···

Planche 8

Peterson's Algorithm (IPL June 81)

At beginning, a₀ = a₁ = false , turnÎ{0,1}

P0 : ··· a0 := true; turn := 1; while a1 && turn != 0 do ; C₀; a0 := false; ···

P1 : ··· a1 := true; turn := 0; while a0 && turn != 1 do ; C₁; a0 := false; ···

Planche 9

Synchronization

Concurrent/Distributed algorithms

Lamport: barber, baker, ...
Dekker's algorithm for P₀, P₁, P_N (Dijsktra 1968)
Peterson is simpler and can be generalised to N processes
Proofs ? By model checking ? With assertions ? In temporal logic (eg Lamport's TLA)?
Dekker's algorithm is too complex
Dekker's algorithm uses busy waiting
Fairness acheived because of fair scheduling

Need for higher constructs in concurrent programming.

Exercice 1 Try to define fairness.

Planche 10

Semaphores

A generalised semaphore s is integer variable with 2 operations

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

signal(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 P₁ || P₂ where
P₁ = [···; wait(s) ; A; signal(s); ···]
P₂ = [···; wait(s) ; B; signal(s); ···]

Planche 11

Operational (micro-)semantics (sequential 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 := e, s ñ ® á ·, s[s(e)/x] ñ

s(e) = true

á if e then P else Q, s ñ ® á P, s ñ

s(e) = false

á if e then P else Q, s ñ ® á Q, s ñ

á P, s ñ ® á P', s' ñ

á P;Q, s ñ ® á P';Q, s' ñ

(P' ¹ ·)

á P, s ñ ® á ·, s' ñ

á P;Q, s ñ ® á Q, s' ñ

s(e) = true

á while e do P, s ñ ® á P;while e do P, s ñ

s(e) = false

á while e do P, s ñ ® á ·, s ñ

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

Planche 12

Operational semantics (parallel part)

Language

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

Semantics (SOS)

á P, s ñ ® á P', s' ñ

á P || Q, s ñ ® á P' || Q, s' ñ

á Q, s ñ ® á Q', s' ñ

á P || Q, s ñ ® á P || Q', s' ñ

á · || ·, s ñ ® á ·, s ñ

s(b) = true

á wait b, s ñ ® á ·, s ñ

s(b) = true á P, s ñ ® á P', s' ñ

á await b do P, s ñ ® á P', s' ñ

s(b) = true á P, s ñ ® á ·, s' ñ

á await b do P, s ñ ® á ·, s' ñ

Exercice 2 Complete SOS for e and v
Exercice 3 Find SOS for boolean semaphores.
Exercice 4 Avoid spurious silent steps in if , while and ||.

Planche 13

SOS reductions

Notations

á P₀, s₀ ñ ® á P₁, s₁ ñ ® á P₂, s₂ ñ ® ··· á P_n, s_n ñ ®

We write

á P₀, s₀ ñ ®^* á P_n, s_n ñ when n ³ 0,

á P₀, s₀ ñ ®⁺ á P_n, s_n ñ when n > 0.

Remark that in our system, we have no rule such as

s(b) = false

á wait b, s ñ ® á wait b, s ñ

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

Planche 14

Atomic statements (Exercices)

Exercice 5 If we make following extension

P,Q ::= ... | { P }

what is the meaning of following rule?

á P, s ñ ®⁺ á ·, s' ñ

á {P}, s ñ ® á ·, s' ñ

Exercice 6 Show await b do P º { wait b; P }

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

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

Planche 15

Producer - Consumer

Planche 16

A typical thread package. Modula-3


INTERFACE Thread;

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 17


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 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 Broadcast(c: Condition);

All threads waiting on c become eligible to run.


PROCEDURE Signal(c: Condition);

One or more threads waiting on c become eligible to run.

Planche 18

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.

Planche 19

Try Finally

A statement of the form:


    TRY S_1 FINALLY S_2 END

executes statement S₁ and then statement S₂. If the outcome of S₁ is normal, the TRY statement is equivalent to S₁;S₂. If the outcome of S₁ is an exception and the outcome of S₂ is normal, the exception from S₁ is re-raised after S₂ is executed. If both outcomes are exceptions, the outcome of the TRY is the exception from S₂.

Planche 20

Concurrent stack

Popping in a stack:


VAR nonEmpty := NEW(Thread.Condition);

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

Pushing into a stack:


LOCK m DO
    newElement.next := head;
    head := newElement;
    Thread.Signal (nonEmpty);
END;

Caution: WHILE is safer than IF in Pop.

Planche 21

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

Planche 22

Deadlocks

Thread A locks mutex m₁
Thread B locks mutex m₂
Thread A trying to lock m₂
Thread B trying to lock m₁

Simple stragegy for semaphore controls

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

Planche 23

Exercices

Exercice 10 Simulate conditions with semaphores. Hint: count number of waiting processes on condition.

Exercice 11 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 12 Give SOS for operations on conditions.

This document was translated from L^AT_EX by H^EV^EA.