concurrency sharing ressource

Description

. .Readers and Writers (1/6)Concurrency 2A shared resource is concurrently read or modified.From shared memory• Several processes may concurrently read the shared resource.to synchronization• A single process (the writer) may modify the resource.• When readers are running, no writer can be executed.by communication on• When a writer is running, no other writer, nor a reader can runchannelsconcurrently.PROCEDURE Read() = PROCEDURE Write() =Jean-Jacques L´evy (INRIA - Rocq)BEGIN BEGINAcquireShared(); AcquireExclusive();MPRI concurrency course with :(∗ read shared data ∗) (∗ write shared data ∗)ReleaseShared(); ReleaseExclusive();Pierre-Louis Curien (PPS)END Read; END Write;Eric Goubault (CEA)James Leifer (INRIA - Rocq)Catuscia Palamidessi (INRIA - Futurs)1 3. .Les lecteurs et les ´ecrivains (2/6)PlanEn lecture, on a nReaders simultan´es (nReaders > 0).• exercises (followup)En ´ecriture, on a nReaders =−1.• readers and writersPROCEDURE AcquireShared() = PROCEDURE AcquireExclusive() =BEGIN BEGIN• the five philosophersLOCK m DO LOCK m DOWHILE nReaders = −1 DO WHILE nReaders != 0 DO• synchronous communication channelsThread.Wait(m, c); Thread.Wait(m, c);• CML END; END;++ nReaders; nReaders := −1;• coding semaphoresEND; END;END AcquireShared;END AcquireExclusive;PROCEDURE ReleaseShared() = PROCEDURE ReleaseExclusive() =BEGIN BEGINLOCK m DO LOCK m DO−− nReaders;nReaders := 0;IF nReaders = 0 THENThread.Broadcast(c);END;Thread ...

Informations

• Publié par: Sies
• Nombre de lectures: 21
• Langue: Français

Extrait

.

.

Concurrency 2

From shared memory to synchronization by communication on channels

JeanJacquesL´evy(INRIARocq)

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

Plan

exercises (followup) readers and writers the five philosophers synchronous communication channels CML coding semaphores

1

2

.

Readers and Writers (1/6)

A shared resource is concurrentlyreadormodified. Several processes may concurrently read the shared resource. A single process (the writer) may modify the resource. When readers are running, no writer can be executed. When a writer is running, no other writer, nor a reader can run concurrently.

PROCEDURERead() = BEGIN AcquireShared(); (∗read shared data∗) ReleaseShared(); ENDRead;

PROCEDUREWrite() = BEGIN AcquireExclusive(); (∗write shared data∗) ReleaseExclusive(); ENDWrite;

3

. Leslecteursetlese´crivains(2/6) Enlecture, on anReaders(sesulimn´tanReaders>0). En´ecriture, on anReaders=−1. PROCEDUREAcquireShared() = PROCEDUREAcquireExclusive() = BEGIN BEGIN LOCKmDO LOCK mDO WHILEnReaders =−1DO WHILE nReaders != 0DO Thread.Wait(m, c); Thread.Wait(m, c); END; END; ++ nReaders; nReaders :=−1; END; END; ENDAcquireShared; ENDAcquireExclusive; PROCEDUREReleaseShared() = PROCEDUREReleaseExclusive() = BEGIN BEGIN LOCKmDO LOCK mDO −− := 0; nReaders; nReaders IFnReaders = 0THEN Thread.Broadcast(c) ; Thread.Signal(c); END; END: ENDReleaseExclusive; ENDReleaseShared;

4

