Add Vulkan Memory Model Support to Dartagnan (hernanponcedeleon#516)

Co-authored-by: Hernan Ponce de Leon <[email protected]>

README.md

@@ -99,6 +99,7 @@ For programs written in `.c` and `.bpl`, value `<arch>` specifies the programmin
 - arm8
 - riscv
 - ptx
+- vulkan
 
 The target architecture is supposed to match (this is responsibility of the user) the intended weak memory model specified by the CAT file. 
 

cat/spirv-check.cat

@@ -0,0 +1,220 @@
+SPIRV
+(* Vulkan + SPIR-V Memory Model *)
+(* This file is not intended for verification purposes, but rather to perform several sanity checks *)
+
+// Base relations:
+// vloc: events accessing the same virtual location, aka "same reference (sref)" in the Vulkan spec
+// syncbar: synchronize by barriers with same logical barrier resource (barID)
+// ssg: same subgroup
+// swg: same workgroup
+// sqf: same queuefamily
+// ssw: system-synchronizes-with
+
+// Tags:
+// SC0, SC1: storage class 0, 1
+// SEMSC0, SEMSC1: storage class semantics 0. 1
+// SG, WG, QF, DV: subgroup, workgroup, queuefamily, device domains
+// AV, VIS: availability, visibility
+// AVDEVICE, VISDEVICE: availability, visibility op to the device domain
+
+(*******************)
+(*  Auxiliaries *)
+(*******************)
+
+(* Tags *)
+let PRIV = (R | W) \ NONPRIV // PRIV is the complement of NONPRIV
+
+let SEMSC01 = SEMSC0 & SEMSC1
+
+let AVSHADER = (AV | SEMAV) & DV
+let VISSHADER = (VIS | SEMVIS) & DV
+
+let AVQF = (AV | SEMAV) & (DV | QF)
+let VISQF = (VIS | SEMVIS) & (DV | QF)
+
+let AVWG = (AV | SEMAV) & (DV | QF | WG)
+let VISWG = (VIS | SEMVIS) & (DV | QF | WG)
+
+let AVSG = AV | SEMAV
+let VISSG = VIS | SEMVIS
+
+(* Relations *)
+let inscope = (DV * DV) |
+              (sqf & ((DV | QF) * (DV | QF))) |
+              (swg & ((DV | QF | WG) * (DV | QF | WG))) |
+              (ssg & ((DV | QF | WG | SG) * (DV | QF | WG | SG)))
+
+let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id // mutually ordered atomics
+
+let avvisSem = ((SC0 | SC1) * (AVDEVICE | VISDEVICE))
+                | (SC0 * ((SEMAV | SEMVIS) & SEMSC0))
+                | (SC1 * ((SEMAV | SEMVIS) & SEMSC1))
+let avvisSet = [AV | VIS]; (vloc & loc)
+let avvisinc = ((avvisSem | avvisSem^-1) \ id) |
+               (avvisSet | avvisSet^-1)
+
+let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po
+let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po
+
+let asmo = co & (ATOM * ATOM)
+let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
+let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
+
+// synchronizes-with is similar to C++, with an additional case for fence->cbar->cbar->fence
+let sw = inscope & (
+    ([REL & ATOM]; rs; (rf & mutordatom); [ACQ & ATOM]) |                                               // atomic->atomic
+    ([REL & F]; posemtosc; [ATOM & W]; hypors; (rf & mutordatom); [ACQ & ATOM]) |                       // fence->atomic
+    ([REL & ATOM]; rs; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) |                           // atomic->fence
+    ([REL & F]; posemtosc; [ATOM & W]; hypors; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) |   // fence->fence
+    // (stor[CBAR]) terms are redundant because scbarinst is an equivalence relation on scbarinst, but they make the sequence of instructions more clear.
+    ([REL & F]; po?; [CBAR]; ((syncbar & inscope) \ id); [CBAR]; po?; [ACQ & F])                        // fence->cbar->cbar->fence,
+)
+
+let ithbsemsc0 = ( ssw |
+                   ([SEMSC0]; sw; [SEMSC0]) |
+                   ([SC0 | SEMSC0]; po; [REL & SEMSC0]) |
+                   ([ACQ & SEMSC0]; po; [SC0 | SEMSC0])
+                 )+
+let ithbsemsc1 = ( ssw |
+                   ([SEMSC1]; sw; [SEMSC1]) |
+                   ([SC1 | SEMSC1]; po; [REL & SEMSC1]) |
+                   ([ACQ & SEMSC1]; po; [SC1 | SEMSC1])
+                 )+
+let ithbsemsc01 = ( ssw |
+                   ([SEMSC01]; sw; [SEMSC01]) |
+                   ([SC0 | SC1 | SEMSC01]; po; [REL & SEMSC01]) |
+                   ([ACQ & SEMSC01]; po; [SC0 | SC1 | SEMSC01])
+                 )+
+
+// happens-before
+let hb = ithbsemsc0 | ithbsemsc1 | ithbsemsc01 | po
+
+// chains will produce the availability/visibility chains with this pattern:
+let E = (M | F | CBAR | AVDEVICE | VISDEVICE) \ IW
+let chains = E * E
+
+let avsg = [AVSG]
+let avwg = (chains & (avsg; (hb & ssg & avvisinc))?); [AVWG]
+let avqf = (chains & ((avsg; (hb & ssg & avvisinc))? ; (avwg; (hb & swg & avvisinc))?)); [AVQF]
+let avsh = (chains & ((avsg; (hb & ssg & avvisinc))? ; (avwg; (hb & swg & avvisinc))?; (avqf; (hb & sqf & avvisinc))?)); [AVSHADER]
+let avdv = [AVDEVICE]
+
+let vissg = [VISSG]
+let viswg = [VISWG]; (chains & (((hb & ssg & avvisinc); vissg)?))
+let visqf = [VISQF]; (chains & (((hb & swg & avvisinc) ; viswg)?; ((hb & ssg & avvisinc); vissg)?))
+let vissh = [VISSHADER]; (chains & (((hb & sqf & avvisinc) ; visqf)?; ((hb & swg & avvisinc); viswg)?; ((hb & ssg & avvisinc); vissg)?))
+let visdv = [VISDEVICE]
+
+// loc order, relates memory accesses to the same location
+let locord = loc &
+             (  (hb & int & vloc) |
+                ([R \ PRIV]; hb; [(R | W) \ PRIV]) | // RaR, WaR (non-private)
+                ([R]; ssw+; [R | W]) | // RaR, WaR (any)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsg; (hb & ssg);                          [W \ PRIV])) |   // WaW (via subgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsg; (hb & ssg); vissg; (po? & avvisinc); [R \ PRIV])) |   // RaW (via subgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avwg; (hb & swg);                          [W \ PRIV])) |   // WaW (via subgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avwg; (hb & swg); viswg; (po? & avvisinc); [R \ PRIV])) |   // RaW (via workgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avqf; (hb & sqf);                          [W \ PRIV])) |   // WaW (via queue family instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avqf; (hb & sqf); visqf; (po? & avvisinc); [R \ PRIV])) |   // RaW (via queue family instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsh; (hb);                                [W \ PRIV])) |   // WaW (via shader domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsh; (hb);       vissh; (po? & avvisinc); [R \ PRIV])) |   // RaW (via shader domain)
+                (       ([W];        (hb & avvisinc);  avdv; (hb);                                [W]))        |   // WaW (via device domain)
+                (       ([W];        (hb & avvisinc);  avdv; (hb);       visdv; (hb & avvisinc);  [R]))            // RaW (via device domain)
+             )
+
+let w-locord = [W]; locord
+
+// visible to = location ordered W->R with no intervening write (W->W->R)
+let visto = (w-locord \ (w-locord; w-locord+)); [R]
+
+(**************************)
+(* Sanity checks for tags *)
+(**************************)
+
+// RMW atomics in A
+let rmwIsAtomic = ([RMW] \ [ATOM])
+flag ~empty rmwIsAtomic as checkRmwIsAtomic
+
+// Atomics are reads and writes, not fences
+let atomicIsRW = ([ATOM] \ [R | W])
+flag ~empty atomicIsRW as checkAtomicIsRW
+
+// acquire can be used on atomic reads or fences
+let acqIsRF = ([ACQ] \ [(R & ATOM) | F])
+flag ~empty acqIsRF as checkAcqIsRF
+
+// releases can be used on atomic writes or fences
+let relIsWF = ([REL] \ [(W & ATOM) | F])
+flag ~empty relIsWF as checkRelIsWF
+
+// Fences must release or acquire
+let fIsRelAcq = ([F] \ [REL | ACQ])
+flag ~empty fIsRelAcq as checkFIsRelAcq
+
+// Only writes/reads can have explicit availability/visibility ops, respectively
+let avIsRW = ([AV] \ [W])
+flag ~empty avIsRW as checkAvIsRW
+let visIsRW = ([VIS] \ [R])
+flag ~empty visIsRW as checkVisIsRW
+
+// nonpriv is only meaningful for memory accesses
+let nonprivIsRW = ([NONPRIV] \ [R | W])
+flag ~empty nonprivIsRW as checkNonprivIsRW
+
+// Atomic operations are always considered non-private
+let atomicIsNonpriv = ([ATOM] \ [NONPRIV])
+flag ~empty atomicIsNonpriv as checkAtomicIsNonpriv
+
+// Atomic operations implicitly have availability/visibility operations
+let atomicIsAv = ([W & ATOM] \ [AV])
+flag ~empty atomicIsAv as checkAtomicIsAv
+let atomicIsVis = ([R & ATOM] \ [VIS])
+flag ~empty atomicIsVis as checkAtomicIsVis
+
+// availability/visibility semantics in REL/ACQ only, respectively
+let semavIsRel = ([SEMAV] \ [REL])
+flag ~empty semavIsRel as checkSemAvIsRel
+let semvisIsAcq = ([SEMVIS] \ [ACQ])
+flag ~empty semvisIsAcq as checkSemVisIsAcq
+
+// acquire/release ops have one or more semantics storage classes
+let acqIsSem = ([ACQ] \ [SEMSC0 | SEMSC1])
+flag ~empty acqIsSem as checkAcqIsSem
+let relIsSem = ([REL] \ [SEMSC0 | SEMSC1])
+flag ~empty relIsSem as checkRelIsSem
+
+// no pair of the same control barrier instance can be in the same thread
+let scbarinstIsPo = (syncbar & (po | po^-1))
+flag ~empty scbarinstIsPo as checkScbarinstIsPo
+
+// can't have two cbars where one comes first in po in one thread and second in po in another thread
+let scbarinstIsPo2 = (syncbar & (po; syncbar; po) & syncbar)
+flag ~empty scbarinstIsPo2 as checkScbarinstIsPo2
+
+// the same instance of a control barrier must have same scope, acq/rel, semantics
+let scbarinstIsDV = (syncbar & (DV * (_ \ DV)))
+flag ~empty scbarinstIsDV as checkScbarinstIsDV
+let scbarinstIsQF = (syncbar & (QF * (_ \ QF)))
+flag ~empty scbarinstIsQF as checkScbarinstIsQF
+let scbarinstIsWG = (syncbar & (WG * (_ \ WG)))
+flag ~empty scbarinstIsWG as checkScbarinstIsWG
+let scbarinstIsSG = (syncbar & (SG * (_ \ SG)))
+flag ~empty scbarinstIsSG as checkScbarinstIsSG
+let scbarinstIsAcq = (syncbar & (ACQ * (_ \ ACQ)))
+flag ~empty scbarinstIsAcq as checkScbarinstIsAcq
+let scbarinstIsRel = (syncbar & (REL * (_ \ REL)))
+flag ~empty scbarinstIsRel as checkScbarinstIsRel
+let scbarinstIsSemsc0 = (syncbar & (SEMSC0 * (_ \ SEMSC0)))
+flag ~empty scbarinstIsSemsc0 as checkScbarinstIsSemsc0
+let scbarinstIsSemsc1 = (syncbar & (SEMSC1 * (_ \ SEMSC1)))
+flag ~empty scbarinstIsSemsc1 as checkScbarinstIsSemsc1
+
+(*******************************)
+(* Sanity checks for relations *)
+(*******************************)
+
+// assert AssertLocordSameLoc { all X : Exec | X.locord in X.sloc }
+flag ~empty (locord \ loc) as AssertLocordSameLoc
+
+// no (W->W->R) in visto
+flag ~empty (visto & ([W]; locord; [W]; locord; [R])) as AssertVisTo

cat/spirv-nochains.cat

@@ -0,0 +1,153 @@
+SPIRV
+(* Vulkan + SPIR-V Memory Model *)
+(* For when availability/visibility chains are not supported *)
+
+// Base relations:
+// vloc: events accessing the same virtual location, aka "same reference (sref)" in the Vulkan spec
+// syncbar: synchronize by barriers with same logical barrier resource (barID)
+// ssg: same subgroup
+// swg: same workgroup
+// sqf: same queuefamily
+// ssw: system-synchronizes-with
+
+// Tags:
+// SC0, SC1: storage class 0, 1
+// SEMSC0, SEMSC1: storage class semantics 0. 1
+// SG, WG, QF, DV: subgroup, workgroup, queuefamily, device domains
+// AV, VIS: availability, visibility
+// AVDEVICE, VISDEVICE: availability, visibility op to the device domain
+
+(*******************)
+(*  Auxiliaries *)
+(*******************)
+
+(* Tags *)
+let PRIV = (R | W) \ NONPRIV // PRIV is the complement of NONPRIV
+
+let SEMSC01 = SEMSC0 & SEMSC1
+
+let AVSHADER = (AV | SEMAV) & DV
+let VISSHADER = (VIS | SEMVIS) & DV
+
+let AVQF = (AV | SEMAV) & (DV | QF)
+let VISQF = (VIS | SEMVIS) & (DV | QF)
+
+let AVWG = (AV | SEMAV) & (DV | QF | WG)
+let VISWG = (VIS | SEMVIS) & (DV | QF | WG)
+
+let AVSG = AV | SEMAV
+let VISSG = VIS | SEMVIS
+
+(* Relations *)
+let inscope = (DV * DV) |
+              (sqf & ((DV | QF) * (DV | QF))) |
+              (swg & ((DV | QF | WG) * (DV | QF | WG))) |
+              (ssg & ((DV | QF | WG | SG) * (DV | QF | WG | SG)))
+
+// mutually ordered atomics
+let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id
+
+let avvisSem = ((SC0 | SC1) * (AVDEVICE | VISDEVICE))
+                | (SC0 * ((SEMAV | SEMVIS) & SEMSC0))
+                | (SC1 * ((SEMAV | SEMVIS) & SEMSC1))
+let avvisSet = [AV | VIS]; (vloc & loc)
+let avvisinc = ((avvisSem | avvisSem^-1) \ id) |
+               (avvisSet | avvisSet^-1)
+
+let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po
+let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po
+
+let asmo = co & (ATOM * ATOM)
+let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
+let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
+
+// synchronizes-with is similar to C++, with an additional case for fence->cbar->cbar->fence
+let sw = inscope & (
+    ([REL & ATOM]; rs; (rf & mutordatom); [ACQ & ATOM]) |                                               // atomic->atomic
+    ([REL & F]; posemtosc; [ATOM & W]; hypors; (rf & mutordatom); [ACQ & ATOM]) |                       // fence->atomic
+    ([REL & ATOM]; rs; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) |                           // atomic->fence
+    ([REL & F]; posemtosc; [ATOM & W]; hypors; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) |   // fence->fence
+    // (stor[CBAR]) terms are redundant because scbarinst is an equivalence relation on scbarinst, but they make the sequence of instructions more clear.
+    ([REL & F]; po?; [CBAR]; ((syncbar & inscope) \ id); [CBAR]; po?; [ACQ & F])                               // fence->cbar->cbar->fence,
+)
+
+let ithbsemsc0 = ( ssw |
+                   ([SEMSC0]; sw; [SEMSC0]) |
+                   ([SC0 | SEMSC0]; po; [REL & SEMSC0]) |
+                   ([ACQ & SEMSC0]; po; [SC0 | SEMSC0])
+                 )+
+let ithbsemsc1 = ( ssw |
+                   ([SEMSC1]; sw; [SEMSC1]) |
+                   ([SC1 | SEMSC1]; po; [REL & SEMSC1]) |
+                   ([ACQ & SEMSC1]; po; [SC1 | SEMSC1])
+                 )+
+let ithbsemsc01 = ( ssw |
+                   ([SEMSC01]; sw; [SEMSC01]) |
+                   ([SC0 | SC1 | SEMSC01]; po; [REL & SEMSC01]) |
+                   ([ACQ & SEMSC01]; po; [SC0 | SC1 | SEMSC01])
+                 )+
+
+// happens-before
+let hb = ithbsemsc0 | ithbsemsc1 | ithbsemsc01 | po
+
+// chains will turn off nontrivial availability/visibility with this pattern:
+let E = (M | F | CBAR | AVDEVICE | VISDEVICE) \ IW
+let chains = [E]
+
+let avsg = [AVSG]
+let avwg = (chains & (avsg; (hb & ssg & avvisinc))?); [AVWG]
+let avqf = (chains & ((avsg; (hb & ssg & avvisinc))? ; (avwg; (hb & swg & avvisinc))?)); [AVQF]
+let avsh = (chains & ((avsg; (hb & ssg & avvisinc))? ; (avwg; (hb & swg & avvisinc))?; (avqf; (hb & sqf & avvisinc))?)); [AVSHADER]
+let avdv = [AVDEVICE]
+
+let vissg = [VISSG]
+let viswg = [VISWG]; (chains & (((hb & ssg & avvisinc); vissg)?))
+let visqf = [VISQF]; (chains & (((hb & swg & avvisinc) ; viswg)?; ((hb & ssg & avvisinc); vissg)?))
+let vissh = [VISSHADER]; (chains & (((hb & sqf & avvisinc) ; visqf)?; ((hb & swg & avvisinc); viswg)?; ((hb & ssg & avvisinc); vissg)?))
+let visdv = [VISDEVICE]
+
+// loc order, relates memory accesses to the same location
+let locord = loc &
+             (  (hb & int & vloc) |
+                ([R \ PRIV]; hb; [(R | W) \ PRIV]) | // RaR, WaR (non-private)
+                ([R]; ssw+; [R | W]) | // RaR, WaR (any)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsg; (hb & ssg);                          [W \ PRIV])) |   // WaW (via subgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsg; (hb & ssg); vissg; (po? & avvisinc); [R \ PRIV])) |   // RaW (via subgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avwg; (hb & swg);                          [W \ PRIV])) |   // WaW (via subgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avwg; (hb & swg); viswg; (po? & avvisinc); [R \ PRIV])) |   // RaW (via workgroup instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avqf; (hb & sqf);                          [W \ PRIV])) |   // WaW (via queue family instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avqf; (hb & sqf); visqf; (po? & avvisinc); [R \ PRIV])) |   // RaW (via queue family instance domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsh; (hb);                                [W \ PRIV])) |   // WaW (via shader domain)
+                (vloc & ([W \ PRIV]; (po? & avvisinc); avsh; (hb);       vissh; (po? & avvisinc); [R \ PRIV])) |   // RaW (via shader domain)
+                (       ([W];        (hb & avvisinc);  avdv; (hb);                                [W]))        |   // WaW (via device domain)
+                (       ([W];        (hb & avvisinc);  avdv; (hb);       visdv; (hb & avvisinc);  [R]))            // RaW (via device domain)
+             )
+
+let w-locord = [W]; locord
+
+(***********************)
+(* Memory Model Axioms *)
+(***********************)
+
+// Atom instructions' scoped modification order must relate all mutually ordered atomics writes at the same location
+empty ([ATOM & W]; mutordatom; [ATOM & W]) \ (asmo | asmo^-1) as coherence
+
+// locord, rf, fr, asmo must not form cycles
+acyclic (locord | rf | fr | asmo) as consistency-cycle
+
+// non-atomic cannot read-from a value that is shadowed by another write
+empty (rf; ([R \ ATOM])) & (([W]; locord); ([W]; locord)+) as consistency-rf
+
+// rmw events are atomic
+empty rmw & (fre; coe) as atomic
+
+let non-rmw-reads = (R \ RMW) * (R \ RMW)
+empty ((((locord | locord^-1) | mutordatom) \ non-rmw-reads) \ (loc \ id \ non-rmw-reads)) as locord-complete
+
+(***************)
+(* Data Races *)
+(***************)
+
+let pair_with_write = ((W * W) | (W * R) | (R * W)) \ ((IW * _) | (_ * IW)) // ignore IW
+let dr = loc & (pair_with_write \ mutordatom \ id \ (locord | locord^-1))
+flag ~empty dr as racy