Semantiek & Correctheid Thread synchronisatie & communicatie

Semantiek & Correctheid Thread synchronisatie & communicatie

Naam:

Christian Gilissen (0342688) Maurice Samulski (0342319)

Datum: Versie:

30 juni 2004 2.5

Inhoudsopgave Inhoudsopgave ....................................................................................................................2 Inleiding ...............................................................................................................................3 Thread synchronisatie en communicatie .............................................................................4 Algemeen............................................................................................................. 4 Message Queues................................................................................................. 4 Mailboxes............................................................................................................. 5 Signals................................................................................................................. 5 Syntax & SOS semantiek van While....................................................................................6 Message Queues in While...................................................................................................8 Signals in While .................................................................................................................10 Race Conditions & Deadlocks ...........................................................................................12 Race Conditions ................................................................................................ 12 Deadlocks .......................................................................................................... 12 Message Queues versus Signals ......................................................................................15 While versus Signals .........................................................................................................20 While versus Message Queues .........................................................................................24 Gödel codering .................................................................................................. 24 Gödel codering : een element toevoegen .......................................................... 25 Gödel codering : een element uitlezen............................................................... 27 Conclusies .........................................................................................................................28 Referenties ........................................................................................................................29

Semantiek & Correctheid: Thread synchronisatie & communicatie

2/29

Inleiding Dit verslag is geschreven naar aanleiding van de opdracht “semantiek in het wild” voor het vak “Semantiek en Correctheid”. Het onderwerp van dit verslag is “synchronisatie en communicatie van threads” en beschouwt enkele bekende constructies voor het synchroniseren en communiceren van threads in combinatie met de taal While. • We vragen ons af wat er voor nodig is om de taal While uit te breiden met zogenaamde message queues en signals. • We vergelijken message queues met signals en vragen ons af of signals meerwaarde hebben ten opzichtte van message queues. • We bekijken de mogelijkheid om in While gebruik te maken van message queues zonder dat we de semantiek van While uitbreiden. We gebruiken een versie van While waarin threads worden geïmplementeerd met behulp van het “par” statement. We negeren zoveel mogelijk alle potentiële problemen van threads die voor ons niet van belang zijn. (Signals worden vaak gebruikt om deze te voorkomen). Omdat het par statement alleen in SOS kan worden uitgedrukt wordt er in dit verslag dan ook alleen gewerkt met SOS semantiek. Voor het lezen van dit verslag is er enige voorkennis van threads vereist.


3/29

Thread synchronisatie en communicatie Algemeen Threads zijn delen van programma’s die onafhankelijk en parallel aan andere stukken programma kunnen lopen. Een bekend probleem bij threads is de communicatie en synchronisatie ervan. Het is immers erg handig om meerdere threads aan een gezamenlijke taak te laten werken. Hierbij is het belangrijk dat threads elkaar niet in de weg lopen door bijvoorbeeld gedeelde data op verkeerde momenten te manipuleren. In principe zijn er twee dingen die we graag willen hebben: 1. we willen threads afhankelijk van elkaar taken laten uitvoeren (in een bepaalde volgorde). 2. we willen dat threads (op veilige wijze) data met elkaar kunnen delen. Om bovenstaande zaken te verwezenlijken zijn er in veel talen bepaalde constructies ontwikkeld. We zullen van deze constructies in dit verslag niet aantonen dat zij inderdaad deze zaken verwezenlijken.

Message Queues Message queues worden gebruikt om verschillende threads te synchroniseren en met elkaar te laten communiceren. Een message queue is een lijst waar een thread een waarde in kan zetten. Een andere thread (of dezelfde, maar dat is niet zo nuttig) kan deze waarde er weer uit halen. De waarde die er als eerste in werd gezet wordt er ook weer als eerste uit gehaald; het zogenaamde FIFO (First-In-First-Out) principe. Wanneer een thread dus gegevens van een andere thread nodig heeft zal hij in de message queue kijken of de gegevens al beschikbaar zijn. Als de gegevens niet beschikbaar zijn dan zal de thread wachten. Grafisch kan men een message queue als volgt weergeven:

