Vecerajúci filozofi: Program pre os
Na zaciatku predpokladáme, ze
- ? filozofi špekulujú (? procesy sú thinking)
- ? vidlicky sú špinavé (? fork sú dirty)
- fork a request-token sú na rôznych miestach
- forks sú tak, ze graf G’ je acyklický: napr. ocíslujeme procesy a fork dostane proces s nizším císlom (vyšší index ? vyššia priorita)
Program os
always
? ? u:: u.me = ??v: E[u, v]::
(fork[u, v] = u ? (clean[u, v] ? rt[u, v] = v))? ?
? ? ? u, v: E[u, v]::
sendreq[u, v] = ((fork[u, v] = v) ? (rt[u, v] = u) ? u.h)
? sendfork[u, v] = ((fork[u, v] = u) ? ?clean[u, v] ?
(rt[u, v] = u) ? ?u.e) ?
initially
? ? u:: u.dine = t ?
? ? ?(u, v):: clean[u, v] = false ?
? ? ?(u, v): u < v:: fork[u, v], rt[u, v] = u, v ?
assign
? ? u:: u.dine = e if u.h ? u.me
|| ? || v: clean[u, v] := false if u.h ? u.me ? ?
? ? ?(u, v):: rt[u, v] := v if sendreq[u, v]
? fork[u, v], clean[u, v] = v, true if sendfork[u, v] ?