-------------------------------------------------------------------------------
-- Peterson's mutual exclusion protocol generalized to n processes using locks
-- arranged in a binary tree; the binary tree is optimal if the number of
-- processes is a power of two, but could be specialized otherwise
-------------------------------------------------------------------------------

module peterson_tree (ARCH_TREE) is

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

(*
 * Process P (i) competing for the access to critical section
 *
 *   loop
 *      non critical section ;
 *      A[i] := 1 ;
 *      b := j ;
 *      while A[j] = 1 and b = j do
 *      end while ;
 *      critical section ;
 *      A[i] := 0
 *   end loop
 *)

process acquire [A, C: Operation] (pid: Pid, i, k: Nat) is
   -- instance of Peterson protocol for two processes
   -- variable B is represented by a cell C[k] and the values written to C[k]
   -- are the indexes for variable array A
   -- pid: number of the process
   -- i: own index for variable array A
   -- k: index for variable array C  
   var j, a_j, c_k: Nat in
      -- j: other index for variable array A
      if i mod 2 == 0 then j := i + 1 else j := i - 1 end if; 
      A (Write, i, 1 of Nat, pid);
      C (Write, k, j, pid);
      loop L in
         A (Read, j, ?a_j, pid);
         C (Read, k, ?c_k, pid);
         if not ((a_j == 1) and (c_k == j)) then break L end if
      end loop
   end var
end process

process release [A: Operation] (pid: Pid, i: Nat) is
   A (Write, i, 0 of Nat, pid)
end process

function number_levels : Nat is
   var x: Nat in
      x := N - 1;
      var m: Nat in
         m := 1;
         while x > 1 loop
            m := m + 1;
            x := x div 2
         end loop;
         return m
      end var
   end var
end function

process P [NCS:Pid, CS:Access, A, C:Operation] (pid: Pid) is
   var level, m, d, i, k: Nat in
      loop
         NCS (pid);
         m := 2 * (((N - 1) div 2) + 1);
	 d := 1;
         i := 0;
         k := 0;
         for level := 0 while level < number_levels by level := level + 1 loop
            acquire [A, C] (pid, i + (Nat (pid) div d), k + (Nat (pid) div (2 * d)));
            i := i + m;
            m := m div 2;
	    d := d * 2;
            k := k + m
         end loop;
         CS (Enter, pid); CS (Leave, pid);
         for level := 0 while level < number_levels by level := level + 1 loop
	    d := d div 2;
            m := m * 2;
            i := i - m;            
            release [A] (pid, i + (Nat (pid) div d))
         end loop
      end loop
   end var
end process

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

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

end module