module ARCH_7B (FUNCTIONS, CHANNELS, VARIABLE, VARIABLE_ARRAY, TUPLE_ARRAY, MESI_CACHE) is

-------------------------------------------------------------------------------
-- Architecture of systems communicating by means of 3*N + 1 shared variables, 
-- 3*N of which are represented as the cells a[0], ..., a[N-1], c[0], ..., 
-- c[N-1], and d[0], ..., d[N-1] of three N-variable arrays, the (3*N + 1)th
-- variable being represented by a separate process.
-- The two arrays c and d are grouped, such that the i-th values of both can be
-- read atomically (this is required for instance by the black-white bakery
-- protocol [Taubenfeld-04]).
-------------------------------------------------------------------------------

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

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

process Protocol [NCS: Pid, CS: Access, A, B, C, D: Operation] is
   par A, B, C, D in
      par
         P [NCS, CS, A, B, C, D] (0 of Pid)
       ||
         P [NCS, CS, A, B, C, D] (1 of Pid)
       ||
         P [NCS, CS, A, B, C, D] (2 of Pid)
       ||
         P [NCS, CS, A, B, C, D] (3 of Pid)
       ||
         P [NCS, CS, A, B, C, D] (4 of Pid)
      end par
    ||
      par
         Variable_Array [A] (0 of Nat)
       ||
         Tuple_Array [C, D] (0 of Nat, 0 of Nat)
       ||
         Variable [B] (0 of Nat)
      end par
   end par
end process

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

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