= Message-passing mutual exclusion server
Maintain an owner identity, initially empty, and a <FIFO queue> of accepted client requests. A request appends its sender to the <FIFO queue>. A release from the owner clears the owner. Whenever there is no owner and the <FIFO queue> is nonempty, remove its oldest request, record that client as owner, and send a grant. The server processes these state changes sequentially.
\b[Safety proof.] At most one grant is outstanding: a new grant requires an empty owner field, and a valid release clears precisely the preceding ownership. Compliant clients access the resource only while holding their grant, so <mutual exclusion> follows. With reliable eventual <message passing>, continued server execution and finite resource-use durations, the <FIFO queue> also gives <starvation freedom> for accepted requests, since later requests cannot overtake them.
Back to article page
