TCS / Research / Publications / Semantics of Semaphores
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Semantics of Semaphores


Stefan Rönn. Semantics of semaphores. Research Report A53, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, 1998.


We present a formal definition of semaphores using weakest preconditions. With the definition we prove the mutual exclusion algorithm and show that the semaphore axioms given by Martin and de Snepscheut are implied by the invariant relation of the proof. We further demonstrate how a general k-semaphore can be realised with the help of a split binary semaphore. To this end, we introduce a program construct that facilitates the usage of the split binary semaphore.


semaphores, process synchronization, mutual exclusion, weakest preconditions

Suggested BibTeX entry:

    address = {Espoo, Finland},
    author = {Stefan R{\"o}nn},
    institution = {Helsinki University of Technology, Digital Systems Laboratory},
    number = {A53},
    pages = {10},
    title = {Semantics of Semaphores},
    type = {Research Report},
    year = {1998},

PostScript (151 kB)
GZipped PostScript (60 kB)

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.