<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 />
(* emacs fontification -*-caml-*- *)

(*

--- Introduction ---

This file contains a mathematical version of the relaxed memory model
of C11 and C++11, written in the specification language of Lem. Lem
can compile it to Ocaml, HOL, Isabelle or Latex. The basic model is
faithful to the intent of the 2011 standard and included here in
full. In addition, there are several simplified models that either remove
redundant concepts or provide simplifications for programs that
restrict the input language of programs.

There are lots of definitions that make up the models. To help you
navigate them, the following table of contents (with unique key
phrases) can be used to search the document. Where appropriate, there
are comments describing or explaining the definitions. These are
especially important for the top-level definitions of the simplified models.

--- Contents ---


1 - Relational definitions

2 - Action and location types

  - 2.1 - Projection functions

  - 2.2 - Location kinds

3 - The preferred model

  - 3.1  - Execution records

  - 3.2  - Well formed action

  - 3.3  - Well formed threads

  - 3.4  - Consistent locks

  - 3.5  - Well formed reads from mapping

  - 3.6  - Happens before

  - 3.7  - Consistent SC and modification orders

  - 3.8  - Visible side effects and VSSEs

  - 3.9  - Undefined behaviour

  - 3.10 - Consistent reads from mapping

  - 3.11 - Consistent execution

  - 3.12 - Preferred model top level judgement

4 - Standard C/C++ model

  - 4.1  - Standard model top level judgement

5 - Model with seperate lock order

  - 5.1  - Seperate lock order top level judgement

6 - Model with per-location lock orders

  - 6.1  - per-location lock order top level judgement

7 - Model with single step mutex synchronisation

  - 7.1  - single step mutex synchronisation top level judgement

8 - Model simplified for programs without consumes

  - 8.1  - No consume top level judgement

9 - Model simplified for programs without consumes or relaxed

  - 9.1  - No consume or relaxed top level judgement

10 - Model simplified for programs without consumes, relaxed, acquires or releases

  - 10.1  - No consume, relaxed, acquire or release top level judgement


*)


(*************************************************** *)
(* 1 - Relational definitions *)
(*************************************************** *)


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)

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 

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)

(*************************************************** *)
(* 2 - Action and location types *)
(*************************************************** *)

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


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

type lock_outcome =
    Success
  | Blocked

type action =
  | Lock of action_id * thread_id * location * lock_outcome
  | 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
  | Blocked_rmw of action_id * thread_id * location

(*************************************************** *)
(*   - 2.1 - Projection functions *)
(*************************************************** *)

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
    | Blocked_rmw 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
    | Blocked_rmw _ 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
    | Blocked_rmw _ _ l      -> Some l
    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_successful_lock a =
    match a with
      Lock _ _ _ Success -> true
    | _                    -> false
    end

let is_blocked_lock a =
    match a with
      Lock _ _ _ Blocked -> 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_blocked_rmw a =
    match a with
      Blocked_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_atomic_action a =
    is_atomic_load a || is_atomic_store a || is_atomic_rmw 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

(* It is important to note that seq_cst atomics are both acquires and releases *)

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)

(**************************************** *)
(*   - 2.2 - Location kinds *)
(**************************************** *)

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 a || is_unlock a
          | Non_atomic -> is_load a || is_store a
          | Atomic     -> is_store a || is_atomic_action a || is_blocked_rmw 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


(**************************************** *)
(* 3 - The preferred model *)
(**************************************** *)


(* This simplification has ben verified equivalent to the Standard's model
   (section 4) using the HOL theorem prover. It removes the complicated
   notion of VSSE's, whose force is covered by the coherence requirements.
   For those looking to work with C or C++ concurrency, this is the
   preferred model. Predicates from this model will be used in
   those that follow. *)


(*********************************************** *)
(*  - 3.1 - Execution records *)
(*********************************************** *)

type opsem_execution_part =
  <|  actions : action set;
      threads : thread_id set;
      lk      : location -> location_kind;
      sb      : (action * action) set;
      asw     : (action * action) set;
      dd      : (action * action) set;
      cd      : (action * action) set;  |>

type witness_execution_part =
  <|  rf     : (action * action) set;
      mo      : (action * action) set;
      sc      : (action * action) set;  |>


