Tentamen "Co-operating Sequential Processes."
Aan een grote ronde tafel zijn de plaatsen cyclisch genummerd van 0 t/m 39; de leden van een gezelschap van 40 personen zijn eveneens genummerd van 0 t/m 39, ieder mag alleen op zijn eigen plaats - dwz. de plaats, die zijn eigen nummer heeft - aan tafel aanzitten.
Hun gedragspatroon bestaat uit een niet-eindigende cyclische opeenvolging van:
leven (buitenskamers);
borrelen (binnenskamers, maar niet aan tafel);
eten (binnenskamers, aan tafel);
en alleen voor de heren
sigaren (binnenskamers, niet aan tafel).
Hun gedragingen moeten zo gesynchroniseerd zijn dat
1) nimmer drie cyclische opeenvolgende plaatsen aan tafel tegelijkertijd bezet zijn, en
2) geen dame van tafel opstaat, tenzij er tenminste 1 andere dame in de kamer is.
Voor de dames (die qualitate qua na tafel geen sigaar roken) is het opstaan van tafel en het verlaten van de kamer eenzelfde handeling. Eventuele personen, die met aan tafel gaan moeten wachten (wegens regel 1) op het van tafel opstaan van dame A, die (wegens regel 2) met opstaan moet wachten totdat, zeg, dame B binnenkomt, hebben ten aanzien van het aan tafel gaan voorrang boven dame B.
Er zijn tenminste twee dames in het gezelschap, dat met iedereen buitenskamers levend geinitialiseerd wordt.
De oplossing acht (ik) in het omvattend universum gedeclareerd:
| 1) | de boolean procedure dame(u); value u; integer u; deze heeft de waarde "true" als persoon nr. u een dame is, de waarde "false" als persoon nr. u een heer is. |
| 2) | de integer procedure mod40(u); value u; integer u; deze heeft de waarde van u, gereduceerd modulo 40. |
Gegeven is een oplossing van de volgende structuur.
begin
semaphore
mutex, damutex; semaphore
array
persem [0:39];
boolean
array
honger [0:39]; integer
array
eettal [0:39];
integer
damnr, k;
procedure test(u); value
u; integer
u;
begin
if
honger[u] then
begin
if
eettal[mod40(u-1)] < 2 and
eettal[u] < 2 and
eettal[mod40(u+1)] < 2 then
begin
eettal[mod40[u-1)] := eettal[mod40(u-1)] + 1;
eettal[u] := eettal[u] + 1;
eettal[mod40(u+1)] := eettal[mod40(u+1)] + 1;
honger[u] := false ; V(persem[u])
end
end
end
procedure staop(u); value
u; integer
u;
begin
eettal[mod40(u-1)] := eettal[mod40(u-1)] - 1;
eettal[u] := eettal[u] - 1;
eettal[mod40(u+1)] := eettal[mod40(u+1)] - 1;
test(mod40(u-2)); test(mod40(u-1));
test(mod40(u+1)); test(mod40(u+2))
end
for
k := 0 step 1 until 39 do
begin
honger[k] := false; eettal[k] := 0; persem[k] := 0 end;
mutex := 1; damutex := 1; damnr := -1; k := 0;
parbegin
persoon 0 : begin..... ..... ..... .....end;
⋮
persoon39 : begin..... ..... ..... .....end
parend
end
waarbij de structuur van persoon h is als volg:
persoon h:
begin Lh: leven;
if dame(h) then
begin P(damutex); k := k + 1;
if
damnr ≥ 0 then
begin P(mutex); staop(damnr); V(mutex);
V(persem[damnr]); damnr := -1
end;
V(damutex)
end;
borrelen;
P(mutex); honger[h] := true; test(h); V(mutex); P(persem[h]);
eten;
if dame(h) then
begin P(damutex); k := k - 1;
if
k = 0 then
begin
damnr := h; V(damutex); P(persem[h]) end
else
begin P(mutex); staop(h); V(mutex); V(damutex) end
end
else
begin P(mutex); staop(h); V(mutex);
sigaarroken
end;
goto Lh
end
Opgave. Bewijs, dat de gegeven oplossing aan alle specificaties voldoet.
NB. De tentaminandi wordt verzocht hun papier slechts eenzijdig te beschrijven.
transcribed by Sam Samshuijzen
revised Mon, 15 Jan 2007