. Leslecteursetles´ecrivains(3/6) Broadcastntmeteiaimntedm´trrevaoussecessudpororpeeveilletr´ bloque´s.AvecdeuxconditionscRetcW,onauncontroˆleplusfin: PROCEDUREAcquireShared() = PROCEDUREAcquireExclusive() = BEGIN BEGIN LOCKm DO LOCKmDO ++ nWaitingReaders; WHILEnReaders != 0DO WHILEnReaders =−1DO Thread.Wait(m, cW); Thread.Wait(m, cR); END; END ; nReaders:=−1; −−nWaitingReaders; END; ++ nReaders; ENDAcquireExclusive; END; ENDAcquireShared; PROCEDUREReleaseExclusive() = BEGIN PROCEDUREReleaseShared() = LOCKmDO BEGIN nReaders := 0; LOCKm DO IFnWaitingReaders>0THEN −−nReaders; Thread.Broadcast(cR) ; IFnReaders = 0THEN ELSE Thread.Signal(cW); Thread.Signal(cW) ; END: END; ENDReleaseShared; ENDReleaseExclusive;

5

. Leslecteursetles´ecrivains(4/6) Exe´cutersignalnoittirceuqise’nastp`etrfficsee.acl’in`asece’dnueiru´tre Avecunseulprocesseur,cen’estpasunproble`mecarlesre´veill´es passentdansl’e´tatprˆetattendantladisponibilit´eduprocesseur.

Avecplusieursprocesseurs,leprocessusre´veill´epeutretomber rapidementdansl’´etatbloqu´e,tantqueleverroun’estpasrelache´.

Il vaut mieux fairesignalla`reuire´txe’de la section critique. (Ce qu’on ne fait jamais! !)

PROCEDUREReleaseShared() = BEGIN VARdoSignal:BOOLEAN; LOCKmDO −−nReaders; doSignal := nReaders = 0; END: IFdoSignalTHEN Thread.Signal(cW) ; ENDReleaseShared;

6

. Leslecteursetlese´crivains(5/6) Des blocages inutiles sont possibles (avec plusieurs processeurs) sur le Broadcastuter.efid’´ndriec Comme avant, on peut le sortir de la section critique. Siplusieurslecteurssontre´veille´s,un seulprend le verrou. Mieux vaut fairesignalirce´’dniup,erutreaiefsrenfisignalespartagfind’acc`ee´n pour relancer les autres lecteurs.

PROCEDUREAcquireShared() = BEGIN LOCKmDO ++ nWaitingReaders; WHILEnReaders =−1DO Thread.Wait(m, cR); END; −−nWaitingReaders; ++ nReaders; END; Thread.Signal(cR); ENDAcquireShared;

PROCEDUREReleaseExclusive() = BEGIN LOCKmDO nReaders := 0; IFnWaitingReaders>0THEN Thread.Signal(cR) ; ELSE Thread.Signal(cW) ; END; ENDReleaseExclusive;

. Leslecteursetlese´crivains(6/6) Faminepossiblerivan´ecdu’inen attente de fin de lecture. La politique d’ordonnancement des processus peut aider. On peut aussi logiquement imposerlepassaged’un´ecrivain.

PROCEDUREAcquireShared() = BEGIN LOCKmDO ++ nWaitingReaders; IFnWaitingWriters>0THEN Thread.Wait(m, cR); WHILEnReaders =−1DO Thread.Wait(m, cR); END; −−nWaitingReaders; ++ nReaders; END; Thread.Signal(cR); ENDAcquireShared;

PROCEDUREAcquireExclusive() = BEGIN LOCKmDO ++nWaitingWriters; WHILEnReaders != 0DO Thread.Wait(m, cW); END; −−nWaitingWriters; nReaders :=−1; END; ENDAcquireExclusive;

Controˆlerfinementlasynchronisationpeuteˆtrecomplexe.

7

8

.

.

Les 5 philosophes (1/7)

bo`lrPeemed[Dijkstra]pour tester les primitives concurrentes : verrous,conditions,s´emaphores,se´maphoresg´ene´ralise´s,etc. 5 moines philosophesΦ i pensent et mangent. Pour manger, ils vontdanslasallecommune,ou`ilsd´egustentunplatdespaghettis. il fautdeuxfourchettes pour manger les spaghettis. Mais, le monast`erenedisposequede5fourchettes.

