module ARCH_3B_Q (FUNCTIONS, CHANNELS, QUEUE, MEMORY, MESI_CACHE) is

-------------------------------------------------------------------------------
-- Architectures of systems communicating by means of a queue and N+1 shared
-- memory locations. The N+1 shared memory locations are represented as the
-- cells a[0], ..., a[N]. The queue is represented by a shared variable with
-- operations fetch_and_store (and compare_and_swap).
-------------------------------------------------------------------------------

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

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

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

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

process L [NCS: Pid, CS: Access, A, B: Operation, MU: Latency] is
   var
      a: Cache_Array,
      a_i, a_n, b: Cache,
      index: Nat,
      pid: Pid,
      acc: Access,
      op: Operation,
      cop: Cached_Operation
   in
      a   := cache_array (cache (Invalid));
      a_n := cache (Invalid);
      b   := cache (Invalid);
      loop
         alt
            A (?op, ?index, ?any Nat, ?pid) where index < N;
            a_i := a[index];
            cop := update_caches (pid, op, !?a_i);
            a[index] := a_i;
            MU (cop, pid)
          []
            A (?op, N, ?any Nat, ?pid);
            cop := update_caches (pid, op, !?a_n);
            MU (cop, pid)
          []
            B (?op, ?any Nat, ?any Nat, ?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