-------------------------------------------------------------------------------
-- Black&White Bakery mutual exclusion protocol [Taubenfeld-04]
-- (7 bits, complex conditions, starvation-free)
-------------------------------------------------------------------------------

module bw_bakery (ARCH_7B) is

!nat_bits 5 -- use 5 bits to store natural numbers

(*
 * Process P (i) competing for the access to critical section
 * where i = 0..N-1, and ca[] and na[] are arrays of local variables
 * required to compute the maximum
 *
 *   loop
 *      non critical section ;
 *      A[i] := 1 ;
 *      C[i] := B ;
 *      for j := 0 to N-1 do
 *         ca[j] := C[j]
 *         na[j] := D[j]
 *      max := 0 ;
 *      for j := 0 to N-1 do
 *         if (ca[j] == C[i]) and (na[j] > max) then
 *            max := na[j]
 *         end if
 *      end for
 *      D[i] := 1 + max ; 
 *      A[i] := 0 ;
 *      for j := 0 to N-1 do
 *         await A[j] = 0 ;
 *         if C[j] == C[i] then
 *            await (D[j] == 0) or ({D[j],j} >= {D[i],i}) or (C[j] != C[i])
 *         else
 *            await (D[j] == 0) or (C[i] != B) or (C[j] == C[i])
 *         end if ;
 *      end for ;
 *      critical section ;
 *      if C[i] = 0 then
 *         B := 1
 *      else
 *         B := 0
 *      end if ;
 *      D[i] := 0
 *   end loop
 *)

process P [NCS:Pid, CS:Access, A, B, C, D:Operation] (i: Pid) is
   var max, j, a_j, b, c_i, c_j, d_i, d_j: Nat in
   loop
      NCS (i);
      A (Write, i, 1 of Nat, i);
      B (Read, ?b, i);
      C (Write, i, b, i);
      C (Read, i, ?c_i, ?d_i, i);
      max := d_i;
      for j := 0 while j < N by j := j + 1 loop
	 if j != i then
	    C (Read, j of Pid, ?c_j, ?d_j, i);
	    if (c_j == c_i) and (d_j > max) then
	       max := d_j
	    end if
	 end if
      end loop;
      d_i := 1 + max;
      D (Write, i, d_i, i);
      A (Write, i, 0 of Nat, i);
      for j := 0 while j < N by j := j + 1 loop
         if (j != i) then
            -- if j == i, the conditions to wait for are all true:
            --  + A[i] has just been assigned 0
            --  + {D[j],j} == {D[i],i} (for j==i)
            -- thus, we optimize to reduce the number of variable accesses
            loop L3 in
               A (Read, j of Pid, ?a_j, i);
               if a_j == 0 then break L3 end if
	    end loop;
            C (Read, j of Pid, ?c_j, ?any Nat, i);
            if c_j == c_i then
               loop L4 in
                  C (Read, j of Pid, ?c_j, ?d_j, i);
                  if (d_j == 0) or
		     ((d_j > d_i) or ((d_j == d_i) and (j >= i))) or
		     (c_j != c_i)
                  then
                     break L4
                  end if
               end loop
            else
               loop L5 in
                  C (Read, j of Pid, ?c_j, ?d_j, i);
                  if (d_j == 0) or (c_j == c_i) then break L5 end if;
                  B (Read, ?b, i);
                  if c_i != b then break L5 end if
               end loop
            end if
         end if
      end loop;
      CS (Enter, i); CS (Leave, i);
      if c_i == 0 then
         B (Write, 1 of Nat, i)
      else
         B (Write, 0 of Nat, i)
      end if;
      D (Write, i, 0 of Nat, i)
   end loop
   end var
end process

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

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

end module