Semantics of Semaphores

Reference:

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

Abstract:

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.

Keywords:

semaphores, process synchronization, mutual exclusion, weakest preconditions

Suggested BibTeX entry:

@techreport{HUT-TCS-A53,
    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},
}