feia?mcunmoinenemeured`revirraua’uqecantmeomC

Les 5 philosophes (2/7)

(∗–————noitul————erP–e`imoser——∗) VARs:ARRAY[0..4]OF MUTEX; PROCEDUREPhilosophe (i:CARDINAL) = BEGIN (∗penser∗) Thread.Acquire(s[i]); Thread.Acquire(s[(i+1)MOD5]); (∗manger∗) Thread.Release(s[i]); Thread.Release(s[(i+1)MOD5]); ENDPhilosophe; Surete´,maisinterblocage.

9

10

.

.

Les 5 philosophes (3/7)

(∗——————eu–D`exiosemitul——no–——∗)

VARf:ARRAY0..4OF CARDINAL={2, 2, 2, 2, 2}; manger:ARRAY0..4OFThread.Condition;

PROCEDUREPhilosophe (i:CARDINAL) = BEGIN WHILEtrueDO (∗penser∗) PrendreFourchettes(i); (∗manger∗) RelacherFourchettes(i); END; ENDPhilosophe;

f[i]est le nombre de fourchettes disponibles pourΦ i

Les 5 philosophes (4/7)

PROCEDUREPrendreFourchettes (i:CARDINAL) = BEGIN LOCKmDO WHILEf[i] != 2DO Thread.Wait (m, manger[i]); END; −−f[(i−1)MOD5];−−f[(i+1)MOD5]; END: ENDPrendreFourchettes;

PROCEDURERelacherFourchettes (i:CARDINAL) = BEGIN VARg := (i−1)MOD5, d := (i+1)MOD5; LOCKmDO ++ f[g]; ++ f[d]; IFf[d] = 2THEN Thread.Signal (manger[d]); IFf[g] = 2THEN Thread.Signal (manger[g]); END; ENDRelacherFourchettes;

11

12

.

.

Les 5 philosophes (5/7)

v´erifi´eivantestraaitnusLi’vn 4 X f[i] = 10−2×mangeurs i=0

interblocage⇒mangeurs= 0 ⇒f[i] = 2pour touti(0≤i <5) ⇒pasd’intebrolacegopruelediernadr`anemr`denama.reg famine, si, par exemple, les philosophes 1 et 3 complottent contre le philosophe 2, qui mourra de faim.

Les 5 philosophes (6/7)

13

oinperndnerOeserutolprlai`em+s´emaphore g´en´eralis´esalle Aude´butsalle= 4 Pour manger, les philosophes rentrent dans la salle; ;il y a au plus 4 philosophes dans la salle s;ella`rpaelseaperlsirtsotdenasel et retournent penser dans leur cellule. (∗ontilusome`esioirT–——————–————∗) PROCEDUREPhilosophe (i:CARDINAL) = BEGIN (∗penser∗) SemaphoreGen.P(salle) ;(∗—onecqruiet—i—d´ebutz——∗) Thread.Acquire(s[i]); Thread.Acquire(s[(i+1)MOD5]); (∗manger∗) Thread.Release(s[i]); Thread.Release(s[(i+1)MOD5]); SemaphoreGen.V(salle) ;(∗——— fin zone critique ——–∗) ENDPhilosophe;

14

.

.

Les 5 philosophes (7/7) 4 philosophes au plus dans la salle⇒pas d’interblocage. ire´e´finlt’vatvvaeisnanriuits salle+nombre de processus dans la zone critique= 4

