DEFINITION MODULE Semaphores;

  (* Provides mutual exclusion facilities for use by processes. *)

TYPE
  SEMAPHORE;

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 TRUE 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.
  *)

PROCEDURE IsSemaphoreException(): BOOLEAN;
  (* Returns TRUE if the current coroutine is in the exceptional execution state because
     of the raising of the Semaphores exception; otherwise returns FALSE.
  *)

END Semaphores.