(**************************************** *)
(*   - 3.2 - Well formed action *)
(**************************************** *)


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

(*********************************************** *)
(*  - 3.3 - Well formed threads *)
(*********************************************** *)

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 &&
    (forall (a IN actions). 
       (is_blocked_rmw a || is_blocked_lock a) 
       --> 
       not (exist (b IN actions). (a,b) IN sb))

(*********************************************** *)
(*   - 3.4 - Consistent locks *)
(*********************************************** *)

let consistent_locks actions lo hb =
    let mutex_actions = {a | forall (a IN actions) | (is_lock a || is_unlock a)} in
    let lo_happens_before = restrict_relation_set hb mutex_actions in
    strict_total_order_over mutex_actions lo &&
    lo_happens_before subset lo &&
    (forall ((a,c) IN lo). 
      is_successful_lock a && is_successful_lock c && same_location a c
      --> 
      (exist (b IN actions). same_location a b && is_unlock b && (a,b) IN lo && (b,c) IN lo))

(*********************************************** *)
(*  - 3.5 - Well formed reads from mapping *)
(*********************************************** *)

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) ) )

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

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 lo 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_successful_lock b && (a,b) IN lo) ||
        (* 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 *)
        ( not (same_thread a b) &&
          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) ) ) ||
        ( not (same_thread a b) &&
          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 ) ) ) ||
        ( not (same_thread a b) &&
          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 lo rs hrs =
    { (a,b) | forall (a IN actions) (b IN actions) |
       synchronizes_with actions sb asw rf lo 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

(*********************************************** *)
(*   - 3.7 - Consistent SC and modification orders *)
(*********************************************** *)

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 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 )
        | _      ->
            ( 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 )


(*********************************************** *)
(*   - 3.8 - Visible side effects *)
(*********************************************** *)


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}


(*********************************************** *)
(*   - 3.9 - Undefined behaviour *)
(*********************************************** *)

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' Xo Xw lo =
  let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
  let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
  let sw    = synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf lo rs hrs in
  let cad   = carries_a_dependency_to_set Xo.actions Xo.sb Xo.dd Xw.rf in
  let dob   = dependency_ordered_before_set Xo.actions Xw.rf rs cad in
  let ithb  = inter_thread_happens_before Xo.actions Xo.sb sw dob in
  let hb    = happens_before Xo.actions Xo.sb ithb in
  data_races Xo.actions hb


