module MESI_CACHE (FUNCTIONS, CHANNELS) is

function all_remote_invalid (pid: Pid, c: Cache) : Bool is
   -- return "true" iff the state of all remote caches is Invalid
   var i: Nat, res: Bool in
      res := true;
      for i := 0 while (i < N) by i := i + 1 loop
         if ((i != pid) and (c[i] != Invalid)) then
            res := false
         end if
      end loop;
      return res
   end var
end function

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

function update_remote (in out c: Cache, pid: Pid, s: Cache_State) is
   -- set the state of all remote caches to s
   var i: Nat in
      for i := 0 while (i < N) by i := i + 1 loop
         if (i != pid) then
            c[i] := s
         end if
      end loop
   end var
end function

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

function update_caches (pid: Pid, s: Operation, in out c: Cache) :
   Cached_Operation 
is
   -- compute the Cache_Signal corresponding to the operation s executed by
   -- process pid and current cache states c0 (cache of process 0) and c1
   -- (cache of process 1) and update the cache states
   var local: Cache_State, Result: Cached_Operation in
      local := c[Nat (pid)];

      case s in
         Read ->
            case local in
               Modified | Exclusive | Shared ->
                  Result := Read_from_Local
             | Invalid ->
                  if all_remote_invalid (pid, c) then
                     Result := Read_from_Memory;
                     c[Nat (pid)] := Exclusive
                  else
                     Result := Read_from_Remote;
                     c[Nat (pid)] := Shared;
                     update_remote (!?c, pid, Shared)
                  end if
            end case
       | Write ->
            case local in
               Modified | Exclusive ->
                  Result := Write_to_Local
             | Shared ->
                  Result := Write_and_Invalidate
             | Invalid ->
                  if all_remote_invalid (pid, c) then
                     Result := Write_and_Fetch
                  else
                     Result := Write_and_Invalidate
                  end if
            end case;
            c[Nat (pid)] := Modified;
            update_remote (!?c, pid, Invalid)
       | Fetch_and_Store ->
            case local in
               Modified | Exclusive ->
                  Result := Fetch_and_Store_local
             | Shared ->
                  Result := Fetch_and_Store_shared
             | Invalid ->
                  if all_remote_invalid (pid, c) then
                     Result := Fetch_and_Store_global
                  else
                     Result := Fetch_and_Store_shared
                  end if
            end case;
            c[Nat (pid)] := Modified;
            update_remote (!?c, pid, Invalid)
       | Compare_and_Swap ->
            case local in
               Modified | Exclusive ->
                  Result := Compare_and_Swap_local
             | Shared ->
                  Result := Compare_and_Swap_shared
             | Invalid ->
                  if all_remote_invalid (pid, c) then
                     Result := Compare_and_Swap_global
                  else
                     Result := Compare_and_Swap_shared
                  end if
            end case;
            c[Nat (pid)] := Modified;
            update_remote (!?c, pid, Invalid)
       | Read_and_Increment ->
            case local in
               Modified | Exclusive ->
                  Result := Read_and_Increment_local
             | Shared ->
                  Result := Read_and_Increment_shared
             | Invalid ->
                  if all_remote_invalid (pid, c) then
                     Result := Read_and_Increment_global
                  else
                     Result := Read_and_Increment_shared
                  end if
            end case;
            c[Nat (pid)] := Modified;
            update_remote (!?c, pid, Invalid)
      end case;
      return Result
   end var
end function

end module