-------------------------------------------------------------------------------
-- Knuth's mutual exclusion protocol for n processes
-- (N+1 integer variables, complex conditions, starvation-free)
-------------------------------------------------------------------------------

module knuth (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 .. N-1
 *
 *   loop
 *      non critical section ;
 *      loop L1 in
 *         A[i] := 1 ;
 *         loop L2 in
 *            j := B ;
 *            loop L3 in
 *               if j == i then break L2 end if ;
 *               if A[j] != 0 then break L3 end if ;
 *               if j == 0 then
 *                  j := N - 1 ;
 *                  loop L4 in
 *                     if j == i then break L2 end if ;
 *                     if A[j] != 0 then break L3 end if ;
 *                     if j == 0 then break L2 end if ;
 *                     j := j - 1
 *                  end loop
 *               end if ;
 *               j := j - 1
 *            end loop
 *         end loop ;
 *         A[i] := 2 ;
 *         j := N - 1 ;
 *         loop L5 in
 *            if ((j != i) and (A[j] == 2)) then break L5 end if ;
 *            if j == 0 then break L1 end if ;
 *            j := j - 1
 *         end loop 
 *      end loop ;
 *      B := i ;
 *      critical section ;
 *      B := if i == 0 then N - 1 else i - 1 end if ;
 *      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
   loop
      NCS (i);
      loop L1 in
         A (Write, i, 1 of Nat, i);
         loop L2 in
            B (Read, ?b, i);
            j := b of Pid;
            loop L3 in
               if j == i then break L2 end if;
               A (Read, j, ?a_j, i);
               if a_j != 0 then break L3 end if;
               if j == 0 of Pid then
                  j := (N - 1) of Pid;
		  loop L4 in
		     if j == i then break L2 end if;
		     A (Read, j, ?a_j, i);
		     if a_j != 0 then break L3 end if;
		     if j == 0 of Pid then break L2 end if;
		     j := j - 1
		  end loop
	       end if;
               j := j - 1
            end loop
         end loop;
         A (Write, i, 2 of Nat, i);
         j := (N - 1) of Pid;
         loop L5 in
            if j != i then
               A (Read, j, ?a_j, i);
               if a_j == 2 then break L5 end if
            end if;
            if j == 0 of Pid then break L1 end if;
            j := j - 1
         end loop
      end loop;
      B (Write, Nat (i), i);
      CS (Enter, i); CS (Leave, i);
      if i == 0 of Pid then
         B (Write, N - 1, i)
      else
         B (Write, Nat (i - 1), i)
      end if;
      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