"OpenCL"
withoutsc

(* Adapting herd's coherence order (co) to be 
   appropriate for C11's modification order (mo) *)
let mo = co & (nonatomicloc^2)
		
(* Access modes *)
let mo_acq = memory_order_acquire 
let mo_rel = memory_order_release
let mo_acq_rel = memory_order_acq_rel 
let mo_rlx = memory_order_relaxed 
let mo_sc = memory_order_seq_cst

(* Scope annotations *)
let s_wi = memory_scope_work_item 
let s_wg = memory_scope_work_group
let s_dev = memory_scope_device 
let s_all = memory_scope_all_svm_devices

(*******************)
(* Synchronisation *)
(*******************)

let acq = (mo_acq | mo_acq_rel | mo_sc) & (R | F)
let rel = (mo_rel | mo_acq_rel | mo_sc) & (W | F)

(* Fences sequenced before or after *)
let Fpo = [F]; po
let poF = po; [F]
					    
(* Release sequence *)
let rs' = wi | (unv; [R & W])
let rs = co? & rs' & ~((co & ~rs') ; co)

(* Inclusive scopes *)
let incl = wi & s_wi^2 | wg & s_wg^2 | dev & s_dev^2 | s_all^2

(* Inclusive scopes, less conservative (unused) version *)
let incl1 = ([s_wi];wi) | ([s_wg];wg) | ([s_dev];dev) | ([s_all];unv)
let incl' = incl1 & incl1^-1
			     			    
(* Release-acquire synchronisation *)
let ra_sw(r) = ([r & rel]; Fpo?; [W \ s_wi]; rs; [r]; rf; [R \ s_wi];
		poF?; [acq & r]) & incl & ~wi

(* Barrier synchronisation *)
let bar_sw(r) = (entry_fence * exit_fence) & same_B & ~wi & wg & r^2

(* Allowed to synchronise on the other region *)
let scf = mo_sc^2 | (G & L & F)^2

(* Global and local synchronises-with *)
let gsw = ra_sw(G) | bar_sw(G) | (scf & ra_sw(L))  
let lsw = ra_sw(L) | bar_sw(L) | (scf & ra_sw(G)) 

(******************)
(* Happens-before *)
(******************)

(* Global and local happens-before *)
let ghb = (((G^2) & (po | (I * !I))) | gsw)+ 
let lhb = (((L^2) & (po | (I * !I))) | lsw)+ 
show ghb
show lhb
irreflexive ghb as O-Hb-G
irreflexive lhb as O-Hb-L

(*************)
(* Coherence *)
(*************)

let coh(hb) = (rf^-1)?; co; rf?; hb
irreflexive coh(ghb) as O-Coh-G
irreflexive coh(lhb) as O-Coh-L

(************************)
(* Consistency of reads *)
(************************)

(* A load can only read from a store that already happened. *)
irreflexive rf; (ghb | lhb) as O-Rf
				
(* Visible side effects *)
let vis(hb) = (W * R) & hb & loc & ~((hb & loc); [W]; hb)

(* A non-atomic load can only read from a store that is visible. *)
irreflexive rf; [G & nonatomicloc]; ~vis(ghb)^-1 as O-Narf-G
irreflexive rf; [L & nonatomicloc]; ~vis(lhb)^-1 as O-Narf-L

(* Consistency of RMWs *)
irreflexive rf as O-Rmw1
irreflexive co; co; rf^-1 as O-Rmw2
irreflexive co; rf as O-Rmw3

(**************************************)
(* Sequential consistency, simplified *)
(**************************************)

let rb = (rf^-1; co) \ id
let Sp = Fpo?; (rb | mo | (ghb | lhb)); poF?
let Sp = Sp \ (unv; [mo_sc & !(s_all | s_dev)]; unv)

acyclic (mo_sc^2) & Sp as O-Sc
								       
(*********)
(* Races *)
(*********)

let conflict = ((W * W) | (W * R) | (R * W)) & loc

(* Data races *)
let dr = conflict & ~(ghb | lhb) & ~(ghb | lhb)^-1 & ~incl
undefined_unless empty dr as O-Dr
show dr

(* Barrier divergence *)
let bsw = bar_sw(G) | bar_sw(L)
let bd = [entry_fence] & ((~wi & wg); unv) \ (bsw ; unv)
undefined_unless empty bd as O-Bd
show bd