. .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 ...
From shared memory to synchronization by communication on channels
JeanJacquesL´evy(INRIARocq)
MPRI concurrency course with : PierreLouis 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 LOCKmDO WHILEnReaders =−1DO WHILEnReaders != 0DO Thread.Wait(m, c);Thread.Wait(m, c); END;END; ++ nReaders;nReaders :=−1; END;END; ENDAcquireShared;ENDAcquireExclusive; PROCEDUREReleaseShared() =PROCEDUREReleaseExclusive() = BEGIN BEGIN LOCKmDO LOCKmDO −−:= 0;nReaders; nReaders IFnReaders = 0THENThread.Broadcast(c) ; Thread.Signal(c);END; END:ENDReleaseExclusive; ENDReleaseShared;
. 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.
. 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.
bo`lrPeemed[Dijkstra]pour tester les primitives concurrentes : verrous,conditions,s´emaphores,se´maphoresg´ene´ralise´s,etc. 5 moines philosophesΦipensent et mangent. Pour manger, ils vontdanslasallecommune,ou`ilsd´egustentunplatdespaghettis. il fautdeuxfourchettes pour manger les spaghettis. Mais, le monast`erenedisposequede5fourchettes.
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Φinfilisrola,)]i[s(ePutecx´eoi.nructinstetteirac SiΦi(is[)%+1),5]orale´dnminfistne(PruneidattsΦi+1attend inde´finimentsurP(s[(i+2)%5]). SiΦi(sePutec%51)i+[(´xeinstetteion.ructolsr)]a,ricalinfi ⇒Pas de famine.
Exercice 1Programmer 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 onboard 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 rendezvous (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. ⇒joincalculus[Fournet, Gonthier, 96],π1calculus[Amadio, 97], nomadicpic[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) ;;
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);;
Exercice 2Give 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 ?