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.

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.