Szymański's algorithm

Szymanski's Mutual Exclusion Algorithm is a mutual exclusion algorithm devised by computer scientist Dr. Boleslaw Szymanski, 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. Szymanski's 5).

The algorithm

The algorithm is modeled on a waiting room with an entry and exit doorway.[1] Initially the entry door is open and the exit door is closed. 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 processes then enter the critical section one by one (or in larger groups if the critical section permits this). The last process to leave the critical section closes the exit door and reopens the entry door, so the next batch of processes may enter.

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). The status of the entry door is computed by reading the flags of all processes. Pseudo-code is given below:

#Entry protocol
flag[self] ← 1                    #Standing outside waiting room
await(all flag[1..N] ∈ {0, 1, 2}) #Wait for open door
flag[self] ← 3                    #Standing in doorway
if any flag[1..N] = 1:            #Another process is waiting to enter
    flag[self] ← 2                #Waiting for other processes to enter
    await(any flag[1..N] = 4)     #Wait for a process to enter and close the door

flag[self] ← 4                    #The door is closed
await(all flag[1..self-1] ∈ {0, 1})   #Wait for everyone of lower ID to finish exit protocol

#Critical section
#...

#Exit protocol
await(all flag[self+1..N] ∈ {0, 1, 4}) #Ensure everyone in the waiting room has
                                       #realized that the door is supposed to be closed
flag[self] ← 0 #Leave. Reopen door if nobody is still in the waiting room

Note that the order of the "all" and "any" tests must be uniform.

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.[2][5]

References

  1. 1 2 Szymanski, Boleslaw K. (1988). "A simple solution to Lamport's concurrent programming problem with linear wait". ICS '88: Proceedings of the 2nd international conference on Supercomputing. St. Malo, France: ACM: 621–626. doi:10.1145/55364.55425. ISBN 0-89791-272-1.
  2. 1 2 Manna, Zohar; Pnueli, Amir (1990). "An Exercise in Verification of Multi-Process Programs.". Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra. Springer Verlag. pp. 289–301. ISBN 978-0-387-97299-2.
  3. ↑ Szymanski, Boleslaw (1990). "Mutual Exclusion Revisited" (PDF). Fifth Jerusalem Conference on Information Technology. Jerusalem, Israel: 110–117.
  4. ↑ Lamport, Leslie (1986). "The mutual exclusion problem: partII—statement and solutions". Journal of the ACM. ACM. 33 (2): 327–348. doi:10.1145/5383.5385.
  5. ↑ de Roever, Willem-Paul; de Boer, Frank; Hannemann, Ulrich; Hooman, Jozef; Lakhnech, Yassine; Poel, Mannes; Zwiers, Job (November 2002). Concurrency Verification. Number 54 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. doi:10.2277/0521806089. ISBN 978-0-521-80608-4.

See also


This article is issued from Wikipedia - version of the 7/31/2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.