message queue F I F O

thread receiving thread

sending thread

thread


4/29

Mailboxes Een mailbox is eigenlijk een eenvoudige message queue waarbij er slechts ruimte is voor 1 bericht. De message queue bevat dus precies 1 element. thread

thread

sending thread

receiving thread

mailbox

Signals Een mechanisme dat veel lijkt op message queues is “signals”. De term signals wordt in de literatuur voor velerlei verschillende zaken gebruikt. Wij verstaan onder “signals” het volgende mechanisme: • Een thread kan een signal versturen naar een andere thread. • De andere thread kan wachten op een bepaald signal. thread signal

receiving thread

sending thread

thread

De beschreven constructies komen het beste tot hun recht wanneer er lokale en globale variabele omgevingen zijn. Iedere thread heeft zijn eigen lokale variabele omgeving en er is een globale variabele omgeving waar alle threads aan kunnen.


5/29

Syntax & SOS semantiek van While De syntax van de taal While ziet er als volgt uit:

S ::= x := a | skip | S 1 ; S 2 | if b then S 1 else S 2 | while b do S De SOS semantiek van de taal While ziet er als volgt uit:

[ass sos]

x := a, s ⇒ s[x a A[| a |]s]

[skip sos]

skip, s ⇒ s

[comp ]

S 1, s ⇒ S '1, s ' S 1; S 2, s ⇒ S '1; S 2, s '

[comp

2

S 1, s ⇒ s ' S 1; S 2, s ⇒ S 2, s '

[if

tt

]

if b then S 1 else S 2, s ⇒ S 1, s

if B[| b |]s = tt

[if

ff

]

if b then S 1 else S 2, s ⇒ S 2, s

if B[| b |]s = ff

1

sos

sos

sos

sos

]

[while sos]

while b do S , s ⇒ if b then (S; while b do S ) else skip, s


6/29

Voor het gebruik van threads in While is er het “par” statement.

[par ] 1 sos

[par ] 2

sos

[par ] 3

sos

[par ] 4

sos

S 1, s ⇒ S 1' , s' S 1 par S 2, s ⇒ S 1' par S 2, s'

S 1, s ⇒ s ' S 1 par S 2, s ⇒ S 2, s' S 2, s ⇒ S 2 ' , s ' S 1 par S 2, s ⇒ S 1 par S 2' , s' S 2, s ⇒ s ' S 1 par S 2, s ⇒ S 1, s'


7/29

Message Queues in While Om een message queue te beschrijven moeten we eerst een datastructuur beschrijven waarin we meerdere waarden kunnen opslaan. Deze datastructuur moet werken volgens het FIFO principe. We noemen dit datatype een queue. We breiden de syntax van While uit met een queue declaratie:

S ::= ... | queue q Q Met

Q ::= ε | Q : a

Een queue zien we als een queue, gevolgd door een numerieke waarde, of als leeg. Volgens bovenstaande syntax kun je een queue declareren door: queue q1 :1:2:3 De semantiek van een queue declaratie ziet er als volgt uit:

queue q Q, s → s[q a Q] Queue variabelen worden gedeeld tussen threads. De verzamelingen van lokale variabelen voor threads zijn disjunct. We zullen deze declaratie in alle voorbeelden weglaten en aannemen dat de gebruikte queue al is toegevoegd aan de state. Queues hoeven nooit verwijderd te worden; we nemen aan dat ze bij beëindiging van het programma automatisch worden verwijderd. Om een element toe te voegen aan een queue introduceren we het volgende statement:

[pushsos]

push a q, s → s[| q a q : Α[| a |] s |]

Push heeft 2 parameters: de numerieke waarde die op de queue geplaatst moet worden en de naam van de queue waarop de waarde geplaatst moet worden. De waarde wordt achteraan op de queue geplaatst waardoor het geheel werkt als een FIFO. In de praktijk zou zo’n statement als volgt gebruikt kunnen worden: push 5 q1


