-------------------------------------------------------------------------------
-- Anderson's array based-queue lock [Anderson-90]
-------------------------------------------------------------------------------

module anderson (ARCH_3B_A) is

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

(*
 * pseudo-code [Anderson-90]
 * -------------------------
 *
 * Init :   A[0] := 1
 *
 * Lock :   C[i] := Read_and_Increment (B) ;
 *          wait until (A[C[i] mod n] == 1) ;
 *          A[C[i] mod n] := 0
 *
 * Unlock : A[(C[i] + 1) mod n] := 1
 *)

process P [NCS: Pid, CS: Access, A, B: Operation] (i: Pid) is
   if i == 0 of Pid then
      -- initialization (exactly one process has access to the lock)
      A (Write, 0 of Pid, 1 of Nat, i)
   end if;
   var b: Pid, a_b: Nat in
      loop
         NCS (i);
         B (Read_and_Increment, ?b, i);
         -- the following assignment is already performed by process QUEUE 
         -- b := b mod n
         loop L in
            A (Read, b, ?a_b, i);
            if a_b == 1 then break L end if
         end loop;
         A (Write, b, 0 of Nat, i);
         CS (Enter, i); CS (Leave, i);
         A (Write, ((Nat (b) + 1) mod N) of Pid, 1 of Nat, i)
      end loop
   end var
end process

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

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

end module