<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* Help emacs fontification -*-caml-*- *)

let irrefl s ord = forall (x IN s). not ((x,x) IN ord)

let trans s ord = forall (x IN s) (y IN s) (z IN s). (((x,y) IN ord) && ((y,z) IN ord)) --> ((x,z) IN ord)

(*val cross : forall 'a. 'a set -> 'a set -> ('a * 'a) set*)
let cross S T = { (s,t) | forall (s IN S) (t IN T) | true}

indreln {isabelle}
  forall r x y. r (x, y) ==> tc' r (x, y) and 
  forall r x y. (exist z. tc' r (x,z) && tc' r (z,y)) ==> tc' r (x,y) 

val tc : forall 'a. ('a * 'a) set -> ('a * 'a) set

let {isabelle} tc r =
 let r' = fun (x,y) -> ((x,y) IN r) in  
 { (x,y) | forall ((x,y) IN r) | tc' r' (x,y) }

let rec {ocaml} tc r =
  let one_step = { (x,z) | forall ((x,y) IN r) ((y',z) IN r) | y = y' } in
  if one_step subset r then r else
  tc (one_step union r)

sub [hol] tc = tc

let restrict_relation_set rel s = (rel) inter (cross s s)

let strict_preorder s ord = irrefl s (ord) && trans s (ord)

let relation_over s rel = forall ((a,b) IN rel). a IN s && b IN s 

(*domain rel s subset s && range rel subset s*)

let inj_on f A =
    (forall (x IN A). (forall (y IN A). (f x = f y) --> (x = y)))

let total_order_over s ord =
    relation_over s ord && (forall (x IN s) (y IN s). (x,y) IN ord || (y,x) IN ord || (x = y))

let strict_total_order_over s ord = strict_preorder s ord && total_order_over s ord

let adjacent_less_than ord s x y =
    (x,y) IN ord && not (exist (z IN s). (x,z) IN ord && (z,y) IN ord)

let adjacent_less_than_such_that pred ord s x y =
    pred x && (x,y) IN ord && not (exist (z IN s). pred z && (x,z) IN ord && (z,y) IN ord)

(*************************************************** *)
(*************************************************** *)

type action_id = num
type thread_id = num
type location = num
type value = num

type memory_order =
    Mo_seq_cst
  | Mo_relaxed
  | Mo_release
  | Mo_acquire
  | Mo_consume
  | Mo_acq_rel


type action =
  | Lock of action_id * thread_id * location
  | Unlock of action_id * thread_id * location
  | Atomic_load of action_id * thread_id * memory_order * location * value
  | Atomic_store of action_id * thread_id * memory_order * location * value
  | Atomic_rmw of action_id * thread_id * memory_order * location * value * value
  | Load of action_id * thread_id * location * value
  | Store of action_id * thread_id * location * value
  | Fence of action_id * thread_id * memory_order


let action_id_of a =
    match a with
    | Lock aid _ _              -> aid
    | Unlock aid _ _            -> aid
    | Atomic_load aid _ _ _ _   -> aid
    | Atomic_store aid _ _ _ _  -> aid
    | Atomic_rmw aid _ _ _ _ _  -> aid
    | Load aid _ _ _            -> aid
    | Store aid _ _ _           -> aid
    | Fence aid _ _             -> aid
    end


let thread_id_of a =
    match a with
      Lock _ tid _             -> tid
    | Unlock _ tid _           -> tid
    | Atomic_load _ tid _ _ _  -> tid
    | Atomic_store _ tid _ _ _ -> tid
    | Atomic_rmw _ tid _ _ _ _ -> tid
    | Load _ tid _ _           -> tid
    | Store _ tid _ _          -> tid
    | Fence _ tid _            -> tid
    end


let memory_order_of a =
    match a with
      Atomic_load _ _ mo _ _  -> Some mo
    | Atomic_store _ _ mo _ _ -> Some mo
    | Atomic_rmw _ _ mo _ _ _ -> Some mo
    | Fence _ _ mo            -> Some mo
    | _                       -> None
    end


let location_of a =
    match a with
      Lock _ _ l             -> Some l
    | Unlock _ _ l           -> Some l
    | Atomic_load _ _ _ l _  -> Some l
    | Atomic_store _ _ _ l _ -> Some l
    | Atomic_rmw _ _ _ l _ _ -> Some l
    | Load _ _ l _           -> Some l
    | Store _ _ l _          -> Some l
    | Fence _ _ _            -> None
    end

let value_read_by a =
    match a with
      Atomic_load _ _ _ _ v  -> Some v
    | Atomic_rmw _ _ _ _ v _ -> Some v
    | Load _ _ _ v           -> Some v
    | _                      -> None
    end


let value_written_by a =
    match a with
      Atomic_store _ _ _ _ v -> Some v
    | Atomic_rmw _ _ _ _ _ v -> Some v
    | Store _ _ _ v          -> Some v
    | _                      -> None
    end

let is_lock a =
    match a with
      Lock _ _ _ -> true
    | _          -> false
    end

let is_unlock a =
    match a with
      Unlock _ _ _ -> true
    | _            -> false
    end

let is_atomic_load a =
    match a with
      Atomic_load _ _ _ _ _ -> true
    | _                     -> false
    end

let is_atomic_store a =
    match a with
      Atomic_store _ _ _ _ _ -> true
    | _                      -> false
    end

let is_atomic_rmw a =
    match a with
      Atomic_rmw _ _ _ _ _ _ -> true
    | _                      -> false
    end

let is_load a =
    match a with
      Load _ _ _ _ -> true
    | _            -> false
    end

let is_store a =
    match a with
      Store _ _ _ _ -> true
    | _             -> false
    end

let is_fence a =
    match a with
      Fence _ _ _ -> true
    | _           -> false
    end


(**************************************** *)

let is_lock_or_unlock a =
    is_lock a || is_unlock a

let is_atomic_action a =
    is_atomic_load a || is_atomic_store a || is_atomic_rmw a

let is_load_or_store a =
    is_load a || is_store a

let is_read a =
    is_load a || is_atomic_load a || is_atomic_rmw a

let is_write a =
    is_store a || is_atomic_store a || is_atomic_rmw a

let is_acquire a =
    match memory_order_of a with
      Some Mo_acquire -> is_read a || is_fence a
    | Some Mo_acq_rel -> is_read a || is_fence a
    | Some Mo_seq_cst -> is_read a || is_fence a
    | Some Mo_consume -> is_fence a
    | None -> is_lock a
    | _ -> false
    end

let is_consume a =
    is_read a && (memory_order_of a = Some Mo_consume)

let is_release a =
    match memory_order_of a with
      Some Mo_release -> is_write a || is_fence a
    | Some Mo_acq_rel -> is_write a || is_fence a
    | Some Mo_seq_cst -> is_write a || is_fence a
    | None -> is_unlock a
    | _ -> false
    end

let is_seq_cst a = (memory_order_of a = Some Mo_seq_cst)

(**************************************** *)

type location_kind =
    Mutex
  | Non_atomic
  | Atomic

let actions_respect_location_kinds actions lk =
  forall (a IN actions). match location_of a with
      Some l ->
          match lk l with
            Mutex      -> is_lock_or_unlock a
          | Non_atomic -> is_load_or_store a
          | Atomic     -> is_load_or_store a || is_atomic_action a end
    | None   -> true
    end

let is_at_location_kind lk a lk0 =
    match location_of a with
      Some l -> (lk l = lk0)
    | None   -> false
    end

let is_at_mutex_location lk a =
    is_at_location_kind lk a Mutex

let is_at_non_atomic_location lk a =
    is_at_location_kind lk a Non_atomic

let is_at_atomic_location lk a =
    is_at_location_kind lk a Atomic


(**************************************** *)


let same_thread a b = (thread_id_of a = thread_id_of b)

let threadwise_relation_over s rel =
    relation_over s rel && (forall (x IN rel).
      same_thread (fst x) (snd x))

let same_location a b = (location_of a = location_of b)


let locations_of actions =
{ l | forall (Some l IN { (location_of a) | forall (a IN actions) | true }) | true}


let well_formed_action a =
  match a with
      Atomic_load  _ _ mem_ord _ _ -> mem_ord = Mo_relaxed
                                   || mem_ord = Mo_acquire
                                   || mem_ord = Mo_seq_cst
                                   || mem_ord = Mo_consume
    | Atomic_store _ _ mem_ord _ _ -> mem_ord = Mo_relaxed
                                   || mem_ord = Mo_release
                                   || mem_ord = Mo_seq_cst
    | Atomic_rmw _ _ mem_ord _ _ _ -> mem_ord = Mo_relaxed
                                   || mem_ord = Mo_release
                                   || mem_ord = Mo_acquire
                                   || mem_ord = Mo_acq_rel
                                   || mem_ord = Mo_seq_cst
                                   || mem_ord = Mo_consume
    | _                            -> true
    end

(*********************************************** *)
(*********************************************** *)
(*********************************************** *)

let well_formed_threads actions threads lk sb asw dd cd =
    inj_on action_id_of (actions) &&
    (forall (a IN actions). well_formed_action a) &&
    threadwise_relation_over actions sb &&
    threadwise_relation_over actions dd &&
    threadwise_relation_over actions cd &&
    strict_preorder actions sb &&
    strict_preorder actions dd &&
    strict_preorder actions cd &&
    (forall (a IN actions). thread_id_of a IN threads) &&
    actions_respect_location_kinds actions lk &&
    dd subset sb &&
    relation_over actions asw

let well_formed_reads_from_mapping actions lk rf =
    relation_over actions rf &&
    ( forall (a1 IN actions) (a2 IN actions) (b IN actions). ((a1,b) IN rf && (a2,b) IN rf) --> (a1 = a2) ) &&
    ( forall (a IN actions) (b IN actions). (a,b) IN rf -->
        same_location a b &&
        ( value_read_by b = value_written_by a ) &&
        not (a = b) &&
        not (is_fence a) && not (is_fence b) &&
        ( is_at_mutex_location lk a --> false ) &&
        ( is_at_non_atomic_location lk a --> is_store a && is_load b ) &&
        ( is_at_atomic_location lk a -->
          (is_atomic_store a || is_atomic_rmw a || is_store a) &&
          (is_atomic_load b || is_atomic_rmw b || is_load b) ) )


let all_lock_or_unlock_actions_at lopt aset =
    {a | forall (a IN aset) | is_lock_or_unlock a && (location_of a = lopt)}

let consistent_locks actions lk sc =
     forall (l IN locations_of actions). (lk l = Mutex) --> (
       let lock_unlock_actions =
         all_lock_or_unlock_actions_at (Some l) actions in
       let lock_order = restrict_relation_set sc lock_unlock_actions in
       (*: 30.4.1:5 - The implementation shall serialize those (lock and unlock) operations. :*)
       strict_total_order_over lock_unlock_actions lock_order &&
       (*: 30.4.1:1   A thread owns a mutex from the time it successfully
                  calls one of the lock functions until it calls unlock.:*)
       (*: 30.4.1:20  Requires: The calling thread shall own the mutex. :*)
       (*: 30.4.1:21  Effects: Releases the calling threads ownership of the mutex.:*)
       ( forall (au IN lock_unlock_actions). is_unlock au -->
         ( exist (al IN lock_unlock_actions).
           adjacent_less_than lock_order actions al au && same_thread al au && is_lock al ) ) &&
       (*: 30.4.1:7  Effects: Blocks the calling thread until ownership of
                 the mutex can be obtained for the calling thread.:*)
       (*: 30.4.1:8  Postcondition: The calling thread owns the mutex. :*)
       ( forall (al IN lock_unlock_actions). is_lock al -->
         ( forall (au IN lock_unlock_actions).
             adjacent_less_than lock_order actions au al --> is_unlock au ) ) )


let rs_element rs_head a =
    same_thread a rs_head || is_atomic_rmw a

let release_sequence actions lk mo a_rel b =
    is_at_atomic_location lk b &&
    is_release a_rel &&
    ( (b = a_rel) ||
      ( rs_element a_rel b && (a_rel,b) IN mo && 
        (forall (c IN actions). ((a_rel,c) IN mo && (c,b) IN mo) --> rs_element a_rel c) ) )

let release_sequence_set actions lk mo =
    { (a,b) | forall (a IN actions) (b IN actions) |
       release_sequence actions lk mo a b}

let hypothetical_release_sequence actions lk mo a b =
    is_at_atomic_location lk b &&
    ( (b = a) ||
      ( rs_element a b && (a,b) IN mo && 
        (forall (c IN actions). ((a,c) IN mo && (c,b) IN mo) --> rs_element a c) ) )


let hypothetical_release_sequence_set actions lk mo =
    { (a,b) | forall (a IN actions) (b IN actions) |
       hypothetical_release_sequence actions lk mo a b}


let synchronizes_with actions sb asw rf sc rs hrs a b =
    (* thread sync *)
    (a,b) IN asw ||
    ( same_location a b && a IN actions && b IN actions &&
      ( (* mutex sync *)
        (is_unlock a && is_lock b && (a,b) IN sc) ||
        (* rel/acq sync *)
        ( is_release a && is_acquire b && not (same_thread a b) &&
          (exist (c IN actions). (a,c) IN rs && (c,b) IN rf ) ) ||
        (* fence sync *)
        ( is_fence a && is_release a && is_fence b && is_acquire b &&
          ( exist (x IN actions) (y IN actions). same_location x y &&
              is_atomic_action x && is_atomic_action y && is_write x &&
              (a,x) IN sb && (y,b) IN sb &&
              ( exist (z IN actions). (x,z) IN hrs && (z,y) IN rf) ) ) ||
        ( is_fence a && is_release a && is_atomic_action b && is_acquire b &&
          ( exist (x IN actions). same_location x b &&
            is_atomic_action x && is_write x && (a,x) IN sb &&
            ( exist (z IN actions). (x,z) IN hrs && (z,b) IN rf ) ) ) ||
        ( is_atomic_action a && is_release a &&
          is_fence b && is_acquire b &&
          ( exist (x IN actions). same_location a x && is_atomic_action x &&
            (x,b) IN sb &&
            ( exist (z IN actions). (a,z) IN rs && (z,x) IN rf ) ) ) ) )


let synchronizes_with_set actions sb asw rf sc rs hrs =
    { (a,b) | forall (a IN actions) (b IN actions) |
       synchronizes_with actions sb asw rf sc rs hrs a b}

let carries_a_dependency_to_set actions sb dd rf = tc ( (rf inter sb) union dd )

let dependency_ordered_before actions rf rs cad a d =
     a IN actions && d IN actions &&
     ( exist (b IN actions). is_release a && is_consume b &&
       (exist (e IN actions). (a,e) IN rs && (e,b) IN rf) &&
       ( (b,d) IN cad || (b = d) ) )

let dependency_ordered_before_set actions rf rs cad =
    { (a,b) | forall (a IN actions) (b IN actions) |
       dependency_ordered_before actions rf rs cad a b}


let compose R1 R2 =
    { (w,z) | forall ((w,x) IN R1) ((y,z) IN R2) | (x = y) } 


let inter_thread_happens_before actions sb sw dob =
    let r = sw union dob union (compose sw sb) in
      tc (r union (compose sb r))


let consistent_inter_thread_happens_before actions ithb =
    irrefl actions ithb

let happens_before actions sb ithb =
    sb union ithb

let all_sc_actions actions =
    {a | forall (a IN actions) | is_seq_cst a || is_lock a || is_unlock a}


let consistent_sc_order actions mo sc hb =
       let sc_happens_before = restrict_relation_set hb (all_sc_actions actions) in
       let sc_mod_order = restrict_relation_set mo (all_sc_actions actions) in
       strict_total_order_over (all_sc_actions actions) sc &&
       sc_happens_before subset sc &&
       sc_mod_order subset sc


let consistent_modification_order actions lk sb sc mo hb =
    (forall (a IN actions) (b IN actions). (a,b) IN mo --> (same_location a b && is_write a && is_write b)) &&
    ( forall (l IN locations_of actions).
        match lk l with
          Atomic -> 
            ( let actions_at_l = {a | forall (a IN actions) | location_of a = Some l} in
              let writes_at_l = {a | forall (a IN actions_at_l) | is_write a} in
                strict_total_order_over writes_at_l (restrict_relation_set mo actions_at_l) &&
                (* hb is a subset of mo at l *)
                restrict_relation_set hb writes_at_l subset mo &&
                (* SC fences impose mo *)
                (restrict_relation_set
                   (compose (compose sb (restrict_relation_set sc {a | forall (a IN actions) | is_fence a})) sb )
                   writes_at_l)
                  subset mo)
        | _      ->
            ( let actions_at_l = {a | forall (a IN actions) | location_of a = Some l} in
                Set.is_empty (restrict_relation_set mo actions_at_l) ) end )


let visible_side_effect actions hb a b =
    (a,b) IN hb &&
    is_write a && is_read b && same_location a b &&
    not ( exist (c IN actions). not (c = a) && not (c = b) &&
          is_write c && same_location c b &&
          (a,c) IN hb && (c,b) IN hb)


let visible_side_effect_set actions sb hb =
    { (a,b) | forall ((a,b) IN hb) | visible_side_effect actions hb a b}


let visible_sequence_of_side_effects_tail actions mo hb vsse_head b =
    { c | forall (c IN actions) |
      (vsse_head,c) IN mo && not ((b,c) IN hb) &&
      ( forall (a IN actions).
          ((vsse_head,a) IN mo && (a,c) IN mo) --> not ((b,a) IN hb) ) }


let visible_sequence_of_side_effects actions lk mo hb vsse_head b =
      (b , if is_at_atomic_location lk b then
             {vsse_head} union
             visible_sequence_of_side_effects_tail actions mo hb vsse_head b
           else
             {})


let visible_sequences_of_side_effects_set actions lk mo hb vse =
{ visible_sequence_of_side_effects actions lk mo hb vsse_head b |
  forall (vsse_head IN actions) (b IN actions) | 
  is_at_atomic_location lk b && is_read b &&
  ((vsse_head,b) IN vse) }


let consistent_non_atomic_read_values actions lk rf vse =
    forall (b IN actions).
    (is_read b && is_at_non_atomic_location lk b) -->
      ( if (exist (a_vse IN actions). (a_vse,b) IN vse)
        then (exist (a_vse IN actions). (a_vse,b) IN vse && (a_vse,b) IN rf)
        else not (exist (a IN actions). (a,b) IN rf) )


let consistent_atomic_read_values actions lk rf vsses =
    forall (b IN actions).
    (is_read b && is_at_atomic_location lk b) -->
      ( if (exist ((b',v) IN vsses). b = b')
        then ( exist ((b',v) IN vsses). b = b' &&
               (exist (c IN v). (c,b) IN rf) )
        else not (exist (a IN actions). (a,b) IN rf) )

let coherent_memory_use actions lk rf mo hb =
    (* CoRR *)
    ( forall ((x,a) IN rf) ((y,b) IN rf).
      ((a,b) IN hb && same_location a b && is_at_atomic_location lk b) -->
      ((x = y) || (x,y) IN mo) ) &&
    (* CoWR *)    
    ( forall ((a,b) IN hb) (c IN actions).
      ((c,b) IN rf && is_write a && same_location a b && is_at_atomic_location lk b) -->
      ((c = a) || (a,c) IN mo) ) &&
    (* CoRW *)
    ( forall ((a,b) IN hb) (c IN actions).
      ((c,a) IN rf && is_write b && same_location a b && is_at_atomic_location lk a) -->
      ((c,b) IN mo) )

let rmw_atomicity actions rf mo =
    forall ((a,b) IN rf).
    is_atomic_rmw b --> adjacent_less_than mo actions a b

let sc_reads_restricted actions rf sc mo hb =
    forall ((a,b) IN rf).
    is_seq_cst b -->
    ( adjacent_less_than_such_that (fun c -> is_write c && same_location b c) sc actions a b ) ||
    ( not (is_seq_cst a) &&
      ( forall (x IN actions).
        (adjacent_less_than_such_that (fun c -> is_write c && same_location b c) sc actions x b) --> not ((a,x) IN hb) ) )

let sc_fences_heeded actions sb rf sc mo =
    (* fence restriction 29.3p5 *)
    ( forall ((a,x) IN sb) ((y,b) IN sb) (z IN actions).
      ( is_atomic_action a && is_write a && is_fence x && is_seq_cst x &&
        is_fence y && is_seq_cst y && is_atomic_action b && same_location a b &&
        (x,y) IN sc && (z,b) IN rf) -->
      ((z = a) || (a,z) IN mo) ) &&
    (* fence restriction 29.3p3 *)
    ( forall (a IN actions) ((x,b) IN sb) (y IN actions).
      ( is_write a && is_fence x && is_seq_cst x &&
        is_atomic_action b && same_location a b &&
        adjacent_less_than sc actions a x && (y,b) IN rf) -->
      ((y = a) || (a,y) IN mo) ) &&
    (* fence restriction 29.3p4 *)
    ( forall ((a,x) IN sb) ((y,b) IN rf).
      ((is_atomic_action a && is_write a && is_fence x && is_seq_cst x &&
        is_atomic_action b && same_location a b &&
        (x,y) IN sc) -->
      ((y = a) || (a,y) IN mo) ) )


let consistent_reads_from_mapping actions lk sb rf sc mo hb vse vsses =
    consistent_non_atomic_read_values actions lk rf vse &&
    consistent_atomic_read_values actions lk rf vsses &&
    coherent_memory_use actions lk rf mo hb &&
    rmw_atomicity actions rf mo &&
    sc_reads_restricted actions rf sc mo hb &&
    sc_fences_heeded actions sb rf sc mo


let all_data_dependency_of actions rf cad =
    tc (rf union cad)

let consistent_control_dependency actions threads lk sb asw dd cd rf cad =
    irrefl (tc (cd union all_data_dependency_of actions rf cad))

let consistent_execution actions threads lk sb asw dd cd rf mo sc =
  well_formed_threads actions threads lk sb asw dd cd &&
  consistent_locks actions lk sc &&
  ( let rs    = release_sequence_set actions lk mo in
    let hrs   = hypothetical_release_sequence_set actions lk mo in
    let sw    = synchronizes_with_set actions sb asw rf sc rs hrs in
    let cad   = carries_a_dependency_to_set actions sb dd rf in
    let dob   = dependency_ordered_before_set actions rf rs cad in
    let ithb  = inter_thread_happens_before actions sb sw dob in
    let hb    = happens_before actions sb ithb in
    let vse   = visible_side_effect_set actions sb hb in
    let vsses = visible_sequences_of_side_effects_set actions lk mo hb vse in
    consistent_inter_thread_happens_before actions ithb &&
    consistent_sc_order actions mo sc hb &&
    consistent_modification_order actions lk sb sc mo hb &&
    well_formed_reads_from_mapping actions lk rf &&
    consistent_reads_from_mapping actions lk sb rf sc mo hb vse vsses)


let indeterminate_reads actions rf =
    {b | forall (b IN actions) | is_read b && not (exist (a IN actions). (a,b) IN rf)}

let unsequenced_races actions sb =
    { (a,b) | forall (a IN actions) (b IN actions) |
        not (a = b) && same_location a b && (is_write a || is_write b) &&
        same_thread a b &&
        not ((a,b) IN sb || (b,a) IN sb)  }

let data_races actions hb =
    { (a,b) | forall (a IN actions) (b IN actions) |
        not (a = b) && same_location a b && (is_write a || is_write b) &&
        not (same_thread a b) &&
        not (is_atomic_action a && is_atomic_action b) &&
        not ((a,b) IN hb || (b,a) IN hb)  }


let data_races' actions threads lk sb asw dd cd rf mo sc =
  let rs   = release_sequence_set actions lk mo in
  let hrs  = hypothetical_release_sequence_set actions lk mo in
  let sw   = synchronizes_with_set actions sb asw rf sc rs hrs in
  let cad  = carries_a_dependency_to_set actions sb dd rf in
  let dob  = dependency_ordered_before_set actions rf rs cad in
  let ithb = inter_thread_happens_before actions sb sw dob in
  let hb   = happens_before actions sb ithb in
  data_races actions hb


(*
let full_cpp_memory_model opsem (p : 'program) =
    let executions =
      { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc) |
        opsem p actions threads lk sb asw dd cd &&
        consistent_execution actions threads lk sb asw dd cd rf mo sc } in
    if (exist (ex IN executions)
              actions
              threads
              lk
              sb
              asw
              dd
              cd
              rf
              mo
              sc.
        (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc)) -->
        not (indeterminate_reads actions rf = {}) &&
        not (unsequenced_races actions sb = {}) &&
        not (data_races' actions threads lk sb asw dd cd rf mo sc = {}) )
    then {}
    else executions
*)


(* SECTION *)

(* less vsse's *)

let no_vsse_consistent_atomic_read_values actions lk rf hb vse =
    (* need to be careful that we cant read from a write that the read happens before *)
    forall (b IN actions).
    (is_read b && is_at_atomic_location lk b) -->
      ( if (exist (a_vse IN actions). (a_vse,b) IN vse)
        then (exist (a IN actions). ((a,b) IN rf) && not ((b,a) IN hb))
        else not (exist (a IN actions). (a,b) IN rf) )


let no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse =
    consistent_non_atomic_read_values actions lk rf vse &&
    no_vsse_consistent_atomic_read_values actions lk rf hb vse &&
    coherent_memory_use actions lk rf mo hb &&
    rmw_atomicity actions rf mo &&
    sc_reads_restricted actions rf sc mo hb &&
    sc_fences_heeded actions sb rf sc mo


let no_vsse_consistent_execution actions threads lk sb asw dd cd rf mo sc =
  well_formed_threads actions threads lk sb asw dd cd &&
  consistent_locks actions lk sc &&
  ( let rs    = release_sequence_set actions lk mo in
    let hrs   = hypothetical_release_sequence_set actions lk mo in
    let sw    = synchronizes_with_set actions sb asw rf sc rs hrs in
    let cad   = carries_a_dependency_to_set actions sb dd rf in
    let dob   = dependency_ordered_before_set actions rf rs cad in
    let ithb  = inter_thread_happens_before actions sb sw dob in
    let hb    = happens_before actions sb ithb in
    let vse   = visible_side_effect_set actions sb hb in
    consistent_inter_thread_happens_before actions ithb &&
    consistent_sc_order actions mo sc hb &&
    consistent_modification_order actions lk sb sc mo hb &&
    no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse &&
    well_formed_reads_from_mapping actions lk rf )


(*
let no_vsse_cpp_memory_model opsem (p : 'program) =
    let executions =
      { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc) |
        opsem p actions threads lk sb asw dd cd &&
        no_vsse_consistent_execution actions threads lk sb asw dd cd rf mo sc } in
    if (exist (ex IN executions)
              actions
              threads
              lk
              sb
              asw
              dd
              cd
              rf
              mo
              sc.
        (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc)) -->
        not (indeterminate_reads actions rf = {}) &&
        not (unsequenced_races actions sb = {}) &&
        not (data_races' actions threads lk sb asw dd cd rf mo sc = {}) )
    then {}
    else executions
*)


(* SECTION *)
(* less consume *)
(* check there are no consume actions *)


let no_vsse_consume_happens_before actions sb sw =
    tc (sb union sw)

let no_vsse_consume_consistent_happens_before actions hb =
    irrefl actions hb

let no_vsse_consume_consistent_execution actions threads lk sb asw dd cd rf mo sc =
  well_formed_threads actions threads lk sb asw dd cd &&
  consistent_locks actions lk sc &&
  ( let rs    = release_sequence_set actions lk mo in
    let hrs   = hypothetical_release_sequence_set actions lk mo in
    let sw    = synchronizes_with_set actions sb asw rf sc rs hrs in
    let hb    = no_vsse_consume_happens_before actions sb sw in
    let vse   = visible_side_effect_set actions sb hb in
    no_vsse_consume_consistent_happens_before actions hb &&
    consistent_sc_order actions mo sc hb &&
    consistent_modification_order actions lk sb sc mo hb &&
    no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse &&
    well_formed_reads_from_mapping actions lk rf )


let no_vsse_consume_data_races' actions threads lk sb asw dd cd rf mo sc =
  let rs   = release_sequence_set actions lk mo in
  let hrs  = hypothetical_release_sequence_set actions lk mo in
  let sw   = synchronizes_with_set actions sb asw rf sc rs hrs in
  let hb   = no_vsse_consume_happens_before actions sb sw in
  data_races actions hb


(*
let no_vsse_consume_cpp_memory_model opsem (p : 'program) =
    let executions =
      { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc) |
        opsem p actions threads lk sb asw dd cd &&
        no_vsse_consume_consistent_execution actions threads lk sb asw dd cd rf mo sc } in
    if (exist (ex IN executions)
              actions
              threads
              lk
              sb
              asw
              dd
              cd
              rf
              mo
              sc.
        (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc)) -->
        not (indeterminate_reads actions rf = {}) &&
        not (unsequenced_races actions sb = {}) &&
        not (no_vsse_consume_data_races' actions threads lk sb asw dd cd rf mo sc = {}) )
    then {}
    else executions
*)


(* SECTION *)
(* less relaxed *)
(* release sequences can go? *)


let no_vsse_consume_relaxed_synchronizes_with actions sb asw rf sc a b =
    (* thread sync *)
    (a,b) IN asw ||
    ( same_location a b && a IN actions && b IN actions &&
      ( (* mutex sync *)
        (is_unlock a && is_lock b && (a,b) IN sc) ||
        (* rel/acq sync *)
        ( is_release a && is_acquire b && not (same_thread a b) && (a,b) IN rf ) ) )


let no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc =
    { (a,b) | forall (a IN actions) (b IN actions) |
       no_vsse_consume_relaxed_synchronizes_with actions sb asw rf sc a b}

let no_vsse_consume_relaxed_consistent_execution actions threads lk sb asw dd cd rf mo sc =
  well_formed_threads actions threads lk sb asw dd cd &&
  consistent_locks actions lk sc &&
  ( let sw    = no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc in
    let hb    = no_vsse_consume_happens_before actions sb sw in
    let vse   = visible_side_effect_set actions sb hb in
    no_vsse_consume_consistent_happens_before actions hb &&
    consistent_sc_order actions mo sc hb &&
    consistent_modification_order actions lk sb sc mo hb &&
    no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse &&
    well_formed_reads_from_mapping actions lk rf )


let no_vsse_consume_relaxed_data_races' actions threads lk sb asw dd cd rf mo sc =
  let sw   = no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc in
  let hb   = no_vsse_consume_happens_before actions sb sw in
  data_races actions hb


(*
let no_vsse_consume_relaxed_cpp_memory_model opsem (p : 'program) =
    let executions =
      { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc) |
        opsem p actions threads lk sb asw dd cd &&
        no_vsse_consume_relaxed_consistent_execution actions threads lk sb asw dd cd rf mo sc } in
    if (exist (ex IN executions)
              actions
              threads
              lk
              sb
              asw
              dd
              cd
              rf
              mo
              sc.
        (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc)) -->
        not (indeterminate_reads actions rf = {}) &&
        not (unsequenced_races actions sb = {}) &&
        not (no_vsse_consume_relaxed_data_races' actions threads lk sb asw dd cd rf mo sc = {}) )
    then {}
    else executions
*)


(* SECTION *)

(* SC *)

let consistent_total_order actions sb asw tot =
  strict_total_order_over actions tot &&
  sb subset tot &&
  asw subset tot


let tot_consistent_reads_from_mapping actions lk rf tot =
  (forall (b IN actions).
    (is_read b) -->
    ( let writes_at_same_location = { a | forall (a IN actions) | (same_location a b) && is_write a} in
      ( if (exist (a IN actions). adjacent_less_than (restrict_relation_set tot (writes_at_same_location union {b})) actions a b)
        then (exist (a IN actions). ((a,b) IN rf) && adjacent_less_than (restrict_relation_set tot (writes_at_same_location union {b})) actions a b)
        else not (exist (a IN actions). (a,b) IN rf) ) ) )

let tot_consistent_execution actions threads lk sb asw dd cd rf tot =
  well_formed_threads actions threads lk sb asw dd cd &&
  consistent_locks actions lk tot &&
  consistent_total_order actions sb asw tot &&
  tot_consistent_reads_from_mapping actions lk rf tot &&
  well_formed_reads_from_mapping actions lk rf


let tot_hb_data_races actions sb asw rf tot =
  let sc   = tot inter { (a,b) | forall (a IN actions) (b IN actions) | is_seq_cst a && is_seq_cst b} in
  let mo   = tot inter { (a,b) | forall (a IN actions) (b IN actions) | (same_location a b) && is_write a && is_write b} in
  let sw   = no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc in
  let hb   = no_vsse_consume_happens_before actions sb sw in
  data_races actions hb


let tot_data_races actions tot =
    { (a,b) | forall (a IN actions) (b IN actions) |
        not (a = b) && same_location a b && (is_write a || is_write b) &&
        not (same_thread a b) &&
        not (is_atomic_action a && is_atomic_action b) &&
        (adjacent_less_than tot actions a b || adjacent_less_than tot actions b a)  }

(*


Two memory operations conflict if they access the same memory
location, and at least one of them is a store, atomic store, or
atomic read-modify-write operation.

In a sequentially consistent
execution, two memory operations from different threads form a
type 1 data race if they conflict, at least one of them is a data operation,
and they are adjacent in <T (i.e., they may be executed
concurrently).
*)

(*: SECTION :*)

(*:
let cpp_memory_model opsem (p : 'program) = full_cpp_memory_model opsem (p : 'program)
:*)