-------------------------------------------------------------------------------
-- Kessels' mutual exclusion protocol optimized for two processes [Kessels-82]
-- (4 bits, starvation-free)
-------------------------------------------------------------------------------

module kessels_2 (ARCH_4B) 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] := 1 ;
 *      C[i] := (C[j] + i) mod 2 ;
 *      repeat until (A[j] == 0) or (C[i] != ((C[j] + i) mod 2)) end repeat ;
 *      critical section ;
 *      A[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A, C:Operation] (i: Pid) is
   var j: Pid, a_j, c_i, c_j:Nat in
   j := 1 - i;
   loop
      NCS (i);
      A (Write, i, 1 of Nat, i);
      C (Read, j, ?c_j, i);
      C (Write, i, (c_j + Nat (i)) mod 2, i);
      loop L in
         A (Read, j, ?a_j, i);
         C (Read, i, ?c_i, i);
         C (Read, j, ?c_j, i);
         if (a_j == 0) or (c_i != ((c_j + Nat (i)) mod 2)) then break L end if
      end loop;
      CS (Enter, i); CS (Leave, i);
      A (Write, i, 0 of Nat, i)
   end loop
   end var
end process

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

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

end module