The concept of FCFS was introduced by Lamport in 1974 for his Bakery Algorithm. Another mutual exclusion algorithm that satisfies FCFS is the algorithm of Lyclama and Hadzilacos (1991). A mutual exclusion algorithm satisfies FCFS iff it satisfies the following three conditions: (1) its entry function is a sequential composition of two fragments Doorway and Waiting; (2) a thread traverses Doorway in a bounded number of its own steps without waiting; (3) whenever some thread, say p, enters Doorway when another thread, q, is in Waiting, thread p does not enter the critical section before q does.
Here FCFS is investigated and implemented without mutual exclusion. It can be add the FCFS property to an arbitrary mutual exclusion algorithm. A paper is in preparation. A PVS proof script is available.
The term FIFO (first-in first-out) is reserved for the special case that the Doorway consists of a single atomic statement because then the order of service is determined by the order of executing Doorway.
It is proved that FCFS cannot be distinguished from FIFO, even if the beginning of waiting is made observable. Indeed, FCFS implements FIFO (and vice versa) in the sense of Abadi-Lamport (1991). A paper is in preparation. A PVS proof script is available.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink