-------------------------------------------------------------------------------
-- Dekker's mutual exclusion protocol [Dijkstra-65]
-- (3 bits, complex conditions, starvation-free)
-------------------------------------------------------------------------------

module dekker (ARCH_3B) is

!nat_bits 6 -- use 6 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] := 1 ;
 *      while A[j] = 1 do
 *         if B != i then
 *            A[i] := 0 ;
 *            while B != i do
 *            end while ;
 *            A[i] := 1
 *         end if
 *      end while ;
 *      critical section ;
 *      B := j ;
 *      A[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A, B:Operation] (i: Pid) is
   var j: Pid, a_j, b:Nat in
   j := 1 - i;
   loop
      NCS (i);
      A (Write, i, 1 of Nat, i);
      loop L1 in
         A (Read, j, ?a_j, i);
         if a_j != 1 then break L1 end if;
         B (Read, ?b, i);
         if b != i then
            A (Write, i, 0 of Nat, i);
            loop L2 in
               B (Read, ?b, i);
               if b == i then break L2 end if
            end loop;
            A (Write, i, 1 of Nat, i)
         end if
      end loop;
      CS (Enter, i); CS (Leave, i);
      B (Write, Nat (j), i);
      A (Write, i, 0 of Nat, 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