[RFC] Formal model written in cat and tool support for simulation

[tonghaining]

Together with @hernanponcedeleon, we wrote the vulkan model in the cat language (a standard language to formalize memory models), ported all the tests in this repository to a more standardized format, and added tool support for simulation/verification.

We believe the tool would be valuable for the community and we wanted to get feedback if it would make sense to have the model and the tests in this repository.

The new tool has the following advantages

• it supports goto instructions which allow to write more realistic examples e.g. the XF-barrier.
• it also supports the Nvidia's PTX model, meaning that it can be used to compare how the same program (modulo ISA syntax) behaves according to the different notions of consistency.
• it scales much better than Alloy-based tools. For litmus tests scalability might not be an issue, but it could be used to verify more realistic code.
• it allows to find certain liveness violations due to spinloops not synchronizing correctly.

[hernanponcedeleon]

The possibility to find liveness bugs is probably the main advantage of what we propose wrt to alloy model. Let me give some details about this.

While one may think that axiomatic memory models (based on finite executions) cannot be used to define liveness properties, this is wrong. The theory that allows to do this is explained in this paper.

The overall idea is as follows: if there is a load coming from a spinloop which reads from a coherence-last write and the read value does not break the spinning, a liveness violation has been found.

The XF-Barrier (an inter-workgroup execution barrier) mentioned above can deadlock if there is no proper synchronization.

> cat litmus/VULKAN/Manual/XF-Barrier-weak.litmus 
Vulkan XF-Barrier-weak
{
x=0;
f=0;
P0:r0=0;
P1:r0=0;
}
 P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ;
 st.av.dv.sc0 x, 1   | cbar.wg 1           | cbar.wg 1           ;
 LC00:               | st.dv.sc0 f, 1      | cbar.wg 2           ;
 ld.dv.sc0 r2, f     | LC10:               |                     ;
 bne r2, 0, LC01     | ld.dv.sc0 r2, f     |                     ;
 goto LC00           | bne r2, 1, LC11     |                     ;
 LC01:               | goto LC10           |                     ;
 cbar.wg 1           | LC11:               |                     ;
 st.dv.sc0 f, 0      | cbar.wg 2           |                     ;
                     | ld.vis.dv.sc0 r1, x |                     ;

> java -jar dartagnan/target/dartagnan.jar cat/spirv.cat --target=vulkan --method=assume litmus/VULKAN/Manual/XF-Barrier-weak.litmus --property=liveness --witness.graphviz=true
...
[31.10.2023] 10:34:06 [INFO] AssumeSolver.run - Verification finished with result FAIL
Total verification time(ms): 887

Below we can see an execution leading to a liveness violation. Event E18 (bottom right) reads from the co-maximal write E16, but with this value, it would continue spinning.

The issue is not just a deadlock, but also that the execution has a data race. Both problems can be solved by making some of the memory accesses atomic.

> cat litmus/VULKAN/Manual/XF-Barrier-relacq.litmus 
Vulkan XF-Barrier-relacq
{
x=0;
f=0;
P0:r0=0;
P1:r0=0;
}
 P0@sg 0, wg 0, qf 0             | P1@sg 0, wg 1, qf 0             | P2@sg 0, wg 1, qf 0 ;
 st.av.dv.sc0 x, 1               | cbar.wg 1                       | cbar.wg 1           ;
 LC00:                           | st.atom.dv.sc0 f, 1             | cbar.wg 2           ;
 ld.atom.dv.sc0 r2, f            | LC10:                           |                     ;
 bne r2, 0, LC01                 | ld.atom.acq.dv.sc0.semsc0 r2, f |                     ;
 goto LC00                       | bne r2, 1, LC11                 |                     ;
 LC01:                           | goto LC10                       |                     ;
 cbar.wg 1                       | LC11:                           |                     ;
 st.atom.rel.dv.sc0.semsc0 f, 0  | cbar.wg 2                       |                     ;
                                 | ld.vis.dv.sc0 r1, x             |                     ;