8/29

Om elementen van de queue af te halen introduceren we de pop functie. We gebruiken hier (a:q) als notatie voor een queue waarvan het eerste element (de head) a is en de rest (de tail) q is.

[pop

not_empty

sos

〈 pop q x, s〉 → s [(a : q) a q ][x a a ]

]

Pop heeft 2 argumenten. Het eerste argument is de naam van de queue waar we een element af willen halen. Het 2e argument is een variabele waaraan de waarde die we van de queue halen aan zal worden toegekend. Wanneer de queue niet leeg is verwijderd pop het eerste item op de queue. Bijvoorbeeld: pop q1 c Waarna variabele c de waarde van het eerste element op de queue (q1) heeft gekregen en dat eerste element van de queue is verwijderd. Wanneer de queue wel leeg is wordt er gewacht tot er een element op de queue komt.

[pop

empty

sos

]

〈 pop q x, s〉 → 〈 pop q x, s〉

if q = ε

Omdat dit in sommige gevallen niet is wat we willen. (Stel er komt nooit meer een item op de queue, dan hebben we een hangend programma) introduceren we:

[trypop

empty

[trypop

not_empty

sos

] sos

〈trypop q x, s〉 → s

]

if q = ε

〈trypop q x, s〉 → s [(a : q ) a q ][x a a ] if q ≠ ε

Met behulp van bovenstaande semantiek en syntax beschrijvingen hebben we nu message queues in While.


9/29

Signals in While Een tweede communicatie en synchronisatie middel voor threads zijn zogenaamde signals. Een signal kan een andere thread vertellen dat hij mag beginnen met het uitvoeren van bepaalde taken. Een signal implementeren we in While aan de hand van de volgende syntax voor een signal declaratie:

S ::= ... | newSignal sig Met

sig ::= a

Een signal implementeren we als een signalnaam met een integer waarde. Een signal heeft initieel de waarde 0 (false) . De semantiek :

newSignal sig , s → s[sig a 0] We zullen deze declaratie in alle voorbeelden weglaten en aannemen dat het gebruikte signal al is toegevoegd aan de verzameling van signal variabelen. Signals hoeven nooit uit de state verwijderd te worden, we nemen aan dat ze bij beëindiging van het programma automatisch worden verwijderd. Een signal versturen gaat doormiddel van het statement “signal” met als parameter de naam van het signal. Hiermee wordt de waarde van het betreffende signal op 1 (true) gezet.

[signal sos]

〈 signal sig , s〉 → s [sig a 1]

Bovenstaande semantiek maakt duidelijk dat een signal niet opnieuw kan worden gebruikt, wanneer het signal statement nog een keer wordt aangeroepen blijft de waarde van het signal op 1 staan.


10/29

Wachten op een signal gebeurt met het statement “wait” met als parameter de naam van het signal waarop gewacht moet worden. Wanneer de waarde van het signal waarop gewacht wordt 0 (false) is, dan blijft wait gewoon wachten.

[wait

false

sos

]

〈 wait sig , s〉 → 〈 wait sig , s〉

if A[| sig |]s = 0

Wanneer de waarde van het signal waarop gewacht wordt 1 (true) is, dan wordt wait gewoon ‘overgeslagen’.

[wait

true

sos

]

〈 wait sig , s〉 → s

if A[| sig |] s = 1

〈 wait signal1, s 〉 wanneer A[| signal1 |]s = 1 is dus equivalent met het statement “skip”. Omdat we een signal nu niet kunnen resetten maken we ook nog een reset statement. Wanneer we bijvoorbeeld het volgende programma hebben: while true do wait sig1; S; od Dan zal S als hij eenmaal wordt uitgevoerd daarna oneindig vaak worden uitgevoerd omdat signal sig1, de waarde 1 behoudt.

[resetsos]

〈 reset sig , s〉 → s [sig a 0]

In feite is dit dus het tegenovergestelde van het signal statement.


11/29

