Skip to content

Instantly share code, notes, and snippets.

@cartazio
Last active June 17, 2016 16:13
Show Gist options
  • Save cartazio/5b1d3d8dd12b9279866d to your computer and use it in GitHub Desktop.
Save cartazio/5b1d3d8dd12b9279866d to your computer and use it in GitHub Desktop.
state machine for mesi protocol
module MesiModel where
open import Data.Vec
open import Data.Fin
open import Data.Nat
open import Data.Product
data MesiState : Set where
Invalid : MesiState
Modified : MesiState
Exclusive : MesiState
Shared : MesiState
open MesiState
record MesiCommandI : Set where
coinductive
field
LocalReadI : MesiState × MesiCommandI
LocalWriteI : MesiState × MesiCommandI
RemoteReadI : MesiState × MesiCommandI
RemoteWriteI : MesiState × MesiCommandI
open MesiCommandI
denoteMCI : MesiState -> MesiCommandI
LocalReadI (denoteMCI Invalid) = Exclusive , denoteMCI Exclusive
LocalReadI (denoteMCI Modified) = Modified , denoteMCI Modified
LocalReadI (denoteMCI Exclusive) = Exclusive , denoteMCI Exclusive
LocalReadI (denoteMCI Shared) = Shared , denoteMCI Shared -- MesiState × MesiCommandI
LocalWriteI (denoteMCI Invalid) = Modified , denoteMCI Modified
LocalWriteI (denoteMCI Modified) = Modified , denoteMCI Modified
LocalWriteI (denoteMCI Exclusive)= Modified , denoteMCI Modified
LocalWriteI (denoteMCI Shared) = Modified , denoteMCI Modified -- : MesiState × MesiCommandI
RemoteReadI (denoteMCI Invalid) = Invalid , denoteMCI Invalid -- check
RemoteReadI (denoteMCI Modified) = Invalid , denoteMCI Invalid
RemoteReadI (denoteMCI Exclusive) = Shared , denoteMCI Shared
RemoteReadI (denoteMCI Shared) = Shared , denoteMCI Shared -- : MesiState × MesiCommandI
RemoteWriteI (denoteMCI Invalid) = Invalid , denoteMCI Invalid -- check
RemoteWriteI (denoteMCI Modified) = Invalid , denoteMCI Invalid
RemoteWriteI (denoteMCI Exclusive)= Invalid , denoteMCI Invalid
RemoteWriteI (denoteMCI Shared) = Invalid , denoteMCI Invalid -- : MesiState × MesiCommandI
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment