-------------------------------------------------------------------------------
-- Burns & Lynch mutual exclusion protocol for 2 processes
-- (2 bits, simple conditions, deadlock-free)
-- simplified version of [Burns-Lynch-80]
-------------------------------------------------------------------------------

module burns_lynch (ARCH_2B) 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 ;
 *      loop L1 in
 *         A[i] := 0 ;
 *         j := 0 ;
 *         loop L2 in
 *            if j < i then
 *               if A[j] == 1 then break L2 end if ;
 *               j := j + 1
 *            else
 *               A[i] := 1 ;
 *               j := 0 ;
 *               loop L3 in
 *                  if j == i then break L1 end if ;
 *                  if A[j] == 1 then break L3 end if ;
 *                  j := j + 1
 *               end loop
 *            end if
 *         end loop
 *      end loop ;
 *      loop L4 in
 *         j := i + 1 ;
 *         loop L5 in
 *            if j == N then break L4 end if ;
 *            if A[j] == 1 then break L5 end if ;
 *            j := j + 1
 *         end loop
 *      end loop ;
 *      critical section ;
 *      A[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A:Operation] (i: Pid) is
   var j: Nat, a_j: Nat in
   loop
      NCS (i);
      loop L1 in
         A (Write, i, 0 of Nat, i); -- really necessary ???
         j := 0;
         loop L2 in
            if j < i then
               A (Read, j of Pid, ?a_j, i);
               if a_j == 1 then break L2 end if;
               j := j + 1
            else
               A (Write, i, 1 of Nat, i);
               j := 0;
               loop L3 in
                  if j == i then break L1 end if;
                  A (Read, j of Pid, ?a_j, i);
                  if a_j == 1 then break L3 end if;
                  j := j + 1
               end loop
            end if
         end loop
      end loop;
      loop L4 in
         j := Nat (i) + 1;
         loop L5 in
            if j == N then break L4 end if;
            A (Read, j of Pid, ?a_j, i);
            if a_j == 1 then break L5 end if;
            j := j + 1
         end loop
      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:Operation, MU:Latency] is
   Arch_2b [NCS, CS, A, MU]
end process

end module