08-16-2017, 10:30 PM
Lamport's Mutual Exclusion Algorithm
Assumes messages are delivered in FIFO order between each pair of sites
Is not based on tokens
Is based on Lamport's clock synchronization scheme*
Each request gets a timestamp
Requests with lower timestamps take priority over requests with higher timestamps
Each site maintains a queue of pairs (timestamp, site), ordered by timestamp
* Are these the single-integer valued clocks, or the vector clocks?
The Algorithm
Request
Si sends REQUEST(tsi, i) to all sites in its request set Ri and puts the request on request_queuei
when Sj receives REQUEST(tsi, i) from Si it returns a timestamped REPLY to Si and places Si's request on request_queuej
Si waits to start the CS until both
[L1:] Si has received a message with timestamp > (tsi, i) from all other sites
[L2:] Si's request is at the top of request_queuei
Release
Si removes request from top of request_queuei and sends time-stamped RELEASE message to all the sites in its request set
when Sj receives a RELEASE messages from Si it removes Si's request from request_queuej
Correctness
Suppose Si and Sj are executing the CS concurrently.
L1 and L2 must hold at both sites concurrently.
Si and Sj both have requests at top of their queues and L1 holds, at some instant t.
WLOG suppose Si's request has earlier timestamp than Sj's.
(Remember the tie-breaking rule!)
Assuming communication channels are FIFO, at instant t Si's request is queued at Sj, when Sj is in the CS and Sj's own request is at the top of the queue, ahead of a smaller timestamp request.
This is a contradiction.