DEFINITION MODULE Semaphores;
(* Provides mutual exclusion facilities for use by processes. *)
PROCEDURE Create (VAR s: SEMAPHORE; initialCount: CARDINAL );
(* Creates and returns s as the identity of a new semaphore that
has its associated count initialized to initialCount, and has
no processes yet waiting on it.
PROCEDURE Destroy (VAR s: SEMAPHORE);
(* Recovers the resources used to implement the semaphore s,
provided that no process is waiting for s to become free.
PROCEDURE Claim (s: SEMAPHORE);
(* If the count associated with the semaphore s is non-zero,
decrements this count and allows the calling process to
continue; otherwise suspends the calling process until
s is released.
PROCEDURE Release (s: SEMAPHORE);
(* If there are any processes waiting on the semaphore s,
allows one of them to enter the ready state; otherwise
increments the count associated with s.
PROCEDURE CondClaim (s: SEMAPHORE): BOOLEAN;
(* Returns FALSE if the call Claim(s) would cause the calling
process to be suspended; in this case the count associated
with s is not changed. Otherwise returns TRUE and the
associated count is decremented.