-------------------------------------------------------------------------------
-- Peterson's mutual exclusion protocol for n processes
-- (starvation-free)
-------------------------------------------------------------------------------

module peterson (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;
 *      for j = 1 to n-1 do
 *         A[i] := j;
 *         C[j] := i;
 *         wait until (forall k != i, A[k] < j) or (C[j] != i)
 *      done
 *      critical section;
 *      A[i] := 0;
 *   end loop
 *)

process P [NCS: Pid, CS: Access, A, C: Operation] (i: Pid) is
var j, k, c_j, a_k: Nat, ok: Bool in
   loop
      NCS (i);
      for j := 1 while j < N by j := j + 1 loop
         A (Write, i, j, i);
         C (Write, Pid (j), Nat (i), i);
         loop L in
            C (Read, Pid (j), ?c_j, i);
            if (c_j != i) then
               break L
            end if;
            ok := true;
            k := 0;
            while k < n loop
               if (k != i) then
                  A (Read, Pid (k), ?a_k, i);
		     if (a_k >= j) then
                     ok := false
                  end if
               end if;
               k := k + 1
            end loop;
            if (ok == true) then
               break L
            end if
         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, C: Operation, MU: Latency] is
   Arch_4b [NCS, CS, A, C, MU]
end process

end module