-------------------------------------------------------------------------------
-- Test-test-and-set exclusion protocol using only one bit (resource free or
-- not)
-- (1 variable, complex operations)
-------------------------------------------------------------------------------

module ttas (ARCH_1Q) is

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

(*
 * Process P (i) competing for the access to critical section
 * where i = 0 .. N-1
 *
 *   loop
 *      non critical section ;
 *      await ((B == 0) and_then Compare_and_Swap (B, 0, 1)) ;
 *      critical section ;
 *      B := j
 *   end loop
 *)

process P [NCS:Pid, CS:Access, B:Operation] (i:Pid) is
   var b: Bool, bv: Nat in
   loop
      NCS (i);
      loop L in
	 B (Read, ?bv, i);
	 if bv == 0 then
            B (Compare_and_Swap, 0 of Nat, 1 of Nat, ?b, i);
            if b then break L end if
	 end if
      end loop;
      CS (Enter, i); CS (Leave, i);
      B (Write, 0 of Nat, i)
   end loop
   end var
end process

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

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

end module