-------------------------------------------------------------------------------
-- CLH: protocol simultaneously discovered by Craig [Craig-93] and Landin & 
-- Hagersten [Magnusson-Landin-Hagersten-94]
-------------------------------------------------------------------------------

module clh (ARCH_3B_Q) is

!nat_bits 6 -- use 6 bits to store natural numbers

(*
 * pseudo-code [Magnusson-Landin-Hagersten-94]
 * -------------------------------------------
 *
 * acquire (int **L, **I, **P) {
 *    **I = 1;
 *    atomic { *P = *L; *L = *I; }
 *    while (**P != 0) /* spin */ ;
 * }
 *
 * release (int **I, **P) {
 *    **I = 0;
 *    *I = *P;
 * }
 *)

process acquire [M, Q: Operation] (id: Pid, j: Nat, out var p: Nat) is
   var n: Nat in
      M (Write, j, 1 of Nat, id);
      Q (Fetch_and_Store, ?p, j, id);
      loop L in
         M (Read, p, ?n, id);
         if (n == 0) then break L end if
      end loop
   end var
end process

process release [M: Operation] (id: Pid, in out j: Nat, p: Nat) is
   M (Write, j, 0 of Nat, id);
   j := p
end process

process P [NCS: Pid, CS: Access, M, Q: Operation] (id: Pid, in var j: Nat) is
   var p: Nat in
      loop
         NCS (id);
         acquire [M, Q] (id, j, ?p);
         CS (Enter, id); CS (Leave, id);
         release [M] (id, !?j, p)
      end loop
   end var
end process

-------------------------------------------------------------------------------

process Main [NCS: Pid, CS: Access, A, B: Operation, MU: Latency] is
   Arch_3b_q [NCS, CS, A, B, MU]
end process

end module