Race Conditions & Deadlocks Race Conditions Als threads met elkaar moeten communiceren dan is het noodzakelijk dat er geen race conditions kunnen ontstaan. In het dictaat van Nielson & Nielson is onderstaand voorbeeld opgenomen om te illustreren dat de volgorde van verwerking invloed kan hebben op het uiteindelijke resultaat. (x := 1) par (x := 2; x := x + 2) Dit code voorbeeld kan drie verschillende resultaten voor de waarde van x hebben, namelijk 4,1 en 3. We zullen waar nodig naar dit probleem verwijzen als race conditions.

Deadlocks We bekijken nu het volgende programma: signal sig par wait sig In principe kan het nu voorkomen dat par continue het rechter statement (wait sig) uitvoert waardoor ons programma blijft hangen (deadlock). Om dit vervelende probleem te voorkomen passen we de semantiek van par aan voor die specifieke gevallen waarin onze programma’s zouden kunnen blijven hangen. Wanneer par een wachtende pop of wait tegenkomt zal hij eerst verder gaan met de andere thread. De orginele par semantiek:

[par ] 1 sos

[par ] 2

sos

[par ] 3

sos

[par ] 4

sos

S 1, s ⇒ S 1' , s' S 1 par S 2, s ⇒ S 1' par S 2, s'

S 1, s ⇒ s ' S 1 par S 2, s ⇒ S 2, s' S 2, s ⇒ S 2 ' , s ' S 1 par S 2, s ⇒ S 1 par S 2' , s' S 2, s ⇒ s ' S 1 par S 2, s ⇒ S 1, s'


12/29

Uitbreidingen van par voor signals:

[par ] 5

sos

[par ] 6

sos

[par ] 7

sos

[par ] 8

sos

[par ] 9

[par

sos

10

sos

]

[par ] 11 sos

[par

12

sos

]

S 2, s ⇒ S 2 ' , s ' wait sig ; S 1 par S 2, s ⇒ wait sig ; S 1 par S 2' , s' S 2, s ⇒ s ' wait sig ; S 1 par S 2, s ⇒ wait sig ; S 1, s' S 2, s ⇒ S 2' , s ' ( wait sig ) par S 2, s ⇒ ( wait sig ) par S 2' , s' S 2, s ⇒ s ' ( wait sig ) par S 2, s ⇒ wait sig , s ' S 1, s ⇒ S 1' , s ' S 1 par wait sig ; S 2, s ⇒ S 1' par wait sig ; S 2, s ' S 1, s ⇒ s ' S 1 par wait sig ; S 2, s ⇒ wait sig ; S 2, s ' S 1, s ⇒ S 1' , s ' S 1 par wait sig , s ⇒ S 1' par wait sig , s ' S 1, s ⇒ s ' S 1 par wait sig , s ⇒ wait sig , s '


if A[| sig |]s = 0 if A[| sig |]s = 0 if A[| sig |]s = 0 if A[| sig |] s = 0

if A[| sig |]s = 0 if A[| sig |]s = 0 if A[| sig |]s = 0 if A[| sig |]s = 0

13/29

Het moge duidelijk zijn wat het idee bij deze regels is. Er zijn echter nog meer regels voor par (wanneer er bijvoorbeeld aan beide kanten een wait statement voorkomt). Deze regels zijn nagenoeg equivalent aan de regels zoals hierboven beschreven en daarom laten we deze weg. Hetzelfde geldt voor de par regels waar pop statements in voor komen. Ook deze regels zijn nu triviaal en daarom laten we ze weg. Specifiekere par regels hebben hier uiteraard voorrang op mindere specifieke par regels. Bekijk het volgende programma: (wait sig) par x:=3

[

]

In een toestand waarin geldt A[| sig |] s = 0 zal uiteraard par 8 sos van toepassing zijn en niet par 4 sos .

[

]

We zullen vanaf nu verder werken met deze aangepaste versie van par.


14/29

