-------------------------------------------------------------------------------
-- Lamport's fast mutual exclusion protocol [Lamport-87, Fig. 2]
-- (4 bits, simple conditions, starvation-free)
-------------------------------------------------------------------------------

module lamport (ARCH_4B) 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
 *         A[i] := 1 ;
 *         C[0] := i ;
 *         if C[1] != 0 then
 *            A[i] := 0 ;
 *            while C[1] != 0 do
 *            end while
 *         else
 *            C[1] := i + 1;
 *            if C[0] != i then
 *               A[i] := 0 ;
 *               for j := 0 to N-1 do
 *                  await A[j] == 0
 *               end for
 *               if C[1] != (i + 1) then
 *                  while C[1] != 0 do
 *                  end while
 *               else
 *                  break
 *               end if
 *            else
 *               break
 *            end if
 *         end if
 *      end loop ;
 *      critical section ;
 *      C[1] := 0 ;
 *      A[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A, C:Operation] (i: Pid) is
   var j, a_j, c_0, c_1: Nat in
   loop
      NCS (i);
      loop L1 in
         A (Write, i, 1 of Nat, i);
         C (Write, 0 of Pid, Nat (i), i);
         C (Read, 1 of Pid, ?c_1, i);
         if c_1 != 0 then
            A (Write, i, 0 of Nat, i);
            loop L2 in
               C (Read, 1 of Pid, ?c_1, i);
               if c_1 == 0 then break L2 end if
            end loop
         else
            C (Write, 1 of Pid, Nat (i) + 1, i);
            C (Read, 0 of Pid, ?c_0, i);
            if c_0 != i then
               A (Write, i, 0 of Nat, i);
               for j := 0 while j < N by j := j + 1 loop
                  if j != Nat (i) then
                     -- because A[i] is written only by process i and has just
                     -- been assigned 0, the pseudo-code above can be optimized
                     -- by avoiding to wait for A[i] to become 0 ; this avoids
                     -- one access to a shared variable
                     loop L4 in
                        A (Read, j of Pid, ?a_j, i);
                        if a_j == 0 then break L4 end if
                     end loop
                  end if
               end loop;
               C (Read, 1 of Pid, ?c_1, i);
               if c_1 != (Nat (i) + 1) then
                  loop L4 in
                     C (Read, 1 of Pid, ?c_1, i);
                     if c_1 == 0 then break L4 end if
                  end loop
               else
                  break L1
               end if
            else
               break L1
            end if
         end if
      end loop ;
      CS (Enter, i); CS (Leave, i);
      C (Write, 1 of Pid, 0 of Nat, 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