Szymański's algorithm

Szymański's Mutual Exclusion Algorithm is a mutual exclusion algorithm devised by computer scientist Dr. Bolesław Szymański, which has many favorable properties including linear wait,[1][2] and which extension[3] solved the open problem posted by Leslie Lamport[4] whether there is an algorithm with a constant number of communication bits per process that satisfies every reasonable fairness and failure-tolerance requirement that Lamport conceived of (Lamport's solution used n factorial communication variables vs. Szymański's 5).

The algorithm is modeled on a waiting room with an entry and exit doorway.

All processes which request entry into the critical section at roughly the same time enter the waiting room; the last of them closes the entry door and opens the exit door.

The implementation consists of each process having a flag variable which is written by that process and read by all others (this single-writer property is desirable for efficient cache usage).

Despite the intuitive explanation, the algorithm was not easy to prove correct, however due to its favorable properties a proof of correctness was desirable and multiple proofs have been presented.