Message Queues versus Signals De functionaliteit van message queues komt zeer sterk overeen met de functionaliteit van signals. We zien dat de functionaliteit van signals een subset is van de functionaliteit van message queues. Onderstaand voorbeeld illustreert dit: Voorbeeld 1a: sending thread:

receiving thread:

signal signal1;

par

wait signal1;

Hier wacht de receiving thread op een signaal van de sending thread. Ditzelfde zouden we hebben kunnen doen met behulp van een message queue: Voorbeeld 1b: sending thread: push 0 queue1;

receiving thread: par

pop queue1 x;

Omdat we hier te maken hebben met atomaire statements hoeven we geen rekening te houden met raceconditions. We gaan bewijzen dat:

pop q x, s → s' ⇒ wait sig , s → s'

(stelling 1a)

en

push 0 q, s → s' ⇒ signal sig , s → s'

[]

Onder de aanname dat s q ≅ signal sig op message queue q:

(stelling 1b)

s [sig ] . Waarmee we een mapping bedoelen van

(s [q = ε ]) = ( A[| sig |] s = 0) ∧

(s [q ≠ ε ]) = ( A[| sig |]s = 1)


15/29

De stelling 1a is onjuist. Dit kunnen we duidelijk maken door een tegenvoorbeeld. Voorbeeld 2a: sending thread: signal sig1;

receiving thread: par

while true do wait sig1; od

Wanneer we het recept van voorbeeld 1 ook hier toepassen dan krijgen we het volgende programma: Voorbeeld 2b : sending thread:

receiving thread:

push 0 queue1; par

while true do pop queue1 x; od

Het is duidelijk dat dit programma niet equivalent is met het programma van voorbeeld 2a. Immers bij ieder uitgevoerd pop statement wordt het bericht van de message queue verwijderd. De enige manier om met message queues een equivalent programma te schrijven is door oneindig veel berichten op de queue te plaatsen of door na ieder pop statement een push uit te voeren. We passen onze stellingen aan en bewijzen:

pop q x, s → s' ⇒ wait sig , s → s' Mits

[q = ε ∨ q = 0 : ε ]s ∧ s[| q |] ≅ s[| sig |]

(stelling 2a)

en

push 0 q, s → s' ⇒ signal sig , s → s' Mits

s[| q |] ≅ s[| sig |]

(stelling 2b)


16/29

We bewijzen stelling 2a. We bewijzen dat als:

〈 pop q x; push 0 q, s〉 → s '

(*)

dan ook

〈 wait sig , s〉 → s '

(**)

Als:

[q = ε ∨ q = 0 : ε ]s ∧ s [| q |] ≅ s [| sig |]

We nemen aan (*) en bewijzen dat als de berekeningsrij van (*) termineert, dan termineert ook de berekeningsrij van (**) en de eindtoestanden van beide rijen zijn hetzelfde. Er zijn 2 mogelijkheden voor de gevalsonderscheid:

[

Geval 1 pop not_empty sos

berekeningsrij van

(*). We maken

] [

]

Omdat we de regel pop not_empty sos gebruiken en we als aanname hebben dat de queue of leeg is of slechts 1 element bevat weten we hoe de queue er initieel uit moet zien.

pop q x; push 0 q, s[q a (a : ε )] { pop not_empty} ⇒

push 0 q, s[q a ε ][x a a ]

{

push sos}

⇒

s[q a (0 : ε )]

We zien verder dat de variabele x de waarde heeft gekregen die op de queue stond. We nemen voor x altijd een ongebruikte variabele die behalve hier verder nergens in ons programma voorkomt en ook nooit meer gebruikt zal worden. Om deze reden kunnen we de variabele x als niet relevant voor de toestand beschouwen.


17/29

Voor wait maken we ook een berekeningsrij beginnend in dezelfde toestand. Door onze aannamen zien we dat dat de toestand s[sig a 1] moet zijn.

wait sig , s[sig a 1]

{ wait

true

[

}⇒

sos

]

s sig a 1

Door onze aannamen kunnen we nu zien dat s[q ≠ ε ] = s[sig a 1] .

[

Geval 2 pop empty sos

]

