<div dir="ltr">Hey all,<div>I wrote a toy model of the CPU MESI cacheline protocol in agda using copatterns/coinduction, it turned out super nice! figured y&#39;all  would enjoy it</div><div><br></div><div>i&#39;ve included it inline below, and a github gist here <a href="https://gist.github.com/cartazio/5b1d3d8dd12b9279866d">https://gist.github.com/cartazio/5b1d3d8dd12b9279866d</a></div><div><br></div><div><div>module MesiModel where</div><div><br></div><div>open import Data.Vec</div><div>open import Data.Fin</div><div>open import Data.Nat</div><div>open import Data.Product</div><div><br></div><div><br></div><div>data MesiState : Set where</div><div>  Invalid   : MesiState</div><div>  Modified   : MesiState</div><div>  Exclusive : MesiState</div><div>  Shared    : MesiState</div><div>open MesiState</div><div><br></div><div><br></div><div><br></div><div>record MesiCommandI  : Set where</div><div>      coinductive              </div><div>      field</div><div>        LocalReadI   : MesiState  ×  MesiCommandI </div><div>        LocalWriteI  :  MesiState  ×  MesiCommandI</div><div>        RemoteReadI  :  MesiState  ×  MesiCommandI</div><div>        RemoteWriteI :  MesiState  ×  MesiCommandI</div><div><br></div><div><br></div><div>open MesiCommandI</div><div><br></div><div>denoteMCI : MesiState -&gt; MesiCommandI</div><div>LocalReadI (denoteMCI Invalid)  = Exclusive  , denoteMCI Exclusive</div><div>LocalReadI (denoteMCI Modified)  = Modified  , denoteMCI Modified</div><div>LocalReadI (denoteMCI Exclusive) = Exclusive , denoteMCI Exclusive</div><div>LocalReadI (denoteMCI Shared) = Shared , denoteMCI Shared  -- MesiState  ×  MesiCommandI</div><div><br></div><div>LocalWriteI (denoteMCI Invalid)  = Modified , denoteMCI Modified</div><div>LocalWriteI (denoteMCI Modified) = Modified , denoteMCI Modified</div><div>LocalWriteI (denoteMCI Exclusive)= Modified , denoteMCI Modified</div><div>LocalWriteI (denoteMCI Shared) =   Modified , denoteMCI Modified   -- :  MesiState  ×  MesiCommandI</div><div><br></div><div>RemoteReadI (denoteMCI Invalid)  = Invalid , denoteMCI Invalid -- check</div><div>RemoteReadI (denoteMCI Modified) = Invalid , denoteMCI Invalid</div><div>RemoteReadI (denoteMCI Exclusive) = Shared , denoteMCI Shared</div><div>RemoteReadI (denoteMCI Shared)    = Shared , denoteMCI Shared  -- :  MesiState  ×  MesiCommandI</div><div><br></div><div>RemoteWriteI (denoteMCI Invalid) =  Invalid , denoteMCI Invalid -- check</div><div>RemoteWriteI (denoteMCI Modified) = Invalid , denoteMCI Invalid</div><div>RemoteWriteI (denoteMCI Exclusive)= Invalid , denoteMCI Invalid</div><div>RemoteWriteI (denoteMCI Shared) =   Invalid , denoteMCI Invalid -- :  MesiState  ×  MesiCommandI</div></div><div><br></div></div>