let good_mutex_use actions lk sb lo a =
    let mutexes_at_l =
      {a' | forall (a' IN actions) | (is_successful_lock a' || is_unlock a') && (location_of a' = location_of a)}
    in
    let lock_order = restrict_relation_set lo mutexes_at_l in
    (* violated requirement: The calling thread shall own the mutex. *)
    ( is_unlock a --> ( exist (al IN actions).
              is_successful_lock al && (location_of al = location_of a) && (al,a) IN sb &&
              adjacent_less_than lock_order actions al a ) ) &&
    (* violated requirement: The calling thread does not own the mutex. *)
    ( is_lock a -->
      not ( exist (al IN actions).
          is_successful_lock al && (location_of a = location_of al) && same_thread a al &&
          adjacent_less_than lock_order actions al a ) )

let bad_mutexes Xo lo =
  { a | forall (a IN Xo.actions) | not (good_mutex_use Xo.actions Xo.lk Xo.sb lo a)}


let undefined_behaviour Xo Xw =
  not (data_races'         Xo Xw Xw.sc      = {}) ||
  not (unsequenced_races   Xo.actions Xo.sb = {}) ||
  not (indeterminate_reads Xo.actions Xw.rf = {}) ||
  not (bad_mutexes         Xo Xw.sc         = {})


(*********************************************** *)
(*   - 3.9 - Consistent reads from mapping *)
(*********************************************** *)


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 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 N3291 29.3p4 *)
    ( forall (a IN actions) ((x,b) IN sb) (y IN actions).
      ( is_write a && is_fence x &&
        adjacent_less_than sc actions a x &&
        is_atomic_action b && same_location a b &&
        (y,b) IN rf) -->
      ((y = a) || (a,y) IN mo) ) &&
    (* fence restriction N3291 29.3p5 *)
    ( forall ((a,x) IN sb) ((y,b) IN rf).
      ((is_atomic_action a && is_write a &&
        is_fence x && is_atomic_action b && (x,b) IN sc &&
        same_location a b) -->
      ((y = a) || (a,y) IN mo) ) ) &&
    (* fence restriction N3291 29.3p6 *)
    ( forall ((a,x) IN sb) ((y,b) IN sb) (z IN actions).
      ( is_atomic_action a && is_write a &&
        is_fence x && is_fence y && (x,y) IN sc &&
        is_atomic_action b && same_location a b &&
        (z,b) IN rf) -->
      ((z = a) || (a,z) IN mo) ) &&
    (* SC fences impose mo N3291 29.3p7 *)
    ( forall ((a,x) IN sb) ((y,b) IN sb).
      ( is_atomic_action a && is_write a &&
        is_atomic_action b && is_write b &&
        is_fence x && is_fence y && (x,y) IN sc &&
        same_location a b -->
      (a,b) IN mo) ) &&
    (* SC fences impose mo N3291 29.3p7, w collapsed first write*)
    ( forall (a IN actions) ((y,b) IN sb).
      ( is_atomic_action a && is_write a &&
        is_fence y && (a,y) IN sc &&
        is_atomic_action b && is_write b &&
        same_location a b -->
      (a,b) IN mo) ) &&
    (* SC fences impose mo N3291 29.3p7, w collapsed second write*)
    ( forall ((a,x) IN sb) (b IN actions).
      ( is_atomic_action a && is_write a &&
        is_fence x && is_atomic_action b && is_write b && (x,b) IN sc &&
        same_location a b -->
      (a,b) IN mo) )


let no_vsse_consistent_atomic_read_values actions lk rf hb vse =
    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


(*********************************************** *)
(* 3.11 - Consistent execution *)
(*********************************************** *)

(* This simplification has ben verified equivalent to the model
   in section 3 using the HOL theorem prover. It removes the complicated
   notion of VSSE's, whose force is covered by the coherence requirements.
   For those looking to work with C or C++ concurrency, this is the preferred model. *)


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


(*********************************************** *)
(*  - 3.12 - Preferred model top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} no_vsse_cmm opsem (p : program) =
  let pre_executions =
    { (Xopsem,Xwitness) | opsem p Xopsem && no_vsse_consistent_execution Xopsem Xwitness} in
  if  exist ((Xo,Xw) IN pre_executions).
    undefined_behaviour Xo Xw
  then { (Xo,Xw) | true }
  else pre_executions


(*********************************************** *)
(* 4 - Standard C/C++ model *)
(*********************************************** *)

(* The following definitions make up the memory model described by the
   2011 standard. It was constructed in discussion with the
   standardisation comittee. *)

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) ) }

(* visible sequences of side effects have been proven redundant. See the simpler model in section 3. *)

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_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 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 consistent_execution Xo Xw =
  well_formed_threads Xo.actions Xo.threads Xo.lk Xo.sb Xo.asw Xo.dd Xo.cd &&
  ( let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.sc rs hrs in
    let cad   = carries_a_dependency_to_set Xo.actions Xo.sb Xo.dd Xw.rf in
    let dob   = dependency_ordered_before_set Xo.actions Xw.rf rs cad in
    let ithb  = inter_thread_happens_before Xo.actions Xo.sb sw dob in
    let hb    = happens_before Xo.actions Xo.sb ithb in
    let vse   = visible_side_effect_set Xo.actions Xo.sb hb in
    let vsses = visible_sequences_of_side_effects_set Xo.actions Xo.lk Xw.mo hb vse in
    consistent_locks Xo.actions Xw.sc hb &&
    consistent_inter_thread_happens_before Xo.actions ithb &&
    consistent_sc_order Xo.actions Xw.mo Xw.sc hb &&
    consistent_modification_order Xo.actions Xo.lk Xo.sb Xw.mo hb &&
    well_formed_reads_from_mapping Xo.actions Xo.lk Xw.rf &&
    consistent_reads_from_mapping Xo.actions Xo.lk Xo.sb Xw.rf Xw.sc Xw.mo hb vse vsses)