pop q x; push 0 q, s[q a ε ]

{ pop

empty

}⇒

sos

pop q x; push 0 q, s[q a ε ]

... Het is duidelijk dat deze berekeningsrij looped. Voor wait maken we weer een berekeningsrij beginnend in dezelfde toestand. Door onze aannamen zien we dat dat de toestand s[sig a 0] moet zijn.

wait sig , s[sig a 0] { wait false sos } ⇒

wait sig , s[sig a 0]

... Deze berekingsrij looped vanuit dezelfde toestand als de berekingsrij voor (*). Dat deze toestanden hetzelfde zijn blijkt weer uit onze aannamen. En dus (*) → (**) .

?


18/29

Nu bewijzen we stelling 2b. We bewijzen dat als:

push 0 q, s → s'

(*)

dan ook

signal sig , s → s'

(* *)

We nemen aan (*) en bewijzen dat als de berekeningsrij van (*) termineert, dan termineert ook de berekeningsrij van (**) en de eindtoestanden van beide rijen zijn hetzelfde.

push 0 q, s { push sos } ⇒

s[q a (0 : q)]

Vanuit dezelfde toestand s krijgen we volgens de regel [signal sos ] de berekeningsrij:

〈 signal sig , s〉 {signal sos } ⇒ s [sig a 1]

En volgens onze aannamen geldt s[q a (0 : q )] = s [sig a 1] . Immers s[| q a (0 : q )] = s[| q ≠ ε ]


?

19/29

While versus Signals Het valt op dat de toegevoegde statements voor signals niet zo vreselijk bijzonder zijn en nogal wat overeenkomsten vertonen met de originele statements van While. Wellicht is het zo dat behalve het principe van variabelen in threads en variabelen tussen threads (lokale en globale variabelen) er weinig verschil is. In dat geval zouden er statements in While moeten bestaan die semantisch equivalent zijn met signal en wait. We bewijzen dat

∀s ∈ State Ssos  while not  b == 1 do skip s = Ssos[wait b]s (stelling 3) Mits de signal variabele b ook toegankelijk is voor statements uit While. Nogmaals de SOS semantiek van het while statement:

[whilesos]

〈 while b do S , s〉 → if b then (S ; while b do S ) else skip, s

Eerst bewijzen we dat als

〈 while not (b == 1) do skip, s〉 → s'

(*)

dan ook

〈 wait b, s〉 → s'

(* *)


20/29

We nemen aan (*) en bewijzen dat als de berekeningsrij van (*) termineert, dan termineert ook de berekeningsrij van (**) en de eindtoestanden van beide rijen zijn hetzelfde. De berekenigsrij voor (*) kan op 2 manieren worden gemaakt. We maken een gevalsonderscheid. Geval 1

[if sos] ff

while not (b == 1) do skip , s { while sos } ⇒

if not (b == 1) then (skip; while not (b == 1) do skip ) else skip , s

{ if

ff

sos

}⇒

skip , s {skip sos }

⇒

s Nu maken we een berekeningsrij voor (**) vanuit dezelfde toestand s, gebruikmakend van het gegeven B | not (b == 1) | = ff en dus A | b | s = 1 .

[

]

[ ]

wait b, s

{ wait }⇒ true

s Waarmee we zien dat als (*) begint vanuit s en gaat naar s’, dan gaat ook (**) vanuit s naar s’. (waarbij in dit geval s’ = s)


21/29

Geval 2

[if sos] tt

[ ]

In het 2e geval geldt dus A | b | s = 0 en kunnen we de volgende berekeningsrij maken:

while not (b == 1) do skip , s {

while sos }

⇒

if not (b == 1) then (skip ; while not (b == 1) do skip ) else skip , s

{ if

tt

sos

}⇒

while not (b == 1) do skip , s

{

while

sos

}⇒

if not (b == 1) then (skip ; while not (b == 1) do skip ) else skip , s ... Het is duidelijk dat deze berekeningsrij looped vanuit s. Nu maken we een berekeningsrij voor (**) vanuit dezelfde toestand s, gebruikmakend van het gegeven B | not (b == 1) | = tt en dus A | b | s = 0 .

