-------------------------------------------------------------------------------
-- MCS: Mellor-Crummey & Scott's locking protocol [MellorCrummey-Scott-91]
-- (4 bits and 1 three-valued shared variable, complex operations (fetch&store,
-- compare&swap))
-------------------------------------------------------------------------------

module mcs (ARCH_4B_Q) is

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

(**
 * hypotheses (applicable to any instance of the MCS protocol) :
 * - each process uses always the same local variable I,
 *   thus one can consider a distributed array I[.]
 * - for N processes, the length of the lock list is at most N
 *   because a process can try to acquire the lock only in its entry section
 *
 * based on these hypotheses and in our particular case of N processes, the
 * queue lock using two arrays and a shared variable
 * - (A[i] == N) iff (I[i].next == nil)
 * - (A[i] == j) iff (I[i].next == &I[j]), for j in { 0 ... N-1 }
 * - (C[i] == 1) iff (I[i].locked == true)
 * - B takes N+1 values :
 *     B == i : the lock is held by process i, for i in { 0 ... N-1 }
 *     B == N : the lock is not held
 *)

(*
 * pseudo-code [MellorCrummey-Scott-91]
 * ------------------------------------
 *
 * type qnode = record
 *    next   : ^qnode
 *    locked : Boolean
 * type lock = ^qnode
 *
 * procedure acquire_lock (L : ^lock, I : ^qnode)
 *    I->next := nil
 *    predecessor : ^qnode := fetch_and_store (L, I)
 *    if predecessor != nil                // queue was non-empty
 *       I->locked := true
 *       predecessor->next := I
 *       repeat while I->locked            // spin
 *
 * procedure release_lock (L : ^lock, I : ^qnode)
 *    if I->next = nil                     // no known successor
 *       if compare_and_swap (L, I, nil)   // true iff swapped 
 *          return
 *       repeat while I->next = nil        // spin
 *    I->next->locked := false
 *)

process acquire_lock [A, B, C: Operation] (i: Pid) is
   var b, c_i: Nat in
      A (Write, i, N, i);
      B (Fetch_and_Store, ?b, Nat (i), i);
      if (b < N) then
         C (Write, i, 1 of Nat, i);
         A (Write, b of Pid, Nat (i), i);
	 loop L in
            C (Read, i, ?c_i, i);
            if (c_i == 0) then break L end if
         end loop
      end if
   end var
end process

process release_lock [A, B, C: Operation] (i: Pid) is
   var a_i: Nat, s: Bool in
      A (Read, i, ?a_i, i);
      if a_i == N then
         B (Compare_and_Swap, Nat (i), N, ?s, i);
	 if s == false then
            loop L in
               A (Read, i, ?a_i, i);
               if (a_i < N) then break L end if
            end loop;
            C (Write, Pid (a_i), 0 of Nat, i)
         end if
      else
         C (Write, Pid (a_i), 0 of Nat, i)
      end if
   end var
end process

process P [NCS: Pid, CS: Access, A, B, C: Operation] (i: Pid) is
   loop
      NCS (i);
      acquire_lock [A, B, C] (i);
      CS (Enter, i); CS (Leave, i);
      release_lock [A, B, C] (i)
   end loop
end process

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

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

end module