1987-05-13 14:36:45 +00:00
|
|
|
DEFINITION MODULE Semaphores;
|
1988-02-19 15:54:01 +00:00
|
|
|
(*
|
|
|
|
|
Module: Processes with semaphores
|
|
|
|
|
Author: Ceriel J.H. Jacobs
|
|
|
|
|
Version: $Header$
|
|
|
|
|
|
|
|
|
|
On systems using quasi-concurrency, the only opportunities for process-
|
|
|
|
|
switches are calls to Down and Up.
|
|
|
|
|
*)
|
1987-05-13 14:36:45 +00:00
|
|
|
|
|
|
|
|
TYPE Sema;
|
|
|
|
|
|
|
|
|
|
PROCEDURE Level(s: Sema) : CARDINAL;
|
|
|
|
|
(* Returns current value of semaphore s *)
|
|
|
|
|
|
|
|
|
|
PROCEDURE NewSema(n: CARDINAL) : Sema;
|
|
|
|
|
(* Creates a new semaphore with initial level "n" *)
|
|
|
|
|
|
|
|
|
|
PROCEDURE Down(VAR s: Sema);
|
|
|
|
|
(* If the value of "s" is > 0, then just decrement "s".
|
|
|
|
|
Else, suspend the current process until the semaphore becomes
|
|
|
|
|
positive again.
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
PROCEDURE Up(VAR s: Sema);
|
|
|
|
|
(* Increment the semaphore "s".
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
PROCEDURE StartProcess(P: PROC; n: CARDINAL);
|
|
|
|
|
(* Create a new process with procedure P and workspace of size "n".
|
|
|
|
|
Also transfer control to it.
|
|
|
|
|
*)
|
|
|
|
|
END Semaphores.
|
