= Solution
Use a <message-passing mutual exclusion server> with an `owner` field and a <FIFO queue>. A request includes its client's identity. The server handles one received message at a time, and a client has at most one outstanding request. The following pseudocode assumes reliable <message passing> and compliant clients:
``
owner = NONE
waiting = empty FIFO queue
forever:
(kind, client) = receive_from_any_client()
if kind == REQUEST:
waiting.push_back(client)
else if kind == RELEASE:
assert client == owner
owner = NONE
if owner == NONE and not waiting.empty():
owner = waiting.pop_front()
send(owner, GRANT)
``
A client sends `REQUEST`, waits for `GRANT`, runs its complete animation, and sends `RELEASE` before making another request.
The invariant proving <mutual exclusion> is: \b[at most one client has received an unreturned grant, and that client is `owner`.] Only the final block issues a grant, and it first requires no current owner. A valid release removes that ownership. Since clients use the display only while holding a grant, simultaneous use is impossible. The <FIFO queue> prevents accepted requests from being overtaken by later ones. With eventual message delivery, continued server execution, and finite animations, each accepted request is eventually served; these progress assumptions are separate from the safety invariant.
Back to article page
