Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for OpenCL SPIR-V #792

Open
wants to merge 1 commit into
base: development
Choose a base branch
from
+23,267 −877
Open

Add support for OpenCL SPIR-V #792

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1 change: 1 addition & 0 deletions cat/opencl-herd.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
7 changes: 4 additions & 3 deletions cat/opencl.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
OpenCL
(* OpenCL Memory Model *)
include "basic.cat"

(*
* This model is based on:
Expand All @@ -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]
Expand Down Expand Up @@ -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 *)
Expand All @@ -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
Loading