(*********************************************** *)
(*   - 4.1  - Standard model top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} cmm opsem (p : program) =
  let pre_executions = { (Xopsem,Xwitness) | opsem p Xopsem && consistent_execution Xopsem Xwitness} in
  if  exist ((Xo,Xw) IN pre_executions).
    undefined_behaviour Xo Xw
  then { (Xo,Xw) | true }
  else pre_executions


(*********************************************** *)
(* 5 - Model with seperate lock order *)
(*********************************************** *)

(* A version of the no VSSE model with a seperate lock order. *)


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


let no_vsse_seperate_lo_undefined_behaviour Xo Xw lo =
  not (data_races'         Xo Xw lo         = {}) ||
  not (unsequenced_races   Xo.actions Xo.sb = {}) ||
  not (indeterminate_reads Xo.actions Xw.rf = {}) ||
  not (bad_mutexes         Xo lo            = {})


(*********************************************** *)
(*  - 5.1  - Seperate lock order top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} no_vsse_seperate_lo_cmm opsem (p : program) =
  let pre_executions =
    { (Xopsem,(Xwitness,lo)) |
      opsem p Xopsem && no_vsse_seperate_lo_consistent_execution Xopsem Xwitness lo} in
  if  exist ((Xo,(Xw,lo)) IN pre_executions).
    no_vsse_seperate_lo_undefined_behaviour Xo Xw lo
  then { (Xo,(Xw,lo)) | true }
  else pre_executions


(*********************************************** *)
(* 6 - Model with per-location lock orders *)
(*********************************************** *)

(* This model uses per location lock orders rather than one shared one. *)


let multi_lo_consistent_locks actions lk lo hb =
    let mutex_actions = {a | forall (a IN actions) | (is_lock a || is_unlock a)} in
    let lo_happens_before = restrict_relation_set hb mutex_actions in
    lo_happens_before subset lo &&
    (forall ((a,c) IN lo). is_successful_lock a && is_successful_lock c && same_location a c
      --> 
      (exist (b IN actions). same_location a b && is_unlock b && (a,b) IN lo && (b,c) IN lo)) &&
      forall (l IN locations_of actions).
        let actions_at_l = {a | forall (a IN actions) | location_of a = Some l} in
        match lk l with
          Mutex -> 
            strict_total_order_over actions_at_l (restrict_relation_set lo actions_at_l)
        | _     -> Set.is_empty (restrict_relation_set lo actions_at_l) end


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


(*********************************************** *)
(*   - 6.1  - per-location lock order top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} no_vsse_multi_lo_cmm opsem (p : program) =
  let pre_executions =
    { (Xopsem,(Xwitness,lo)) |
      opsem p Xopsem && no_vsse_multi_lo_consistent_execution Xopsem Xwitness lo} in
  if  exist ((Xo,(Xw,lo)) IN pre_executions).
    no_vsse_seperate_lo_undefined_behaviour Xo Xw lo
  then { (Xo,(Xw,lo)) | true }
  else pre_executions


(*********************************************** *)
(* 7 - Model with single step mutex synchronisation *)
(*********************************************** *)

(* This model creates synchronizes-with edges from each unlock to the
   next lock at the same location, rather than all subsequent ones. *)

let lo_single_synchronizes_with actions sb asw rf lo 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_successful_lock b && (a,b) IN lo && not (exist (c IN actions). (a,c) IN lo && (c,b) IN lo)) ||
        (* 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 *)
        ( not (same_thread a b) &&
          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) ) ) ||
        ( not (same_thread a b) &&
          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 ) ) ) ||
        ( not (same_thread a b) &&
          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 lo_single_synchronizes_with_set actions sb asw rf lo rs hrs =
    { (a,b) | forall (a IN actions) (b IN actions) |
       lo_single_synchronizes_with actions sb asw rf lo rs hrs a b}


let no_vsse_multi_lo_single_sw_consistent_execution Xo Xw lo =
  well_formed_threads Xo.actions Xo.threads Xo.lk Xo.sb Xo.asw Xo.dd Xo.cd &&
  ( let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = lo_single_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf lo rs hrs in
    let cad   = carries_a_dependency_to_set Xo.actions Xo.sb Xo.dd Xw.rf in
    let dob   = dependency_ordered_before_set Xo.actions Xw.rf rs cad in
    let ithb  = inter_thread_happens_before Xo.actions Xo.sb sw dob in
    let hb    = happens_before Xo.actions Xo.sb ithb in
    let vse   = visible_side_effect_set Xo.actions Xo.sb hb in
    multi_lo_consistent_locks Xo.actions Xo.lk lo hb &&
    consistent_inter_thread_happens_before Xo.actions ithb &&
    consistent_sc_order Xo.actions Xw.mo Xw.sc hb &&
    consistent_modification_order Xo.actions Xo.lk Xo.sb Xw.mo hb &&
    well_formed_reads_from_mapping Xo.actions Xo.lk Xw.rf &&
    no_vsse_consistent_reads_from_mapping Xo.actions Xo.lk Xo.sb Xw.rf Xw.sc Xw.mo hb vse)


let los_single_sw_data_races' Xo Xw lo =
  let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
  let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
  let sw    = lo_single_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf lo rs hrs in
  let cad   = carries_a_dependency_to_set Xo.actions Xo.sb Xo.dd Xw.rf in
  let dob   = dependency_ordered_before_set Xo.actions Xw.rf rs cad in
  let ithb  = inter_thread_happens_before Xo.actions Xo.sb sw dob in
  let hb    = happens_before Xo.actions Xo.sb ithb in
  data_races Xo.actions hb


let no_vsse_multi_lo_single_sw_undefined_behaviour Xo Xw lo =
  not (los_single_sw_data_races'         Xo Xw lo         = {}) ||
  not (unsequenced_races   Xo.actions Xo.sb = {}) ||
  not (indeterminate_reads Xo.actions Xw.rf = {}) ||
  not (bad_mutexes         Xo lo            = {})


(*********************************************** *)
(*   - 7.1  - single step mutex synchronisation top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} no_vsse_multi_lo_single_sw_cmm opsem (p : program) =
  let pre_executions =
    { (Xopsem,(Xwitness,lo)) |
      opsem p Xopsem && no_vsse_multi_lo_single_sw_consistent_execution Xopsem Xwitness lo} in
  if  exist ((Xo,(Xw,lo)) IN pre_executions).
    no_vsse_multi_lo_single_sw_undefined_behaviour Xo Xw lo
  then { (Xo,(Xw,lo)) | true }
  else pre_executions


(*********************************************** *)
(* 8 - Model simplified for programs without consumes *)
(*********************************************** *)

(* This model is simplified for use with programs that don't use
   consume memory orders. Happens-before is transitive. *)


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 Xo Xw =
  well_formed_threads Xo.actions Xo.threads Xo.lk Xo.sb Xo.asw Xo.dd Xo.cd &&
  ( let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.sc rs hrs in
    let hb    = no_vsse_consume_happens_before Xo.actions Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions Xo.sb hb in
    consistent_locks Xo.actions Xw.sc hb &&
    no_vsse_consume_consistent_happens_before Xo.actions hb &&
    consistent_sc_order Xo.actions Xw.mo Xw.sc hb &&
    consistent_modification_order Xo.actions Xo.lk Xo.sb Xw.mo hb &&
    well_formed_reads_from_mapping Xo.actions Xo.lk Xw.rf &&
    no_vsse_consistent_reads_from_mapping Xo.actions Xo.lk Xo.sb Xw.rf Xw.sc Xw.mo hb vse)


let no_vsse_consume_data_races' Xo Xw lo =
  let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
  let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
  let sw    = synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf lo rs hrs in
  let hb    = no_vsse_consume_happens_before Xo.actions Xo.sb sw in
  data_races Xo.actions hb


let no_vsse_consume_undefined_behaviour Xo Xw =
  not (no_vsse_consume_data_races' Xo Xw Xw.sc = {}) ||
  not (unsequenced_races   Xo.actions Xo.sb    = {}) ||
  not (indeterminate_reads Xo.actions Xw.rf    = {}) ||
  not (bad_mutexes         Xo Xw.sc            = {})


(*********************************************** *)
(*   - 8.1  - No consume top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} no_vsse_consume_cmm opsem (p : program) =
  let pre_executions =
    { (Xopsem,Xwitness) |
      opsem p Xopsem && no_vsse_consume_consistent_execution Xopsem Xwitness} in
  if  exist ((Xo,Xw) IN pre_executions).
    no_vsse_consume_undefined_behaviour Xo Xw
  then { (Xo,Xw) | true }
  else pre_executions


(*********************************************** *)
(* 9 - Model simplified for programs without consumes or relaxed *)
(*********************************************** *)

(* Without relaxed, can release sequences go? Unfortunately not. This model is NOT equvalent. *)


let no_vsse_consume_relaxed_synchronizes_with actions sb asw rf lo 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 lo) ||
        (* 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 lo =
    { (a,b) | forall (a IN actions) (b IN actions) |
       no_vsse_consume_relaxed_synchronizes_with actions sb asw rf lo a b}


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


let no_vsse_consume_relaxed_data_races' Xo Xw lo =
  let sw    = no_vsse_consume_relaxed_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf lo in
  let hb    = no_vsse_consume_happens_before Xo.actions Xo.sb sw in
  data_races Xo.actions hb


let no_vsse_consume_relaxed_undefined_behaviour Xo Xw =
  not (no_vsse_consume_relaxed_data_races' Xo Xw Xw.sc = {}) ||
  not (unsequenced_races   Xo.actions Xo.sb            = {}) ||
  not (indeterminate_reads Xo.actions Xw.rf            = {}) ||
  not (bad_mutexes         Xo Xw.sc                    = {})


(*********************************************** *)
(*   - 9.1  - No consume or relaxed top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} no_vsse_consume_relaxed_cmm opsem (p : program) =
  let pre_executions =
    { (Xopsem,Xwitness) |
      opsem p Xopsem && no_vsse_consume_relaxed_consistent_execution Xopsem Xwitness} in
  if  exist ((Xo,Xw) IN pre_executions).
    no_vsse_consume_relaxed_undefined_behaviour Xo Xw
  then { (Xo,Xw) | true }
  else pre_executions


(*********************************************** *)
(* 10 - Model simplified for programs without consumes, relaxed, acquires or releases *)
(*********************************************** *)

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 Xo rf tot =
  let lo = restrict_relation_set tot { a | forall (a IN Xo.actions) | is_lock a || is_unlock a } in
  well_formed_threads Xo.actions Xo.threads Xo.lk Xo.sb Xo.asw Xo.dd Xo.cd &&
  consistent_total_order Xo.actions Xo.sb Xo.asw tot &&
  consistent_locks Xo.actions lo tot &&
  tot_consistent_reads_from_mapping Xo.actions Xo.lk rf tot &&
  well_formed_reads_from_mapping Xo.actions Xo.lk rf


let tot_hb_data_races Xo rf tot =
  let sc   = tot inter { (a,b) | forall (a IN Xo.actions) (b IN Xo.actions) | is_seq_cst a && is_seq_cst b} in
  let mo   = tot inter { (a,b) | forall (a IN Xo.actions) (b IN Xo.actions) | (same_location a b) && is_write a && is_write b} in
  let sw   = no_vsse_consume_relaxed_synchronizes_with_set Xo.actions Xo.sb Xo.asw rf tot in
  let hb   = no_vsse_consume_happens_before Xo.actions Xo.sb sw in
  data_races Xo.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)  }


let tot_undefined_behaviour Xo rf tot =
  not (tot_hb_data_races   Xo rf tot        = {}) ||
  not (unsequenced_races   Xo.actions Xo.sb = {}) ||
  not (indeterminate_reads Xo.actions rf    = {}) ||
  not (bad_mutexes         Xo tot           = {})


(*********************************************** *)
(*   - 10.1  - No consume, relaxed, acquire or release top level judgement *)
(*********************************************** *)


let {hol; isabelle; coq; tex} tot_cmm opsem (p : program) =
  let pre_executions = { (Xopsem,(rf,tot)) | opsem p Xopsem && tot_consistent_execution Xopsem rf tot} in
  if  exist ((Xo,(rf,tot)) IN pre_executions).
    tot_undefined_behaviour Xo rf tot
  then { (Xo,(rf,tot)) | true }
  else pre_executions