We show that, contrary to common belief, Dijkstra's K-state mutual exclusion algorithm on a ring [1, 2] also stabilizes when the number K of states per process is one less than the number N+1 of processes in the ring. We formalize the algorithm and verify the proof in PVS, based on Qadeer and Shankar's work [8]. We show that K=N is sharp by giving a counter-example for K=N-1.

, , ,
, , ,
Software Engineering [SEN]
Software Analysis and Transformation

Fokkink, W.J, Hoepman, J.H, & Pang, J. (2004). A note on K-state self-stabilization in a ring with K=N. Software Engineering [SEN]. CWI.