[

]

[ ]

wait b, s

{ wait

false

sos

}⇒

wait b, s ... Het is wederom duidelijk dat ook deze berekeningsrij looped vanuit s. Waarmee we hebben aangetoond dat (*) looped als (**) looped en dat als (*) gaat naar s’, (**) ook gaat naar s’. Waarmee is bewezen dat (*) ⇒ (* *) . Het bewijs van concluderen.

(* *) ⇒ (*)

gaat op analoog, waardoor we stelling 3 kunnen

?


22/29

Het is verder eenvoudig om te zien dat als b een globale variabele is, dat het statement: b := 1; semantisch equivalent is met: signal b; Immers

〈b := 1, s〉 → s[ A[| b |] = 1]

en ook

〈 signal b, s〉 → s[ A[| b |] = 1]

?


23/29

While versus Message Queues Omdat we al gezien hebben dat de functionaliteit van signals ook met de standaard while statements kan worden bereikt (mits er gedeelde variabelen bestaan) en we al hebben gezien dat de functionaliteit van message queues gedeeltelijk overlapt met die van signals, reist de vraag of het niet ook mogelijk is om message queues in While te implementeren zonder uitbreiding van de orginele semantiek. Het eerste probleem waar men tegenop loopt is het feit dat er geen datastructuur is om meerdere waarden in op te slaan. Om de semantiek van While toch niet te hoeven uitbreiden maken we gebruik van Gödel codering.

Gödel codering We maken gebruik van 1 gedeelde (shared) integer variabele waarin we onze reeks van waarden opslaan als één getal met behulp van Gödel codering. Een Gödel codering is de codering van een reeks getallen in één getal. Een reeks getallen x 0 , x1.. xn van lengte n + 1 wordt gecodeerd door: pn(0) x 0 + 1 • pn(1) x1 + 1 • .. pn(n) xn + 1 (Bij iedere x wordt 1 opgeteld zodat het ook mogelijk is om het getal 0 te coderen, immers

∀x ∈ Ν x 0 ≡ 1 )

Hierbij is pn(i ) de functie die het i-de priemgetal oplevert. ( pn(0) = 2 ) Korter gezegd: n

{x , x .. x } = ∏ pn(i) x + 1 i

0

1

n

i=0

Bijvoorbeeld de queue “:3:2:1” coderen we met behulp van een Gödel codering als 2 4 • 33 • 5 2 = 10800 . Dit getal slaan we op in de gedeelde variabele.


24/29

Gödel codering : een element toevoegen Voor het toevoegen van een getal wordt de Gödel codering uitgelezen, gedecodeerd en wordt het nieuwe getal toegevoegd. Dit wordt opnieuw gecodeerd en opgeslagen in de gedeelde variabele waarbij de oude waarde overschreven wordt. Hierbij dient er wel erg gelet te worden op race-conditions. In de tijd dat er een nieuw getal wordt toegevoegd mag er door de receiving thread niet gelezen worden. Gegeven de functies encode_gödel en decode_gödel met het volgende prototypes: encode_gödel (number, queue) De functie die gegeven een getal en een Gödel getal, het getal toevoegt aan het Gödel getal. Bijvoorbeeld: encode_gödel( 3, 108 ); // [1,2] retourneert het getal 18000 ( [3,1,2] ) decode_gödel (position, queue) De functie die gegeven een positie en een Gödel getal het (getal + 1 ) op de positie decodeert uit het Gödel getal. Wanneer de positie niet bestaat wordt er 0 geretourneerd. Posities beginnen vanaf 0. Bijvoorbeeld: decode_gödel( 1, 67500 );

// [1,2,3]

retourneert het getal 3. Wanneer we hier nog 1 vanaf trekken krijgen we het gecodeerde getal 2. (NB “Je moet er altijd 1 vanaf trekken”) decode_gödel ( 3, 67500 );

