"C++11" withinit

include "c11_base.cat"

(* C: sc_fenced_sc_fences_heeded, sc_accesses_sc_reads_restricted,
      sc_accesses_consistent_sc *)
let scco = [sc]; fid; co; idf; [sc]

(* For SC fr, the picture is more complicated. We'd like to have: *)
let scfr = ~[_] &
           ( ([sc]    ; rf^-1; hbl  ; [W & sc]) |
             ([sc]    ; rf^-1; [sc] ; co; [sc]) |
             ([sc & F]; po; fr;     [sc]    ) |
             (    [sc];     fr; po; [sc & F]) |
             ([sc & F]; po; fr; po; [sc & F])
           )

(* SC atomics have to respect happens-before: *)
let schb = [sc]; hb; [sc]

let scp = schb | scco | scfr

acyclic scp as scConsistent
show scp