-------------------------------------------------------------------------------
-- Mutual exclusion protocol 3b_p1
-- (3 bits, simple conditions, starvation-free)
-- generated automatically in [Bar-David-Taubenfeld-03]
-------------------------------------------------------------------------------

module mutex_3b_p1 (ARCH_3B) is

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

(*
 * Process P (i) competing for the access to critical section
 * where i = 0..1, j = 1 - i
 *
 *   loop
 *      non critical section ;
 *      A[i] := j ;
 *      if B = j then
 *         B := i ;
 *         while B = A[j] do
 *         end while ;
 *      end if ;
 *      critical section ;
 *      A[i] := i
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A, B:Operation] (i: Pid) is
   var j: Pid, a_0, a_j, b:Nat in
   j := 1 - i;
   loop
      NCS (i);
      A (Write, i, Nat (j), i);
      B (Read, ?b, i);
      if b == j then
         B (Write, Nat (i), i);
         loop L in
            B (Read, ?b, i);
            A (Read, j, ?a_j, i);
            if b != a_j then break L end if
         end loop
      end if;
      CS (Enter, i); CS (Leave, i);
      A (Write, i, Nat (i), i)
   end loop
   end var
end process

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

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

end module