// [1,2,3]

retourneert het getal 0 omdat de positie 3 niet bestaat.


25/29

Een programma in While dat op deze manier een message queue implementeert zou er als volgt uit kunnen zien voor een sending thread: Voor de overzichtelijkheid gebruiken we hier een variant van While met procedures en parameters. Tevens gebruiken we het protect statement zoals behandeld in het werkcollege. sending thread x := 3; push (x, queue1)

// the shared queue variable is called // queue1

proc push is (number, queue) begin protect counter := 0; temp := decode_gödel(counter , queue) - 1; new := 0; while temp <> 0 do new := encode_gödel(temp, new); counter := counter + 1; temp := decode_gödel(counter , queue) - 1; od new := encode_gödel(x, new); queue := new; end end


26/29

Gödel codering : een element uitlezen De receiving thread leest de Gödel codering uit de gedeelde variabele, decodeert deze, leest het eerste getal en codeert de overige getallen weer en slaat ze op in de gedeelde variabele. Ook hier mag er terwijl de receiving thread uitleest, door de sending thread geen nieuw getal worden toegevoegd. Een programma in While dat op deze manier een message queue implementeert zou er als volgt uit kunnen zien voor een receiving thread: receiving thread pop (queue1, x); proc pop is (queue, number) begin protect counter := 0; while queue == 0 do skip; // queue is empty, wait od previous := decode_gödel(counter , queue) - 1; counter := counter + 1; next := decode_gödel(counter , queue) - 1; while next <> 0 do previous := next; counter := counter + 1; next := decode_gödel(counter , queue) - 1; od number := previous; end end

We gaan verder niet in op hoe de functies decode_gödel en encode_gödel er precies uit zien. We weten dat ze in While te implementeren zijn. Met het vinden van een oplossing voor het opslaan van meedere waarden zonder het uitbreiden van de semantiek van While hebben we het belangrijkste probleem opgelost. Met behulp van de beschreven functies is het eenvoudig om een message queue te implementeren.


27/29

Conclusies We hebben laten zien dat het uitbreiden van While met message queues en signals relatief eenvoudig is en dat de semantiek hiervoor redelijk voor de hand ligt. Tevens hebben we aangetoond dat de functionaliteit van signals gemakkelijk kan worden nagebootst met message queues en dat een uitbreiding van While voor signals dus in feite overbodig is als er al message queues aanwezig zijn. Als laatste hebben we gezien dat zelfs voor het gebruik van message queues While niet persé uitgebreid hoeft te worden. We kunnen de functionaliteit van message queues namelijk ook implementeren door gebruik te maken van Gödel codering. In de praktijk zal dit echter nooit gebeuren omdat Gödel getallen zeer snel erg groot worden en omdat het coderen en decoderen een zeer grote berekening is. Verder dwingen de semantiek uitbreidingen correct gebruik van queues af. Bij het werken met queues zonder semantiek uitbreidingen is het veel eenvoudiger om ‘foute’ programma’s te schrijven. Voor het gebruik van message queues hebben uitbreidingen van de semantiek van While dus zeker de voorkeur.


28/29

Referenties Hilfinger, P., Threads of Control [online], Department of Computer Science Berkeley University, 13 Nov 2002. Portable Document Format. Available from: Nielson, H.R. and Nielson F., Semantics with applications: A Formal Introduction [online], Revised, John Wiley & Sons, July 1999. Portable Document Format. Available from: Postscript Format. Available from: Nutt, G.J., Operating Systems: A Modern Perspective [online], Second Edition, Pearson Education Inc., 18 July 2001. [Chapter 9]. Available from: Sudkamp. T.A., Languages and Machines – An Introduction to the Theory of Computer Science, Second Edition, Addison-Wesley, January 1997. Shene, C.K., Multithreaded Programming with ThreadMentor: A Tutorial [online], Revised, Department of Computer Science Michigan Technological University, 16 April 2002. Available from:


29/29

Semantiek & Correctheid Thread synchronisatie & communicatie

Recommend Documents