Skip to content

Instantly share code, notes, and snippets.

@raphlinus
Created January 17, 2022 17:57
Show Gist options
  • Save raphlinus/56713074a1a759c18f7d9f21dd706988 to your computer and use it in GitHub Desktop.
Save raphlinus/56713074a1a759c18f7d9f21dd706988 to your computer and use it in GitHub Desktop.
An inconsistent execution exists for this litmus test
NEWWG
NEWSG
NEWTHREAD
st.atom.scopedev.sc0 x = 2
NEWWG
NEWSG
NEWTHREAD
st.atom.scopedev.sc0 x = 1
NEWWG
NEWSG
NEWTHREAD
ld.atom.scopedev.sc0 x = 1
ld.atom.scopedev.sc0 x = 2
SATISFIABLE consistent[X] && #X.dr=0
SATISFIABLE (#RFINIT=0) && (!consistent[X] || #dr>0)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment