add support for OpenCL SPIR-V

Signed-off-by: Haining Tong <[email protected]>
hernanponcedeleon · Feb 25, 2025 · 90034ec · 90034ec
1 parent d82d2ef
commit 90034ec
Show file tree

Hide file tree

Showing 628 changed files with 23,267 additions and 877 deletions.
diff --git a/cat/opencl-herd.cat b/cat/opencl-herd.cat
@@ -22,6 +22,7 @@ OpenCL
 // LOCAL: local memory
 // EF: entry fence of barrier
 // XF: exit fence of barrier
+// NAL: non-atomic location
 
 // dynamic_tag relates events to itself that access an address whose init event is marked X or Fence tagged with X
 let dynamic_tag(X) = [range([IW & X]; loc)] | [X & F]

diff --git a/cat/opencl.cat b/cat/opencl.cat
@@ -1,6 +1,5 @@
 OpenCL
 (* OpenCL Memory Model *)
-include "basic.cat"
 
 (*
 * This model is based on:
@@ -23,6 +22,7 @@ include "basic.cat"
 // LOCAL: local memory
 // EF: entry fence of barrier
 // XF: exit fence of barrier
+// NAL: non-atomic location
 
 // dynamic_tag relates events to itself that access an address whose init event is marked X or Fence tagged with X
 let dynamic_tag(X) = [range([IW & X]; loc)] | [X & F]
@@ -119,7 +119,8 @@ acyclic (SC*SC) & scp & incl as O-Sscoped
 
 (* data_races *)
 let cnf = ((W * W) | (W * R) | (R * W)) & loc
-let dr = cnf & ~(ghb | lhb) & ~(ghb | lhb)^-1 & ~wi & ~incl
+// TODO: "there is exactly one initial event per location", in current implementation, memory object like global scope id is initialized by three write events
+let dr = cnf & ~(ghb | lhb) & ~(ghb | lhb)^-1 & ~wi & ~incl \ ((_ * IW) | (IW * _))
 flag ~empty dr as data_race
 
 (* unsequenced_races *)
@@ -129,5 +130,5 @@ flag ~empty ur as unsequenced_race
 
 (* Barrier divergence *)
 let bsw = bar_sw(dynamic_tag(GLOBAL)) | bar_sw(dynamic_tag(LOCAL))
-let bd = [EF] & [domain(~wi & swg)] \ [domain(bsw)]
+let bd = [EF] &  ((~wi & swg); unv) \ (bsw ; unv)
 flag ~empty bd as barrier_divergence