Date: August 1998
Pages: 10
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