module ARCH_1Q (FUNCTIONS, CHANNELS, QUEUE, MESI_CACHE, VIRTUAL) is

-------------------------------------------------------------------------------
-- Architecture of systems communicating by means of one single shared bit,
-- represented by a process QUEUE, and modifiable by atomic compare-and-swap
-- operations.
-------------------------------------------------------------------------------

process Arch_1q [NCS: Pid, CS: Access, B: Operation, MU: Latency] is
   par NCS, CS, B in
      Protocol [NCS, CS, B]
    ||
      L [NCS, CS, B, MU]
   end par
end process

-------------------------------------------------------------------------------
-- Auxiliary process for compositional generation: protocol without latencies
-------------------------------------------------------------------------------

process Protocol [NCS: Pid, CS: Access, B: Operation] is
   par B in
      par
         P [NCS, CS, B] (0 of Pid)
       ||
         P [NCS, CS, B] (1 of Pid)
       ||
         P [NCS, CS, B] (2 of Pid)
       ||
         P [NCS, CS, B] (3 of Pid)
      end par
    ||
      Queue [B] (0 of Nat)
   end par
end process

-------------------------------------------------------------------------------
-- Auxiliary process for inserting latencies
-------------------------------------------------------------------------------

process L [NCS: Pid, CS: Access, B: Operation, MU: Latency] is
   var b: Cache, pid: Pid, acc: Access, op: Operation, cop: Cached_Operation in
      b := Cache (Invalid);
      loop
         alt
            B (?op, ?any Nat, ?pid);
            cop := update_caches (pid, op, !?b);
            MU (cop, pid)
	 []  
	    B (?op, ?any Nat, ?any Nat, ?any Bool, ?pid);
            cop := update_caches (pid, op, !?b);
            MU (cop, pid)
         []
            CS (?acc, ?pid);
            if acc == Enter then
               MU (acc, pid)
            end if
         []
            NCS (?pid);
            MU (Work, pid)
         end alt
      end loop
   end var
end process

end module