pcp_rsrc {Semaphore : TYPE; 
          NumberOfTasks : NATURAL, 
          task_descriptors : pcp_task{Semaphore; NumberOfTasks}!TaskDescriptors
         } : CONTEXT =
BEGIN

  taskCtx : CONTEXT = pcp_task{Semaphore; NumberOfTasks};

  semSetCtx : CONTEXT = set{Semaphore;};
  jobSetCtx : CONTEXT = set{taskCtx!JobIdx;};

  Job2SetOfSemaphores : TYPE = ARRAY taskCtx!JobIdx OF semSetCtx!Set;

  % r.alloc[j] is the set of semaphores owned by "j" in "r"
  % r.request[j] is the set of semaphores that "j" requested but has not obtained.
  RSRC : TYPE = [# alloc : Job2SetOfSemaphores, request : Job2SetOfSemaphores #];

  initial_rsrc : RSRC = LET empty_mapping : Job2SetOfSemaphores = [ [j : taskCtx!JobIdx] semSetCtx!empty_set] 
                        IN (# alloc := empty_mapping, request := empty_mapping #);

  % the following array "caches" the ceiling associated with each semaphore.
  ceiling_map : ARRAY Semaphore OF NATURAL =
	  [ [s : Semaphore] taskCtx!ceiling(s, task_descriptors) ];  

  ceiling(s : Semaphore) : NATURAL = ceiling_map[s];
 
  JobIdx : TYPE = taskCtx!JobIdx;

  priority(j : JobIdx) : NATURAL = taskCtx!priority(j, task_descriptors);

  uses_sem?(j : JobIdx, s : Semaphore) : BOOLEAN = taskCtx!uses_sem?(j, s, task_descriptors);

  % returns the set of jobs other than "j" that own a semaphore of ceiling as high as "j"'s priority
  blk(r : RSRC, j : JobIdx) : jobSetCtx!Set =
    LAMBDA (k : JobIdx) : k /= j AND (EXISTS (s : Semaphore): semSetCtx!contains?(r.alloc[k],s) AND ceiling(s) >= priority(j));

  % A job "j" is blocked in "r" if both "blk(r,j)" and "r.request[j]" are nonempty.
  blocked?(r : RSRC, j : JobIdx) : BOOLEAN =
    NOT jobSetCtx!empty?(blk(r, j)) AND NOT semSetCtx!empty?(r.request[j]);

  % alloc_step(r, j, s) executes command "P(s)" on behalf of "j". The semaphore
  % "s" is allocated to "j" if "blk(r, j)" is empty; otherwise, "s" is stored in
  % "r.request[j]" and "j" becomes blocked.
  alloc_step(r : RSRC, j : JobIdx, s : Semaphore) : RSRC =
    IF jobSetCtx!empty?(blk(r, j)) THEN
      r WITH .alloc[j] := semSetCtx!insert(r.alloc[j], s)
    ELSE
      r WITH .request[j] := semSetCtx!insert(r.request[j], s)
    ENDIF;

  % release_step(r, j, s) executes command "V(s)" on behalf of "j". It simply removes
  % "s" from the set of semaphores allocated to "j".
  release_step(r : RSRC, j : JobIdx, s : Semaphore) : RSRC =
    r WITH .alloc[j] := semSetCtx!remove(r.alloc[j], s);

  release_all_step(r : RSRC, j : JobIdx) : RSRC =
    (r WITH .alloc[j] := semSetCtx!empty_set) WITH .request[j] := semSetCtx!empty_set;

  % wakeup(r, j) allocates to "j" all the semaphores "j" requested. This operation is intended
  % for a job "j" that is reactivated after having been blocked.
  wakeup(r : RSRC, j : JobIdx) : RSRC =
    IF r.request[j] /= semSetCtx!empty_set 
    THEN (r WITH .request[j] := semSetCtx!empty_set) WITH .alloc[j] := semSetCtx!union(r.alloc[j], r.request[j])
    ELSE r ENDIF;

END