SiΦ i nfilisrola,)]i[s(ePutecx´eoi.nructinstetteirac SiΦ i (is[)%+1),5]orale´dnminfistne(PruneidattsΦ i+1 attend inde´finimentsurP(s[(i+2)%5]). SiΦ i (sePutec%51)i+[(´xeinstetteion.ructolsr)]a,ricalinfi ⇒Pas de famine.

Exercice 1 Programmer cette solution des 5 philosophes avec les seuls Thread.Wait, Thread.Signal et Thread.Broadcast.

Communication channels (1/2) shared memory is not structured (see Ariane 502 onboard software)⇒restricted communication between processes network of processes channels as FIFOs[Kahn, Macqueen] eg Eratosthenes sieve

15

16

.

.

Communication channels (2/2) channels just contains scalars communication by rendezvous (Occam, Ada, etc) in 0 0 [P;send(c, x);P]||[Q;receive(c);Q] PandQget synchronized by the communication onc. 0 ThenQandQmay start concurrently. basic model⇒CSP[Hoare, 78], CCS[Milner, 80],πcalcul [Milner, Parrow, Walker, 90], CCS andπcalculus are easily implementable on top of shared memory. Much more difficult for distributed environments, since one has to fight with the global consensus problem. See at end of MPRI concurrency course. ⇒joincalculus[Fournet, Gonthier, 96],π1calculus[Amadio, 97], nomadicpic[Sewell, Wojciechowski, 00]. ., .polyphonic C#[MSR, 03].

Concurrent ML

The Event library in Ocaml implements[Reppy]SML library.

sig type’a channel valnew_channel : unit > ’a Event.channel type’a event valsend : ’a Event.channel > ’a > unit Event.event valreceive : ’a Event.channel > ’a Event.event valchoose : ’a Event.event list > ’a Event.event valwrap : ’a Event.event > (’a > ’b) > ’b Event.event valguard : (unit > ’a Event.event) > ’a Event.event valsync : ’a Event.event > ’a valselect : ’a Event.event list > ’a ... end

17

18

. Updatable storage cell (1/4) openEvent;; type’a request = GET | PUTof’a;; type’a cell = { reqCh: ’a request channel; replyCh: ’a channel; } ;; letsend1 c msg = sync (send c msg) ;; letreceive1 c = sync (receive c) ;;

letgetc = send1 c.reqCh GET; receive1 c.replyCh ;; letputc x = send1 c.reqCh (PUT x) ;;

letcellx = letreqCh = new_channel()in letreplyCh = new_channel()in let recloop x =match(receive1 reqCh)with GET > send1 replyCh x ; loop x | PUT x’ > loop x’ in Thread.create loop x ; {reqCh = reqCh; replyCh = replyCh} ;;

. Updatable storage cell (2/4) openEvent;;

type’a cell = { getCh: ’a channel; putCh: ’a channel; } ;;

letget c = sync (receive c.getCh);;

letput c x = sync (send c.putCh x);;

letcell x = letgetCh = new_channel()in letputCh = new_channel()in let recloop x = select [ wrap (send getCh x) (function() > loop x); wrap (receive putCh) loop ] in Thread.create loop x ; {getCh = getCh; putCh = putCh} ;;

19

20

. Updatable storage cell (3/4) openEvent;;

.

type’a sem = { getCh: ’a channel; putCh: ’a channel; } ;;

letget c = sync (receive c.getCh);; letput c x = sync (send c.putCh x);;

letsem () = letgetCh = new_channel()in letputCh = new_channel()in let recloop x = letputEvt = wrap (receive putCh) (functiony > loop (Some y))in matchxwith None > sync putEvt | Some y > letgetEvt = wrap (send getCh y) (function() > loop x)in select [ getEvt; putEvt ] in Thread.create loop None ; {getCh = getCh; putCh = putCh} ;;

Updatable storage cell (4/4)

loop(None) =Put(y)∙loop(Somey) loop(Somey) =Gethyi ∙loop(None) +Put(z)∙loop(Somez)

def Sem(x) =loop(Somex)

⇓

Sem(x) =Get∙Put(y)∙Sem(y) +Put(y)∙Sem(y)

21

Exercice 2 Give a program and equations for generalized semaphores.

22

. Conclusion ?What are the equations of interactions Simplify by considering just interaction. Find a logic for interaction. Is there an interesting denotational semantics? Find new/correct paradigms for programming. What’s about distribution? Mobility ? Security ?

⇒ next lectures in MPRI Concurrency  course.

23