Synchronization using control barriers

[hernanponcedeleon]

I am trying to understand why the following test fails (i.e. I get SATISFIABLE)

NEWWG
NEWSG
NEWTHREAD
ld.scopedev.sc0 x = 1
cbar.scopewg 0
NEWTHREAD
cbar.scopewg 0
st.scopedev.sc0 x = 1
UNSATISFIABLE consistent[X]

My understanding is that both threads should synchronize at the control barrier, the load should then be ordered before the store, and thus it should not be able to observe value 1.

I tried playing around with making the memory accesses atomic and adding rel_acq semantics to the barriers, but I still get the same result. Am I missing something?

[jeffbolznv]

Hi,

Maybe try cbar.acq.rel.scopewg.semsc0.

If that doesn't work, I suggest to take the intermediate output and load it up in alloy and it can draw all the edges and that may help you find what's missing.

[hernanponcedeleon]

It took me a while to figure out that if I set the expected result to UNSATISFIABLE, the file build/name.test.gen only contains open spirv, but none of the knowledge coming from the source code of the test.

Once I fix that, I managed to load the model (memory model + program) in alloy and realized the problem was that the load and the store were private and thus, despite the hb, they do not participate in locord. Making them atomic or explicit nonpriv solves the problem.