Issues with single threaded SPIR-V test

[reeselevine]

I'm investigating some properties of the outcomes of data races in GPU memory models, and I'm interested in seeing what the Vulkan models currently do. Starting with some simple tests, I'm seeing outcomes that seem buggy. I recently opened an issue against the Vulkan Alloy model about this: KhronosGroup/Vulkan-MemoryModel#39

It looks like I'm seeing some of the same behaviors when using Dartagnan. For example, given the following test:

Vulkan test
{
P0:r0=0;
x=0;
}
 P0@sg 0, wg 0, qf 0 ;
 st.av.dv.sc0 x, 1 ;
 ld.vis.dv.sc0 r0, x ;
filter
(P0:r0 == 0)

And running against the default checks (program_spec,cat_spec,liveness), Dartagnan reports this as PASS. However, it seems wrong that r0 should be able to read 0, since x is set to 1 in the same thread.

I realize these are not typical litmus tests, in that they only consider one thread, but I wanted to get some thoughts on these behaviors, as they affect how I can model multi-threaded tests with data races. Or, if I'm doing something wrong in specifying the test, I would appreciate some guidance!

[hernanponcedeleon]

Any particular reason why you are using filter rather than exists?

The former tells dartagan to check the property in those executions satisfying the filtering condition. Since (as you said) no execution should satisfy this condition, the program is trivially correct.

If you use the later dartagan will report FAIL/No. Keep in mind that PASS/FAIL might be counter intuitive depending if the condition is (~)exists/forall. For litmus tests it is easier to check the No/Ok (similar to herd7)

[reeselevine]

Ah I was just pattern matching from the mp-filter test. Using exists it fails, thanks for explaining the difference!