cmm.html

<!-- Generated by Lem from ../axiomatic/ntc/cmm.lem. -->

<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
          "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/> 
    <title>C/C++ memory model definitions</title>
    <link rel="stylesheet" type="text/css" title="cppmem style" media="screen" href="cppmem.css"/>
  </head>
  <body>
    <h1 id="title">C/C++ memory model definitions</h1>
<pre>

<a name="irrefl">(*========================================================================*)
(*                                                                        *)
(*             cppmem model exploration tool                              *)
(*                                                                        *)
(*                    Mark Batty                                          *)
(*                    Scott Owens                                         *)
(*                    Jean Pichon                                         *)
(*                    Susmit Sarkar                                       *)
(*                    Peter Sewell                                        *)
(*                                                                        *)
(*  This file is copyright 2011, 2012 by the above authors.               *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*  notice, this list of conditions and the following disclaimer.         *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*  notice, this list of conditions and the following disclaimer in the   *)
(*  documentation and/or other materials provided with the distribution.  *)
(*  3. The names of the authors may not be used to endorse or promote     *)
(*  products derived from this software without specific prior written    *)
(*  permission.                                                           *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHE   *)
(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
(*========================================================================*)

(* 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 - Type definitions and projections

  - 2.1 - Action and location types

  - 2.2 - Execution records

  - 2.3 - Projection functions 

  - 2.4 - Location kinds

3 - The preferred model

  - 3.1  - Well formed action

  - 3.2  - Well formed threads

  - 3.3  - Consistent locks

  - 3.4  - Well formed reads from mapping

  - 3.5  - Happens before

  - 3.6  - Consistent SC and modification orders

  - 3.7  - Visible side effects and VSSEs

  - 3.8 - Consistent reads from mapping

  - 3.9  - Undefined behaviour

  - 3.10 - Consistent execution

  - 3.11 - Preferred model top level judgement

4 - Standard C/C++ model

5 - Model with separate lock order

6 - Model with per-location lock orders

7 - Model with per-location lock orders and sc order

8 - Model with single step mutex synchronisation

9 - Model simplified for programs without consumes

10 - Model simplified for programs without consumes or relaxed

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

12 - Model simplified to a single thread, no atomics

13 - Model simplified, single thread, no atomics 2

14 - Model simplified, multi-thread, no atomics, yes locks

*)


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


let irrefl s ord = &forall; (x &isin; s). not ((x,x)&isin; ord)
<a name="trans">

let trans s ord = &forall; (x &isin; s) (y &isin; s) (z &isin; s). (((x,y)&isin; ord)&amp;&amp; ((y,z)&isin; ord))&rarr; ((x,z)&isin; ord)
<a name="cross">

let cross S T = { (s,t) | &forall; (s &isin; S) (t &isin; T) | true}

val tc : &forall; 'a. set ('a * 'a) -> set ('a * 'a)
<a name="set_restrict">

let set_restrict rel s = (rel)^cap; (cross s s)
<a name="strict_partial_order">

let strict_partial_order s ord = irrefl s ord &amp;&amp; trans s ord 
<a name="relation_over">

let relation_over s rel = &forall; ((a,b) &isin; rel). a &isin; s &amp;&amp; (b &isin; s)
<a name="inj_on"> 

let inj_on f A =
    (&forall; (x &isin; A). (&forall; (y &isin; A). (f x = f y)&rarr; (x = y)))
<a name="total">

let total s ord =
     (&forall; (x &isin; s) (y &isin; s). (x,y)&isin; ord || ((y,x)&isin; ord || (x = y)))
<a name="strict_total_order_over">

let strict_total_order_over s ord =
    relation_over s ord &amp;&amp;
    (strict_partial_order s ord &amp;&amp;
    total s ord)
<a name="adjacent_less_than">

let adjacent_less_than ord s x y =
    (x,y)&isin; ord &amp;&amp; not (&exist; (z &isin; s). (x,z)&isin; ord &amp;&amp; ((z,y)&isin; ord))
<a name="adjacent_less_than_such_that">

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

(*************************************************** *)
(* 2 - Type definitions and projections *)
(*************************************************** *)


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


(**** Cppmem base types ****)

type flexsym = string

type cst =
  | Concrete of num
  | Symbolic of string

type cvalue =
  | Rigid of cst
  | Flexible of flexsym

type aid = string
type tid = cvalue
type location = cvalue
type program = num


type memory_order =
  | NA
  | Seq_cst
  | Relaxed
  | Release
  | Acquire
  | Consume
  | Acq_rel

type lock_outcome =
    Locked
  | Blocked

type action =
  | Lock of aid * tid * location * lock_outcome
  | Unlock of aid * tid * location
  | Load of aid * tid * memory_order * location * cvalue
  | Store of aid * tid * memory_order * location * cvalue
  | RMW of aid * tid * memory_order * location * cvalue * cvalue
  | Fence of aid * tid * memory_order
  | Blocked_rmw of aid * tid * location 
<a name="dummy22">


(*********************************************** *)
(*  - 2.2 - Execution records *)
(*********************************************** *)

let dummy22 = true

type location_kind =
    Mutex
  | Non_Atomic
  | Atomic

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

type order_kind =
     Global_order
   | Per_location_order

type relation_usage_flags =
  <|  rf_flag  : bool;
      mo_flag  : bool;
      sc_flag  : bool;
      lo_flag  :option order_kind;
      ao_flag  : bool;
      tot_flag : bool;  |>

type execution_witness =
  <|  rf      : set (action * action);
      mo      : set (action * action);
      sc      : set (action * action);
      lo      : set (action * action);
      ao      : set (action * action);
      tot     : set (action * action);
 |>

type relation_list = list (string * set (action * action))

type complete_execution = (pre_execution * execution_witness * relation_list)

type program_behaviours =
    Defined of set complete_execution
  | Undefined

type named_predicate_tree =
    Leaf of (complete_execution -> bool)
  | Node of list (string * named_predicate_tree)

(*
let rec apply_tree pred_tree X =
    let element_apply_and (name,branch) P = apply_tree branch X && P in
      match pred_tree with
        Leaf p -> p X
      | Node l -> List.fold_right element_apply_and l true end
*)

let rec apply_tree pred_tree X =
      match pred_tree with
        Leaf p -> p X
      | Node l -> List.fold_right 
                    (fun (name,branch) P -> apply_tree branch X &amp;&amp; P)
                    l true end

type fault_setgen =
    One of (string * (complete_execution -> set action))
  | Two of (string * (complete_execution -> set (action * action)))
<a name="each_empty">


let each_empty faults_list X =
    let faults_empty f =
      match f with
        One (name,setgen) -> (setgen X = {})
      | Two (name,setgen) -> (setgen X = {}) end in
    List.for_all faults_empty faults_list


type opsem_t = program -> pre_execution -> bool


type protocol_t = complete_execution -> bool 
<a name="true_protocol">

let true_protocol _ = true

type memory_model =
  <|  consistent : named_predicate_tree;
      relation_calculation : pre_execution -> execution_witness ->
  relation_list;
      undefined : list fault_setgen;
      relation_flags : relation_usage_flags;
  |>


val behaviour : memory_model -> protocol_t -> opsem_t -> program -> program_behaviours 
<a name="dummy23">


(*************************************************** *)
(*   - 2.3 - Projection functions *)
(*************************************************** *)

let dummy23 = true 
<a name="aid_of">

let aid_of a =
    match a with
    | Lock aid _ _ _            -> aid
    | Unlock aid _ _            -> aid
    | Load aid _ _ _ _          -> aid
    | Store aid _ _ _ _         -> aid
    | RMW aid _ _ _ _ _         -> aid
    | Fence aid _ _             -> aid
    | Blocked_rmw aid _ _       -> aid
    end 
<a name="tid_of">


let tid_of a =
    match a with
      Lock _ tid _ _           -> tid
    | Unlock _ tid _           -> tid
    | Load _ tid _ _ _         -> tid
    | Store _ tid _ _ _        -> tid
    | RMW _ tid _ _ _ _        -> tid
    | Fence _ tid _            -> tid
    | Blocked_rmw _ tid _      -> tid
    end 
<a name="loc_of">


let loc_of a =
    match a with
      Lock _ _ l _           -> Some l
    | Unlock _ _ l           -> Some l
    | Load _ _ _ l _         -> Some l
    | Store _ _ _ l _        -> Some l
    | RMW _ _ _ l _ _        -> Some l
    | Fence _ _ _            -> None
    | Blocked_rmw _ _ l      -> Some l
    end 
<a name="value_read_by">

let value_read_by a =
    match a with
      Load _ _ _ _ v         -> Some v
    | RMW _ _ _ _ v _        -> Some v
    | _                      -> None
    end 
<a name="value_written_by">


let value_written_by a =
    match a with
      Store _ _ _ _ v        -> Some v
    | RMW _ _ _ _ _ v        -> Some v
    | _                      -> None
    end 
<a name="is_lock">

let is_lock a =
    match a with
      Lock _ _ _ _ -> true
    | _            -> false
    end 
<a name="is_successful_lock">

let is_successful_lock a =
    match a with
      Lock _ _ _ Locked -> true
    | _                  -> false
    end 
<a name="is_blocked_lock">

let is_blocked_lock a =
    match a with
      Lock _ _ _ Blocked -> true
    | _                  -> false
    end 
<a name="is_unlock">

let is_unlock a =
    match a with
      Unlock _ _ _ -> true
    | _            -> false
    end 
<a name="is_atomic_load">

let is_atomic_load a =
    match a with
      Load _ _ mo _ _ -> mo <> NA
    | _               -> false
    end 
<a name="is_atomic_store">

let is_atomic_store a =
    match a with
      Store _ _ mo _ _ -> mo <> NA
    | _                -> false
    end 
<a name="is_RMW">

let is_RMW a =
    match a with
      RMW _ _ _ _ _ _ -> true
    | _               -> false
    end 
<a name="is_blocked_rmw">

let is_blocked_rmw a =
    match a with
      Blocked_rmw _ _ _ -> true
    | _                 -> false
    end 
<a name="is_NA_load">

let is_NA_load a =
    match a with
      Load _ _ mo _ _ -> mo = NA
    | _               -> false
    end 
<a name="is_NA_store">

let is_NA_store a =
    match a with
      Store _ _ mo _ _ -> mo = NA
    | _                -> false
    end 
<a name="is_load">

let is_load a =
    match a with
      Load _ _ _ _ _ -> true
    | _              -> false
    end 
<a name="is_store">

let is_store a =
    match a with
      Store _ _ _ _ _ -> true
    | _               -> false
    end 
<a name="is_fence">

let is_fence a =
    match a with
      Fence _ _ _ -> true
    | _           -> false
    end 
<a name="is_atomic_action">

let is_atomic_action a =
    match a with
      Load _ _ mo _ _  -> mo <> NA
    | Store _ _ mo _ _ -> mo <> NA
    | RMW _ _ _ _ _ _  -> true
    | _                -> false
    end 
<a name="is_read">

let is_read a =
    match a with
      Load _ _ _ _ _  -> true
    | RMW _ _ _ _ _ _ -> true
    | _               -> false
    end 
<a name="is_write">

let is_write a =
    match a with
      Store _ _ _ _ _ -> true
    | RMW _ _ _ _ _ _ -> true
    | _               -> false
    end 
<a name="dummy23'">


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

let dummy23' = true 
<a name="is_acquire">

let is_acquire a = 
    match a with
      Load _ _ mo _ _  -> mo &isin; {Acquire;Seq_cst}
    | RMW _ _ mo _ _ _ -> mo &isin; {Acquire;Acq_rel;Seq_cst}
    | Fence _ _ mo     -> mo &isin; {Acquire;Seq_cst}
    | _                -> false
    end 
<a name="is_release">

let is_release a = 
    match a with
      Store _ _ mo _ _  -> mo &isin; {Release;Seq_cst}
    | RMW _ _ mo _ _ _  -> mo &isin; {Release;Acq_rel;Seq_cst}
    | Fence _ _ mo      -> mo &isin; {Release;Seq_cst}
    | _                 -> false
    end 
<a name="is_consume">

let is_consume a = 
    match a with
      Load _ _ mo _ _  -> mo = Consume
    | _                -> false
    end 
<a name="is_seq_cst">


let is_seq_cst a =
    match a with
      Load _ _ mo _ _  -> mo = Seq_cst
    | RMW _ _ mo _ _ _ -> mo = Seq_cst
    | Fence _ _ mo     -> mo = Seq_cst
    | _                -> false
    end 
<a name="threadwise">


let threadwise s rel = &forall; ((a,b) &isin; rel). tid_of a = tid_of b 
<a name="locationwise">

let locationwise s rel = &forall; ((a,b) &isin; rel). loc_of a = loc_of b 
<a name="per_location_total">

let per_location_total s rel =
    &forall; (a &isin; s) (b &isin; s). (loc_of a = loc_of b)&rarr;
      ((a,b)&isin; rel || ((b,a)&isin; rel || (a = b)))
<a name="dummy24">


(**************************************** *)
(*   - 2.4 - Location kinds *)
(**************************************** *)

let dummy24 = true 
<a name="dummy241">

(* let actions_respect_location_kinds actions lk = *)
(*   forall (a IN actions). match loc_of a with *)
(*       Some l -> *)
(*           match lk l with *)
(*             Mutex      -> is_lock a     || is_unlock a *)
(*           | Non_Atomic -> is_NA_load a  || is_NA_store a *)
(*           | Atomic     -> is_NA_store a || is_atomic_action a || is_blocked_rmw a end *)
(*     | None   -> true *)
(*     end *)

let dummy241 = true 
<a name="actions_respect_location_kinds">


let actions_respect_location_kinds actions lk =
 &forall; (a &isin; actions). match a with
    | Lock _ _ l _            -> lk l = Mutex
    | Unlock _ _ l            -> lk l = Mutex
    | Load _ _ mo l _         ->
        (mo = NA &amp;&amp; (lk l = Non_Atomic)) || (lk l = Atomic)
    | Store _ _ mo l _        ->
        (mo = NA &amp;&amp; (lk l = Non_Atomic)) || (lk l = Atomic)
    | RMW _ _ _ l _ _         -> lk l = Atomic
    | Fence _ _ _             -> true
    | Blocked_rmw _ _ l       -> lk l = Atomic
    end 
<a name="is_at_mutex_location">


let is_at_mutex_location lk a =
    match loc_of a with
      Some l -> (lk l = Mutex)
    | None   -> false
    end 
<a name="is_at_non_atomic_location">

let is_at_non_atomic_location lk a =
    match loc_of a with
      Some l -> (lk l = Non_Atomic)
    | None   -> false
    end 
<a name="is_at_atomic_location">

let is_at_atomic_location lk a =
    match loc_of a with
      Some l -> (lk l = Atomic)
    | None   -> false
    end 
<a name="dummy31">


(**************************************** <a name="preferred">*)
(* 3 - The preferred memory_model *)
(**************************************** *)


(* This simplification should be equivalent to the Standard's memory_model
   (section 4) (this was verified for earlier versions 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
   memory_model. Predicates from this memory_model will be used in those that
   follow. *)


(**************************************** *)
(*   - 3.1 - Well formed action *)
(**************************************** *)

let dummy31 = true 
<a name="locations_of">

let locations_of actions =
{ l | &forall; (Some l &isin; { (loc_of a) | &forall; (a &isin; actions) | true }) | true}
<a name="well_formed_action">


let well_formed_action a =
  match a with
    | Load  _ _ mo _ _ -> mo &isin; {NA;Relaxed;Acquire;Seq_cst;Consume}
    | Store _ _ mo _ _ -> mo &isin; {NA;Relaxed;Release;Seq_cst}
    | RMW _ _ mo _ _ _ -> mo &isin; {Relaxed;Release;Acquire;Acq_rel;Seq_cst}
    | Fence _ _ mo     -> mo &isin; {Release;Acquire;Seq_cst}
    | _                -> true
    end 
<a name="dummy32">

(*********************************************** *)
(*  - 3.2 - Well formed threads *)
(*********************************************** *)

(*
    relation_over Xo.actions Xo.cd &&
    threadwise Xo.actions Xo.cd &&
    strict_partial_order Xo.actions Xo.cd &&
    Xo.cd subset Xo.sb &&
*)

let dummy32 = true 
<a name="blocking_observed">

let blocking_observed actions sb =
    (&forall; (a &isin; actions). 
       (is_blocked_rmw a || is_blocked_lock a)&rarr; 
       not (&exist; (b &isin; actions). (a,b)&isin; sb))
<a name="dummy32'">


(* This should really be moved to the undefined behaviour... not sure now.*)

let dummy32' = true 
<a name="well_formed_threads">

let well_formed_threads (Xo,_,_) =
    (&forall; (a &isin; Xo.actions). well_formed_action a)&amp;&amp; (* especially this *)
    (actions_respect_location_kinds Xo.actions Xo.lk &amp;&amp;
    (blocking_observed Xo.actions Xo.sb &amp;&amp;
    (inj_on aid_of Xo.actions &amp;&amp;
    ((&forall; (a &isin; Xo.actions). tid_of a &isin; Xo.threads)&amp;&amp;
    (relation_over Xo.actions Xo.sb &amp;&amp;
    (relation_over Xo.actions Xo.dd &amp;&amp;
    (relation_over Xo.actions Xo.asw &amp;&amp;
    (threadwise Xo.actions Xo.sb &amp;&amp;
    (threadwise Xo.actions Xo.dd &amp;&amp;
    (strict_partial_order Xo.actions Xo.sb &amp;&amp;
    (strict_partial_order Xo.actions Xo.dd &amp;&amp;
    (Xo.dd subset Xo.sb))))))))))))
<a name="dummy33">

(*********************************************** *)
(*   - 3.3 - Consistent locks *)
(*********************************************** *)

let dummy33 = true 
<a name="consistent_locks">

let consistent_locks (Xo,Xw,("hb",hb)::_) =
    (&forall; ((a,c) &isin; Xw.sc). 
      (is_successful_lock a &amp;&amp; (is_successful_lock c &amp;&amp; (loc_of a = loc_of c)))&rarr; 
      (&exist; (b &isin; Xo.actions). (loc_of a = loc_of b)&amp;&amp; (is_unlock b &amp;&amp; ((a,b)&isin; Xw.sc &amp;&amp; ((b,c)&isin; Xw.sc)))))
<a name="dummy34">

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


let dummy34 = true 
<a name="well_formed_rf">


let well_formed_rf (Xo,Xw,_) =
    &forall; ((a,b) &isin; Xw.rf).
      a &isin; Xo.actions &amp;&amp; (b &isin; Xo.actions &amp;&amp;
      (loc_of a = loc_of b &amp;&amp;
      (is_write a &amp;&amp; (is_read b &amp;&amp;
      (value_read_by b = value_written_by a &amp;&amp;
      (&forall; (a' &isin; Xo.actions). ((a',b)&isin; Xw.rf)&rarr; (a = a')))))))
<a name="dummy35">


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

let dummy35 = true 
<a name="rs_element">

let rs_element head a =
    (tid_of a = tid_of head) || is_RMW a 
<a name="release_sequence">


let release_sequence actions lk mo a_rel b =
    is_release a_rel &amp;&amp;
    ( (b = a_rel) ||
      ( rs_element a_rel b &amp;&amp; ((a_rel,b)&isin; mo &amp;&amp;
        (&forall; (c &isin; actions). ((a_rel,c)&isin; mo &amp;&amp; ((c,b)&isin; mo))&rarr; rs_element a_rel c)) ) )
<a name="release_sequence_set">

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


let release_sequence_set actions lk mo =
  { (rel,b) | &forall; (rel &isin; actions) (b &isin; actions) |
    is_release rel &amp;&amp;
    ( (b = rel) ||
      ( (rel,b)&isin; mo &amp;&amp; 
        (rs_element rel b &amp;&amp;
        (&forall; (c &isin; actions).
          ((rel,c)&isin; mo &amp;&amp; ((c,b)&isin; mo))&rarr; rs_element rel c)) ) ) }
<a name="hypothetical_release_sequence_set">


let hypothetical_release_sequence_set actions lk mo =
  { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
    is_at_atomic_location lk a &amp;&amp;
    (is_write a &amp;&amp;
    ( (b = a) ||
      ( (a,b)&isin; mo &amp;&amp; 
        (rs_element a b &amp;&amp;
        (&forall; (c &isin; actions).
          ((a,c)&isin; mo &amp;&amp; ((c,b)&isin; mo))&rarr; rs_element a c)) ) )) }
<a name="hypothetical_release_sequence">

let hypothetical_release_sequence actions lk mo a b =
    is_at_atomic_location lk a &amp;&amp;
    (is_write a &amp;&amp;
    ( (b = a) ||
      ( rs_element a b &amp;&amp; ((a,b)&isin; mo &amp;&amp;
        (&forall; (c &isin; actions). ((a,c)&isin; mo &amp;&amp; ((c,b)&isin; mo))&rarr; rs_element a c)) ) ))
<a name="synchronizes_with">


(* 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)&isin; asw ||
    ( (loc_of a = loc_of b)&amp;&amp; (a &isin; actions &amp;&amp; (b &isin; actions &amp;&amp;
      ( (* mutex sync *)
        (* this seems to be the multi loc lo version... *)
        (is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo))) ||
        (* rel/acq sync *)
        (( is_release a &amp;&amp; (is_acquire b &amp;&amp; ((tid_of a <> tid_of b)&amp;&amp;
          (&exist; (c &isin; actions). (a,c)&isin; rs &amp;&amp; ((c,b)&isin; rf) ))) ) ||
        (* fence sync *)
        (( (tid_of a <> tid_of b)&amp;&amp;
          (is_fence a &amp;&amp; (is_release a &amp;&amp; (is_fence b &amp;&amp; (is_acquire b &amp;&amp;
          ( &exist; (x &isin; actions) (y &isin; actions). (loc_of x = loc_of y)&amp;&amp;
              (is_atomic_action x &amp;&amp; (is_atomic_action y &amp;&amp; (is_write x &amp;&amp;
              ((a,x)&isin; sb &amp;&amp; ((y,b)&isin; sb &amp;&amp;
              ( &exist; (z &isin; actions). (x,z)&isin; hrs &amp;&amp; ((z,y)&isin; rf))))))) ))))) ) ||
        (( (tid_of a <> tid_of b)&amp;&amp;
          (is_fence a &amp;&amp; (is_release a &amp;&amp; (is_atomic_action b &amp;&amp; (is_acquire b &amp;&amp;
          ( &exist; (x &isin; actions). (loc_of x = loc_of b)&amp;&amp;
            (is_atomic_action x &amp;&amp; (is_write x &amp;&amp; ((a,x)&isin; sb &amp;&amp;
            ( &exist; (z &isin; actions). (x,z)&isin; hrs &amp;&amp; ((z,b)&isin; rf) )))) ))))) ) ||
        ( (tid_of a <> tid_of b)&amp;&amp;
          (is_atomic_action a &amp;&amp; (is_release a &amp;&amp;
          (is_fence b &amp;&amp; (is_acquire b &amp;&amp;
          ( &exist; (x &isin; actions). (loc_of a = loc_of x)&amp;&amp; (is_atomic_action x &amp;&amp;
            ((x,b)&isin; sb &amp;&amp;
            ( &exist; (z &isin; actions). (a,z)&isin; rs &amp;&amp; ((z,x)&isin; rf) ))) ))))) )))) ))) )
<a name="synchronizes_with_set">


let synchronizes_with_set actions sb asw rf lo rs hrs =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       synchronizes_with actions sb asw rf lo rs hrs a b}
<a name="carries_a_dependency_to_set">

let carries_a_dependency_to_set actions sb dd rf = tc ( (rf ^cap; sb)&cup; dd )
<a name="dependency_ordered_before">

let dependency_ordered_before actions rf rs cad a d =
     a &isin; actions &amp;&amp; (d &isin; actions &amp;&amp;
     ( &exist; (b &isin; actions). is_release a &amp;&amp; (is_consume b &amp;&amp;
       ((&exist; (e &isin; actions). (a,e)&isin; rs &amp;&amp; ((e,b)&isin; rf))&amp;&amp;
       ( (b,d)&isin; cad || (b = d) ))) ))
<a name="dependency_ordered_before_set">

let dependency_ordered_before_set actions rf rs cad =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       dependency_ordered_before actions rf rs cad a b}
<a name="compose">


let compose R1 R2 =
    { (w,z) | &forall; ((w,x) &isin; R1) ((y,z) &isin; R2) | (x = y) }
<a name="inter_thread_happens_before"> 


let inter_thread_happens_before actions sb sw dob =
    let r = sw &cup; dob &cup; (compose sw sb) in
      tc (r &cup; (compose sb r))
<a name="consistent_ithb">


let consistent_ithb
      (Xo,Xw,("hb",hb)::_::_::("ithb",ithb)::_) =
    irrefl Xo.actions ithb 
<a name="happens_before">

let happens_before actions sb ithb =
    sb &cup; ithb 
<a name="dummy36">

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

let dummy36 = true 
<a name="consistent_sc">

let consistent_sc (Xo,Xw,("hb",hb)::_) =
    let all_sc_actions =
      { a | &forall; (a &isin; Xo.actions) |
        is_seq_cst a || (is_lock a || is_unlock a) } in
    let sc_happens_before = set_restrict hb (all_sc_actions) in
    let sc_mod_order = set_restrict Xw.mo all_sc_actions in
    strict_total_order_over all_sc_actions Xw.sc &amp;&amp;
    (sc_happens_before subset Xw.sc &amp;&amp;
    (sc_mod_order subset Xw.sc))
<a name="consistent_mo">


let consistent_mo (Xo,Xw,("hb",hb)::_) =
    trans Xo.actions Xw.mo &amp;&amp;
    (irrefl Xo.actions Xw.mo &amp;&amp;
    (&forall; (a &isin; Xo.actions) (b &isin; Xo.actions).
      ((a,b)&isin; Xw.mo)&rarr; (not ((b,a)&isin; hb)&amp;&amp;
      (((a,b)&isin; Xw.mo || ((b,a)&isin; Xw.mo))
      = ( is_write a &amp;&amp; (is_write b &amp;&amp;
          ((loc_of a = loc_of b)&amp;&amp;
          is_at_atomic_location Xo.lk a)) )))))
<a name="dummy37">


(* let consistent_mo_old (Xo,Xw,("hb",hb)::_) = *)
(*     (forall (a IN Xo.actions) (b IN Xo.actions). (a,b) IN Xw.mo --> ((loc_of a = loc_of b) && is_write a && is_write b)) && *)
(*     ( forall (l IN locations_of Xo.actions). *)
(*              match Xo.lk l with *)
(*           Atomic ->  *)
(*             ( let actions_at_l = {a | forall (a IN Xo.actions) | loc_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 (set_restrict Xw.mo actions_at_l) && *)
(*                 (* hb is a subset of mo at l *) *)
(*                 set_restrict hb writes_at_l subset Xw.mo ) *)
(*         | _      -> *)
(*             ( let actions_at_l = {a | forall (a IN Xo.actions) | loc_of a = Some l} in *)
(*                 Set.is_empty (set_restrict Xw.mo actions_at_l) ) end  *)


(*********************************************** *)
(*   - 3.7 - Visible side effects *)
(*********************************************** *)


(* let visible_side_effect actions hb a b = *)
(*     (a,b) IN hb && *)
(*     is_write a && is_read b && (loc_of a = loc_of b) && *)
(*     not ( exists (c IN actions). not (c = a) && not (c = b) && *)
(*           is_write c && (loc_of c = loc_of b) && *)
(*           (a,c) IN hb && (c,b) IN hb) *)

let dummy37 = true 
<a name="visible_side_effect_set">

let visible_side_effect_set actions hb =
    { (a,b) | &forall; ((a,b) &isin; hb) |
      is_write a &amp;&amp; (is_read b &amp;&amp; ((loc_of a = loc_of b)&amp;&amp;
      not ( &exist; (c &isin; actions). not (c &isin; {a;b})&amp;&amp;
          (is_write c &amp;&amp; ((loc_of c = loc_of b)&amp;&amp;
          ((a,c)&isin; hb &amp;&amp; ((c,b)&isin; hb))))))) }
<a name="dummy38">


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

let dummy38 = true 
<a name="det_read">

let det_read (Xo,Xw,("hb",hb)::_) =
    &forall; (r &isin; Xo.actions).
      is_read r &rarr;
      (( &exist; (w &isin; Xo.actions).
          is_write w &amp;&amp; ((loc_of w = loc_of r)&amp;&amp; ((w,r)&isin; hb)) ) =
      (&exist; (w' &isin; Xo.actions). (w',r)&isin; Xw.rf))
<a name="consistent_non_atomic_rf">

let consistent_non_atomic_rf (Xo,Xw,("hb",hb)::("vse",vse)::_) =
    &forall; ((w,r) &isin; Xw.rf). is_at_non_atomic_location Xo.lk r &rarr;
      ((w,r)&isin; vse)
<a name="consistent_atomic_rf">

let consistent_atomic_rf (Xo,Xw,("hb",hb)::_) =
    &forall; ((w,r) &isin; Xw.rf). is_at_atomic_location Xo.lk r &rarr;
        not ((r,w)&isin; hb)
<a name="consistent_non_atomic_read_values">


let consistent_non_atomic_read_values (Xo,Xw,("hb",hb)::("vse",vse)::_) =
    &forall; (b &isin; Xo.actions).
    (is_read b &amp;&amp; is_at_non_atomic_location Xo.lk b)&rarr;
      ( if (&exist; (a_vse &isin; Xo.actions). (a_vse,b)&isin; vse)
        then (&exist; (a_vse &isin; Xo.actions). (a_vse,b)&isin; vse &amp;&amp; ((a_vse,b)&isin; Xw.rf))
        else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) )
<a name="consistent_non_atomic_read_values_rejig">

let consistent_non_atomic_read_values_rejig (Xo,Xw,("hb",hb)::("vse",vse)::_) =
    &forall; (b &isin; Xo.actions).
    (is_read b &amp;&amp; is_at_non_atomic_location Xo.lk b)&rarr;
      ( if (&exist; (w &isin; Xo.actions). (w,b)&isin; hb &amp;&amp; is_write w)
        then (&exist; (a_vse &isin; Xo.actions). (a_vse,b)&isin; vse &amp;&amp; ((a_vse,b)&isin; Xw.rf))
        else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) )
<a name="no_vsse_consistent_atomic_read_values">


let no_vsse_consistent_atomic_read_values (Xo,Xw,("hb",hb)::("vse",vse)::_) =
    &forall; (b &isin; Xo.actions).
    (is_read b &amp;&amp; is_at_atomic_location Xo.lk b)&rarr;
      ( if (&exist; (a_vse &isin; Xo.actions). (a_vse,b)&isin; vse)
        then (&exist; (a &isin; Xo.actions). ((a,b)&isin; Xw.rf)&amp;&amp; not ((b,a)&isin; hb))
        else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) )
<a name="no_vsse_consistent_atomic_read_values_rejig">


let no_vsse_consistent_atomic_read_values_rejig (Xo,Xw,("hb",hb)::("vse",vse)::_) =
    &forall; (b &isin; Xo.actions).
    (is_read b &amp;&amp; is_at_atomic_location Xo.lk b)&rarr;
      ( if (&exist; (w &isin; Xo.actions). (w,b)&isin; hb &amp;&amp; is_write w)
        then (&exist; (a &isin; Xo.actions). ((a,b)&isin; Xw.rf)&amp;&amp; not ((b,a)&isin; hb))
        else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) )
<a name="dummy38'">


(* let coherent_memory_use_old (Xo,Xw,("hb",hb)::_) = *)
(*     (* CoRR *) *)
(*     ( forall ((x,a) IN Xw.rf) ((y,b) IN Xw.rf). *)
(*       ((a,b) IN hb && (loc_of a = loc_of b) && is_at_atomic_location Xo.lk b) --> *)
(*       ((x = y) || (x,y) IN Xw.mo) ) && *)
(*     (* CoWR *)     *)
(*     ( forall ((a,b) IN hb) (c IN Xo.actions). *)
(*       ((c,b) IN Xw.rf && is_write a && (loc_of a = loc_of b) && is_at_atomic_location Xo.lk b) --> *)
(*       ((c = a) || (a,c) IN Xw.mo) ) && *)
(*     (* CoRW *) *)
(*     ( forall ((a,b) IN hb) (c IN Xo.actions). *)
(*       ((c,a) IN Xw.rf && is_write b && (loc_of a = loc_of b) && is_at_atomic_location Xo.lk a) --> *)
(*       ((c,b) IN Xw.mo) ) *)

let dummy38' = true 
<a name="coherent_memory_use">

let coherent_memory_use (Xo,Xw,("hb",hb)::_) =
    (* CoRR *)
    ( not ( &exist; ((a,b) &isin; Xw.rf) ((c,d) &isin; Xw.rf).
              (b,d)&isin; hb &amp;&amp; ((c,a)&isin; Xw.mo) ) )&amp;&amp;
    (* CoWR *)    
    (( not ( &exist; ((a,b) &isin; Xw.rf) (c &isin; Xo.actions).
              (c,b)&isin; hb &amp;&amp; ((a,c)&isin; Xw.mo) ) )&amp;&amp;
    (* CoRW *)
    (( not ( &exist; ((a,b) &isin; Xw.rf) (c &isin; Xo.actions).
              (b,c)&isin; hb &amp;&amp; ((c,a)&isin; Xw.mo) ) )&amp;&amp;
    (* CoRW *)
    ( not (&exist; ((a,b) &isin; hb). (b,a)&isin; Xw.mo) )))
<a name="rmw_atomicity">

let rmw_atomicity (Xo,Xw,("hb",hb)::_) =
    &forall; ((a,b) &isin; Xw.rf).
    is_RMW b &rarr; adjacent_less_than Xw.mo Xo.actions a b 
<a name="sc_reads_restricted">

let sc_reads_restricted (Xo,Xw,("hb",hb)::_) =
    &forall; ((a,b) &isin; Xw.rf).
      is_seq_cst b &rarr;
      (( adjacent_less_than_such_that
          (fun c -> is_write c &amp;&amp; (loc_of c = loc_of b)) Xw.sc Xo.actions a b ) ||
      ( not (is_seq_cst a)&amp;&amp;
        ( &forall; (x &isin; Xo.actions).
            ( adjacent_less_than_such_that
                (fun c -> is_write c &amp;&amp; (loc_of c = loc_of b)) Xw.sc Xo.actions x b )&rarr; not ((a,x)&isin; hb) ) ))
<a name="sc_fences_heeded">


let sc_fences_heeded (Xo,Xw,("hb",hb)::_) =
    (* fence restriction N3291 29.3p4 *)
    ( &forall; (a &isin; Xo.actions) ((x,b) &isin; Xo.sb) (y &isin; Xo.actions).
      ( is_fence x &amp;&amp; (is_atomic_action b &amp;&amp;
        (( adjacent_less_than_such_that
          (fun c -> is_write c &amp;&amp; (loc_of c = loc_of b)) Xw.sc Xo.actions a x )&amp;&amp;
        ((y,b)&isin; Xw.rf))))&rarr;
      ((y = a) || ((a,y)&isin; Xw.mo)) )&amp;&amp;
    (* fence restriction N3291 29.3p5 *)
    (( &forall; ((a,x) &isin; Xo.sb) ((y,b) &isin; Xw.rf).
      ((is_atomic_action a &amp;&amp; (is_write a &amp;&amp;
        (is_fence x &amp;&amp; (is_atomic_action b &amp;&amp; ((x,b)&isin; Xw.sc &amp;&amp;
        (loc_of a = loc_of b))))))&rarr;
      ((y = a) || ((a,y)&isin; Xw.mo)) ) )&amp;&amp;
    (* fence restriction N3291 29.3p6 *)
    (( &forall; ((a,x) &isin; Xo.sb) ((y,b) &isin; Xo.sb) (z &isin; Xo.actions).
      ( is_atomic_action a &amp;&amp; (is_write a &amp;&amp;
        (is_fence x &amp;&amp; (is_fence y &amp;&amp; ((x,y)&isin; Xw.sc &amp;&amp;
        (is_atomic_action b &amp;&amp; ((loc_of a = loc_of b)&amp;&amp;
        ((z,b)&isin; Xw.rf))))))))&rarr;
      ((z = a) || ((a,z)&isin; Xw.mo)) )&amp;&amp;
    (* SC fences impose mo N3291 29.3p7 *)
    (( &forall; ((a,x) &isin; Xo.sb) ((y,b) &isin; Xo.sb).
      ( (is_atomic_action a &amp;&amp; (is_write a &amp;&amp;
        (is_atomic_action b &amp;&amp; (is_write b &amp;&amp;
        (is_fence x &amp;&amp; (is_fence y &amp;&amp; ((x,y)&isin; Xw.sc &amp;&amp;
        (loc_of a = loc_of b))))))))&rarr;
      ((a,b)&isin; Xw.mo)) )&amp;&amp;
    (* SC fences impose mo N3291 29.3p7, w collapsed first write*)
    (( &forall; (a &isin; Xo.actions) ((y,b) &isin; Xo.sb).
      ( (is_atomic_action a &amp;&amp; (is_write a &amp;&amp;
        (is_fence y &amp;&amp; ((a,y)&isin; Xw.sc &amp;&amp;
        (is_atomic_action b &amp;&amp; (is_write b &amp;&amp;
        (loc_of a = loc_of b)))))))&rarr;
      ((a,b)&isin; Xw.mo)) )&amp;&amp;
    (* SC fences impose mo N3291 29.3p7, w collapsed second write*)
    ( &forall; ((a,x) &isin; Xo.sb) (b &isin; Xo.actions).
      ( (is_atomic_action a &amp;&amp; (is_write a &amp;&amp;
        (is_fence x &amp;&amp; (is_atomic_action b &amp;&amp; (is_write b &amp;&amp; ((x,b)&isin; Xw.sc &amp;&amp;
        (loc_of a = loc_of b)))))))&rarr;
      ((a,b)&isin; Xw.mo)) )))))
<a name="no_vsse_consistent_rf">


let no_vsse_consistent_rf X =
    consistent_non_atomic_read_values X &amp;&amp;
    (no_vsse_consistent_atomic_read_values X &amp;&amp;
    (coherent_memory_use X &amp;&amp;
    (rmw_atomicity X &amp;&amp;
    (sc_reads_restricted X &amp;&amp;
    sc_fences_heeded X))))
<a name="no_vsse_consistent_rf_rejig">


let no_vsse_consistent_rf_rejig X =
    det_read X &amp;&amp;
    (consistent_non_atomic_rf X &amp;&amp;
    (consistent_atomic_rf X &amp;&amp;
    (coherent_memory_use X &amp;&amp;
    (rmw_atomicity X &amp;&amp;
    (sc_reads_restricted X &amp;&amp;
    sc_fences_heeded X)))))
<a name="dummy39">


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

let dummy39 = true 
<a name="indeterminate_reads">

let indeterminate_reads (Xo,Xw,("hb",hb)::_) =
    {b | &forall; (b &isin; Xo.actions) | is_read b &amp;&amp; not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf)}
<a name="unsequenced_races">

let unsequenced_races (Xo,Xw,("hb",hb)::_) =
    { (a,b) | &forall; (a &isin; Xo.actions) (b &isin; Xo.actions) |
        not (a = b)&amp;&amp; ((loc_of a = loc_of b)&amp;&amp; ((is_write a || is_write b)&amp;&amp;
        ((tid_of a = tid_of b)&amp;&amp;
        not ((a,b)&isin; Xo.sb || ((b,a)&isin; Xo.sb)))))  }
<a name="data_races">

let data_races (Xo,Xw,("hb",hb)::_) =
    { (a,b) | &forall; (a &isin; Xo.actions) (b &isin; Xo.actions) |
        not (a = b)&amp;&amp; ((loc_of a = loc_of b)&amp;&amp; ((is_write a || is_write b)&amp;&amp;
        ((tid_of a <> tid_of b)&amp;&amp;
        (not (is_atomic_action a &amp;&amp; is_atomic_action b)&amp;&amp;
        not ((a,b)&isin; hb || ((b,a)&isin; hb))))))  }
<a name="good_mutex_use">


let good_mutex_use actions lk sb lo a =
    let mutexes_at_l =
      {a' | &forall; (a' &isin; actions) | (is_lock a' || is_unlock a')&amp;&amp; (loc_of a' = loc_of a)}
    in
    let lock_order = set_restrict lo mutexes_at_l in
    (* violated requirement: The calling thread shall own the mutex. *)
    ( is_unlock a &rarr; ( &exist; (al &isin; actions).
              is_successful_lock al &amp;&amp; ((al,a)&isin; sb &amp;&amp;
              adjacent_less_than lock_order actions al a) ) )&amp;&amp;
    (* violated requirement: The calling thread does not own the mutex. *)
    ( is_lock a &rarr;
      not ( &exist; (al &isin; actions).
          is_successful_lock al &amp;&amp; ((tid_of a = tid_of al)&amp;&amp;
          adjacent_less_than lock_order actions al a) ) )
<a name="bad_mutexes">


let bad_mutexes (Xo,Xw,("hb",hb)::_) =
  { a | &forall; (a &isin; Xo.actions) | not (good_mutex_use Xo.actions Xo.lk Xo.sb Xw.sc a)}
<a name="undefined_behaviour">


let undefined_behaviour =
  [ Two ("data_races", data_races);
    Two ("unsequenced_races", unsequenced_races);
    One ("indeterminate_reads", indeterminate_reads);
    One ("bad_mutexes", bad_mutexes) ]
<a name="dummy310">


(*********************************************** *)
(* 3.10 - Consistent execution *)
(*********************************************** *)

let dummy310 = true 
<a name="no_vsse_relations">

let no_vsse_relations Xo Xw =
    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 hb in
    [ ("hb", hb);
      ("vse", vse);
      ("ithb", ithb);
      ("dob", dob);
      ("cad", cad);
      ("sw", sw);
      ("hrs", hrs);
      ("rs", rs) ]
<a name="no_vsse_consistent_execution">

let no_vsse_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_locks", Leaf consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("consistent_sc", Leaf consistent_sc);
         ("consistent_mo", Leaf consistent_mo);
         ("consistent_rf",
           Node [ ("consistent_non_atomic_read_values",
                     Leaf consistent_non_atomic_read_values);
                  ("no_vsse_consistent_atomic_read_values",
                     Leaf no_vsse_consistent_atomic_read_values);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="no_vsse_consistent_execution_rejig">


let no_vsse_consistent_execution_rejig =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_locks", Leaf consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("consistent_mo", Leaf consistent_mo);
         ("consistent_sc", Leaf consistent_sc);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf", Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="dummy312">


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

let dummy312 = true 
<a name="no_vsse_memory_model">

let no_vsse_memory_model =
  <| consistent = no_vsse_consistent_execution;
     relation_calculation = no_vsse_relations;
(*     protocol = true_protocol;*)
     undefined = undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = None;
           ao_flag  = false;
           tot_flag = false |>
  |>


val no_vsse_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy4">


(*********************************************** <a name="standard">*)
(* 4 - Standard C/C++ memory_model *)
(*********************************************** *)

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

let dummy4 = true 
<a name="visible_sequence_of_side_effects_tail">

let visible_sequence_of_side_effects_tail actions mo hb vsse_head b =
    { c | &forall; (c &isin; actions) |
      (vsse_head,c)&isin; mo &amp;&amp; (not ((b,c)&isin; hb)&amp;&amp;
      ( &forall; (a &isin; actions).
          ((vsse_head,a)&isin; mo &amp;&amp; ((a,c)&isin; mo))&rarr; not ((b,a)&isin; hb) )) }
<a name="visible_sequence_of_side_effects">

(* visible sequences of side effects have been proven redundant. See the simpler memory_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}&cup;
             visible_sequence_of_side_effects_tail actions mo hb vsse_head b
           else
             {})
<a name="visible_sequences_of_side_effects_set">

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 &isin; actions) (b &isin; actions) | 
  is_at_atomic_location lk b &amp;&amp; (is_read b &amp;&amp;
  ((vsse_head,b)&isin; vse)) }
<a name="visible_sequence_of_side_effects_relation">

let visible_sequence_of_side_effects_relation actions lk mo hb vse =
  { (v,b) | &forall; (b &isin; actions) (v &isin; actions) (vsse_head &isin; actions) |
    is_at_atomic_location lk b &amp;&amp; (is_read b &amp;&amp; (((vsse_head,b)&isin; vse)&amp;&amp;
    (v = vsse_head || (v &isin; visible_sequence_of_side_effects_tail actions mo hb vsse_head b)))) }
<a name="relations">


let relations Xo Xw =
    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 hb in
    let vsses = visible_sequence_of_side_effects_relation Xo.actions Xo.lk Xw.mo hb vse in
    [ ("hb", hb);
      ("vse", vse);
      ("vsses", vsses);
      ("ithb", ithb);
      ("dob", dob);
      ("cad", cad);
      ("sw", sw);
      ("hrs", hrs);
      ("rs", rs) ]
<a name="consistent_atomic_read_values_old">


let consistent_atomic_read_values_old (Xo,Xw,("hb",hb)::("vse",vse)::("vsses",vsses)::_) =
    &forall; (b &isin; Xo.actions).
    (is_read b &amp;&amp; is_at_atomic_location Xo.lk b)&rarr;
      ( if (&exist; ((b',v) &isin; vsses). b = b')
        then ( &exist; ((b',v) &isin; vsses). b = b' &amp;&amp;
               (&exist; (c &isin; v). (c,b)&isin; Xw.rf) )
        else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) )
<a name="consistent_atomic_read_values">


let consistent_atomic_read_values (Xo,Xw,("hb",hb)::("vse",vse)::("vsses",vsses)::_) =
    &forall; (b &isin; Xo.actions).
    (is_read b &amp;&amp; is_at_atomic_location Xo.lk b)&rarr;
      ( if (&exist; (v &isin; Xo.actions). (v,b)&isin; vsses)
        then ( &exist; (v' &isin; Xo.actions). (v',b)&isin; vsses &amp;&amp; ((v',b)&isin; Xw.rf) )
        else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) )
<a name="consistent_execution">


let consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("consistent_locks", Leaf consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("consistent_sc", Leaf consistent_sc);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("consistent_non_atomic_read_values",
                     Leaf consistent_non_atomic_read_values);
                  ("consistent_atomic_read_values",
                     Leaf consistent_atomic_read_values);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="dummy41">


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

let dummy41 = true 
<a name="cmm_memory_model">

let cmm_memory_model =
  <| consistent = consistent_execution;
     relation_calculation = relations;
(*     protocol = true_protocol;*)
     undefined = undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = None;
           ao_flag  = false;
           tot_flag = false |>
  |>


val cmm_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy5">


(*********************************************** *)
(* 5 - Memory_Model with separate lock order *)
(*********************************************** *)

(* A version of the no VSSE memory_model with a separate lock order. *)

let dummy5 = true 
<a name="separate_lo_consistent_sc">

let separate_lo_consistent_sc (Xo,Xw,("hb",hb)::_) =
    let all_sc_actions =
      { a | &forall; (a &isin; Xo.actions) | is_seq_cst a } in
    let sc_happens_before = set_restrict hb (all_sc_actions) in
    let sc_mod_order =
      set_restrict Xw.mo all_sc_actions in
    strict_total_order_over all_sc_actions Xw.sc &amp;&amp;
    (sc_happens_before subset Xw.sc &amp;&amp;
    (sc_mod_order subset Xw.sc))
<a name="separate_lo_consistent_lo">


let separate_lo_consistent_lo (Xo,Xw,("hb",hb)::_) =
    let all_lo_actions =
      { a | &forall; (a &isin; Xo.actions) | is_lock a || is_unlock a } in
    let lo_happens_before = set_restrict hb all_lo_actions in
    strict_total_order_over all_lo_actions Xw.lo &amp;&amp;
    (lo_happens_before subset Xw.lo)
<a name="separate_lo_consistent_locks">


let separate_lo_consistent_locks (Xo,Xw,("hb",hb)::_) =
    (&forall; ((a,c) &isin; Xw.lo). 
      (is_successful_lock a &amp;&amp; (is_successful_lock c &amp;&amp; (loc_of a = loc_of c)))&rarr; 
      (&exist; (b &isin; Xo.actions). (loc_of a = loc_of b)&amp;&amp; (is_unlock b &amp;&amp; ((a,b)&isin; Xw.lo &amp;&amp; ((b,c)&isin; Xw.lo)))))
<a name="no_vsse_separate_lo_relations">


let no_vsse_separate_lo_relations Xo Xw =
    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.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 hb in
    [ ("hb", hb);
      ("vse", vse);
      ("ithb", ithb);
      ("dob", dob);
      ("cad", cad);
      ("sw", sw);
      ("hrs", hrs);
      ("rs", rs) ]
<a name="separate_lo_consistent_execution">


let separate_lo_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("separate_lo_consistent_locks",
            Leaf separate_lo_consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("separate_lo_consistent_sc", Leaf separate_lo_consistent_sc);
         ("separate_lo_consistent_lo", Leaf separate_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="separate_lo_bad_mutexes">


let separate_lo_bad_mutexes (Xo,Xw,("hb",hb)::_) =
  { a | &forall; (a &isin; Xo.actions) | not (good_mutex_use Xo.actions Xo.lk Xo.sb Xw.lo a)}
<a name="separate_lo_undefined_behaviour">


let separate_lo_undefined_behaviour =
  [ Two ("data_races", data_races);
    Two ("unsequenced_races", unsequenced_races);
    One ("indeterminate_reads", indeterminate_reads);
    One ("separate_lo_bad_mutexes", separate_lo_bad_mutexes) ]
<a name="dummy51">


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

let dummy51 = true 
<a name="separate_lo_memory_model">

let separate_lo_memory_model =
  <| consistent = separate_lo_consistent_execution;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_calculation = no_vsse_separate_lo_relations;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Global_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val separate_lo_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy6">


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

(* This memory_model uses per-location lock orders rather than a shared one. *)

let dummy6 = true 
<a name="multi_lo_consistent_lo">

let multi_lo_consistent_lo (Xo,Xw,("hb",hb)::_) =
    let mutex_actions =
      { a | &forall; (a &isin; Xo.actions) | is_lock a || is_unlock a } in
    let mutex_hb = set_restrict hb mutex_actions in
    relation_over mutex_actions Xw.lo &amp;&amp;
    (locationwise mutex_actions Xw.lo &amp;&amp;
    (strict_partial_order mutex_actions Xw.lo &amp;&amp;
    (per_location_total mutex_actions Xw.lo &amp;&amp;
    (mutex_hb subset Xw.lo))))
<a name="multi_lo_consistent_locks">


let multi_lo_consistent_locks (Xo,Xw,("hb",hb)::_) =
    (&forall; ((a,c) &isin; Xw.lo). 
      (is_successful_lock a &amp;&amp; is_successful_lock c)&rarr; 
      (&exist; (b &isin; Xo.actions). is_unlock b &amp;&amp; ((a,b)&isin; Xw.lo &amp;&amp; ((b,c)&isin; Xw.lo))))
<a name="multi_lo_consistent_execution">


let multi_lo_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("multi_lo_consistent_locks", Leaf multi_lo_consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("separate_lo_consistent_sc", Leaf separate_lo_consistent_sc);
         ("multi_lo_consistent_lo", Leaf multi_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="dummy61">


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

let dummy61 = true 
<a name="multi_lo_memory_model">

let multi_lo_memory_model =
  <| consistent = multi_lo_consistent_execution;
     relation_calculation = no_vsse_separate_lo_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val multi_lo_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy6a">


(*********************************************** *)
(* 6a - Memory_Model with per-location lock orders and sc coherence *)
(*********************************************** *)

let dummy6a = true 
<a name="sc_coherent">

let sc_coherent (Xo,Xw,("hb",hb)::_) =
    (* CoRR *)
    ( not
      ( &exist; ((x,a) &isin; Xw.rf) ((y,b) &isin; Xw.rf).
          (loc_of a = loc_of b)&amp;&amp; (is_at_atomic_location Xo.lk b &amp;&amp;
          ((a,b)&isin; Xw.sc &amp;&amp;
          ((x,y)&isin; Xw.mo))) ) )&amp;&amp;
    (* CoWR *)    
    (( not
      ( &exist; ((x,a) &isin; Xw.rf) ((y,b) &isin; Xw.rf).
          (loc_of a = loc_of b)&amp;&amp; (is_at_atomic_location Xo.lk b &amp;&amp;
          ((a,b)&isin; Xw.sc &amp;&amp;
          ((x,y)&isin; Xw.mo))) ) )&amp;&amp;
    (* CoRW *)
    (( not
      ( &exist; ((a,b) &isin; Xw.sc) (c &isin; Xo.actions).
          (loc_of a = loc_of b)&amp;&amp; (is_at_atomic_location Xo.lk a &amp;&amp;
          ((c,a)&isin; Xw.rf &amp;&amp;
          ((c,b)&isin; Xw.mo))) ) )&amp;&amp;
    (* CoRR *)
    (( not
      ( &exist; ((x,a) &isin; Xw.rf) ((y,b) &isin; Xw.rf).
          (loc_of a = loc_of b)&amp;&amp; (is_at_atomic_location Xo.lk b &amp;&amp;
          ((a,b)&isin; hb &amp;&amp;
          ((x,y)&isin; Xw.sc))) ) )&amp;&amp;
    (* CoWR *)    
    (( not
      ( &exist; ((x,a) &isin; Xw.rf) ((y,b) &isin; Xw.rf).
          (loc_of a = loc_of b)&amp;&amp; (is_at_atomic_location Xo.lk b &amp;&amp;
          ((a,b)&isin; hb &amp;&amp;
          ((x,y)&isin; Xw.sc))) ) )&amp;&amp;
    (* CoRW *)
    ( not
      ( &exist; ((a,b) &isin; hb) (c &isin; Xo.actions).
          (loc_of a = loc_of b)&amp;&amp; (is_at_atomic_location Xo.lk a &amp;&amp;
          ((c,a)&isin; Xw.rf &amp;&amp;
          ((c,b)&isin; Xw.sc))) ) )))))
<a name="sc_coherent_execution">


let sc_coherent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("multi_lo_consistent_locks", Leaf multi_lo_consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("separate_lo_consistent_sc", Leaf separate_lo_consistent_sc);
         ("multi_lo_consistent_lo", Leaf multi_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]);
         ("sc_coherent", Leaf sc_coherent) ]
<a name="dummy6a1">


(*********************************************** *)
(*   - 6a.1  - sc coherent top level judgement *)
(*********************************************** *)

let dummy6a1 = true 
<a name="sc_coherent_memory_model">

let sc_coherent_memory_model =
  <| consistent = sc_coherent_execution;
     relation_calculation = no_vsse_separate_lo_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val sc_coherent_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy6b">


(*********************************************** *)
(* 6b - Memory_Model with per-location lock orders and strong coherence *)
(*********************************************** *)

let dummy6b = true 
<a name="strong_coherence">

let strong_coherence (Xo,Xw,("hb",hb)::_) =
    let fr = { (a,b)
             | &forall; (a &isin; Xo.actions) (b &isin; Xo.actions)
             | &exist; (c &isin; Xo.actions). ((c,a)&isin; Xw.rf)&amp;&amp; ((c,b)&isin; Xw.mo) } in
    irrefl Xo.actions (tc
      ( compose Xw.sc (Xw.sc &cup; Xw.mo &cup; Xw.rf &cup; hb &cup; fr) ))
<a name="strong_coherence_execution">


let strong_coherence_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("multi_lo_consistent_locks", Leaf multi_lo_consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("separate_lo_consistent_sc", Leaf separate_lo_consistent_sc);
         ("multi_lo_consistent_lo", Leaf multi_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
(*                ("coherent_memory_use", Leaf coherent_memory_use);*)
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]);
         ("strong_coherence", Leaf strong_coherence) ]
<a name="dummy6b1">


(*********************************************** *)
(*   - 6b.1  - strong coherence top level judgement *)
(*********************************************** *)

let dummy6b1 = true 
<a name="strong_coherence_memory_model">

let strong_coherence_memory_model =
  <| consistent = strong_coherence_execution;
     relation_calculation = no_vsse_separate_lo_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val strong_coherence_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy7">


(*********************************************** *)
(* 7 - Memory_Model with per-location lock orders and sc order *)
(*********************************************** *)

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

let dummy7 = true 
<a name="multi_sc_consistent_sc">

let multi_sc_consistent_sc (Xo,Xw,("hb",hb)::_) =
    let all_sc_actions =
      { a | &forall; (a &isin; Xo.actions) | is_seq_cst a } in
    let sc_happens_before = set_restrict hb all_sc_actions in
    let sc_mod_order = set_restrict Xw.mo all_sc_actions in
    relation_over all_sc_actions Xw.sc &amp;&amp;
    (locationwise all_sc_actions Xw.sc &amp;&amp;
    (strict_partial_order all_sc_actions Xw.sc &amp;&amp;
    (per_location_total all_sc_actions Xw.sc &amp;&amp;
    (sc_happens_before subset Xw.sc &amp;&amp;
    (sc_mod_order subset Xw.sc)))))
<a name="multi_sc_consistent_execution">


let multi_sc_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("multi_lo_consistent_locks",
            Leaf multi_lo_consistent_locks);
         ("consistent_ithb", Leaf consistent_ithb);
         ("multi_sc_consistent_sc", Leaf multi_sc_consistent_sc);
         ("multi_lo_consistent_lo", Leaf multi_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="dummy71">


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

let dummy71 = true 
<a name="multi_sc_memory_model">

let multi_sc_memory_model =
  <| consistent = multi_sc_consistent_execution;
     relation_calculation = no_vsse_separate_lo_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val multi_sc_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy8">


(*********************************************** *)
(* 8 - Memory_Model with single step mutex synchronisation *)
(*********************************************** *)

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

let dummy8 = true 
<a name="lo_single_synchronizes_with">

let lo_single_synchronizes_with actions sb asw rf lo rs hrs a b =
    (* thread sync *)
    (a,b)&isin; asw ||
    ( (loc_of a = loc_of b)&amp;&amp; (a &isin; actions &amp;&amp; (b &isin; actions &amp;&amp;
      ( (* mutex sync *)
        (is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo &amp;&amp; not (&exist; (c &isin; actions). (a,c)&isin; lo &amp;&amp; ((c,b)&isin; lo))))) ||
        (* rel/acq sync *)
        (( is_release a &amp;&amp; (is_acquire b &amp;&amp; ((tid_of a <> tid_of b)&amp;&amp;
          (&exist; (c &isin; actions). (a,c)&isin; rs &amp;&amp; ((c,b)&isin; rf) ))) ) ||
        (* fence sync *)
        (( (tid_of a <> tid_of b)&amp;&amp;
          (is_fence a &amp;&amp; (is_release a &amp;&amp; (is_fence b &amp;&amp; (is_acquire b &amp;&amp;
          ( &exist; (x &isin; actions) (y &isin; actions). (loc_of x = loc_of y)&amp;&amp;
              (is_atomic_action x &amp;&amp; (is_atomic_action y &amp;&amp; (is_write x &amp;&amp;
              ((a,x)&isin; sb &amp;&amp; ((y,b)&isin; sb &amp;&amp;
              ( &exist; (z &isin; actions). (x,z)&isin; hrs &amp;&amp; ((z,y)&isin; rf))))))) ))))) ) ||
        (( (tid_of a <> tid_of b)&amp;&amp;
          (is_fence a &amp;&amp; (is_release a &amp;&amp; (is_atomic_action b &amp;&amp; (is_acquire b &amp;&amp;
          ( &exist; (x &isin; actions). (loc_of x = loc_of b)&amp;&amp;
            (is_atomic_action x &amp;&amp; (is_write x &amp;&amp; ((a,x)&isin; sb &amp;&amp;
            ( &exist; (z &isin; actions). (x,z)&isin; hrs &amp;&amp; ((z,b)&isin; rf) )))) ))))) ) ||
        ( (tid_of a <> tid_of b)&amp;&amp;
          (is_atomic_action a &amp;&amp; (is_release a &amp;&amp;
          (is_fence b &amp;&amp; (is_acquire b &amp;&amp;
          ( &exist; (x &isin; actions). (loc_of a = loc_of x)&amp;&amp; (is_atomic_action x &amp;&amp;
            ((x,b)&isin; sb &amp;&amp;
            ( &exist; (z &isin; actions). (a,z)&isin; rs &amp;&amp; ((z,x)&isin; rf) ))) ))))) )))) ))) )
<a name="lo_single_synchronizes_with_set">


let lo_single_synchronizes_with_set actions sb asw rf lo rs hrs =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       lo_single_synchronizes_with actions sb asw rf lo rs hrs a b}
<a name="lo_single_relations">


let lo_single_relations Xo Xw =
    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 Xw.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 hb in
    [ ("hb", hb);
      ("vse", vse);
      ("ithb", ithb);
      ("dob", dob);
      ("cad", cad);
      ("sw", sw);
      ("hrs", hrs);
      ("rs", rs) ]
<a name="dummy81">


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

let dummy81 = true 
<a name="lo_single_memory_model">

let lo_single_memory_model =
  <| consistent = multi_sc_consistent_execution;
     relation_calculation = lo_single_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val lo_single_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy9">


(*********************************************** *)
(* 9 - Memory_Model simplified for programs without consumes *)
(*********************************************** *)

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

let dummy9 = true 
<a name="no_consume_hb">

let no_consume_hb sb sw =
    tc (sb &cup; sw)
<a name="no_consume_relations">


let no_consume_relations Xo Xw =
    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 Xw.lo rs hrs in
    let hb    = no_consume_hb Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("sw", sw);
      ("hrs", hrs);
      ("rs", rs) ]
<a name="no_consume_consistent_hb">


let no_consume_consistent_hb (Xo,Xw,("hb",hb)::_) =
    irrefl Xo.actions hb 
<a name="no_consume_consistent_execution">


let no_consume_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("multi_lo_consistent_locks", Leaf multi_lo_consistent_locks);
         ("no_consume_consistent_hb", Leaf no_consume_consistent_hb);
         ("multi_sc_consistent_sc", Leaf multi_sc_consistent_sc);
         ("multi_lo_consistent_lo", Leaf multi_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="dummy91">


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

let dummy91 = true 
<a name="no_consume_memory_model">

let no_consume_memory_model =
  <| consistent = no_consume_consistent_execution;
     relation_calculation = no_consume_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val no_consume_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy10">


(*********************************************** *)
(* 10 - Memory_Model simplified for programs without consumes or relaxed *)
(*********************************************** *)

(* Without relaxed, can release sequences go? Unfortunately not. This
memory_model is NOT equivalent without the extra condition that
initialisation of atomics happen-before all accesses of that atomic.
The reason is that non-atomic initialisation can be one of the writes
in the release sequence that immediately precedes an RMW. Then in this
memory_model, there is no hb from the release to the read of the RMW, but
there is in the preferred memory_model. Then we can construct an execution
with a race in the preffered memory_model that is inconsitent on this
memory_model. *)

let dummy10 = true 
<a name="rel_acq_sc_synchronizes_with">

let rel_acq_sc_synchronizes_with actions sb asw rf lo a b =
    (* thread sync *)
    (a,b)&isin; asw ||
    (* mutex sync *)
    ((is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo))) ||
    (* rel/acq sync *)
    ( is_release a &amp;&amp; (is_acquire b &amp;&amp; ((tid_of a <> tid_of b)&amp;&amp; ((a,b)&isin; rf))) ))
<a name="rel_acq_sc_synchronizes_with_set">


let rel_acq_sc_synchronizes_with_set actions sb asw rf lo =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       rel_acq_sc_synchronizes_with actions sb asw rf lo a b}
<a name="rel_acq_sc_relations">


let rel_acq_sc_relations Xo Xw =
    let sw    = rel_acq_sc_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.lo in
    let hb    = no_consume_hb Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("sw", sw) ]
<a name="rel_acq_sc_consistent_execution">


let rel_acq_sc_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("multi_lo_consistent_locks", Leaf multi_lo_consistent_locks);
         ("no_consume_consistent_hb", Leaf no_consume_consistent_hb);
         ("multi_sc_consistent_sc", Leaf multi_sc_consistent_sc);
         ("multi_lo_consistent_lo", Leaf multi_lo_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read",
                     Leaf det_read);
                  ("consistent_non_atomic_rf",
                     Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf",
                     Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_reads_restricted", Leaf sc_reads_restricted);
                  ("sc_fences_heeded", Leaf sc_fences_heeded) ]) ]
<a name="not_rel_acq_sc">


let not_rel_acq_sc (Xo,Xw,("hb",hb)::_) =
  { a | &forall; (a &isin; Xo.actions) | 
    match a with
    | Lock _ _ _ _            -> false
    | Unlock _ _ _            -> false
    | Load _ _ mo _ _         -> not (mo &isin; {NA;Acquire})
    | Store _ _ mo _ _        -> not (mo &isin; {NA;Release})
    | RMW _ _ mo _ _ _        -> mo <> Acq_rel
    | Fence _ _ _             -> true
    | Blocked_rmw _ _ _       -> false
    end
}
<a name="rel_acq_sc_undefined_behaviour">


let rel_acq_sc_undefined_behaviour =
  [ Two ("data_races", data_races);
    Two ("unsequenced_races", unsequenced_races);
    One ("indeterminate_reads", indeterminate_reads);
    One ("separate_lo_bad_mutexes", separate_lo_bad_mutexes);
    One ("not_rel_acq_sc", not_rel_acq_sc)
 ]
<a name="dummy101">


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

let dummy101 = true 
<a name="rel_acq_sc_memory_model">

let rel_acq_sc_memory_model =
  <| consistent = rel_acq_sc_consistent_execution;
     relation_calculation = rel_acq_sc_relations;
(*     protocol = true_protocol;*)
     undefined = rel_acq_sc_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
    mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val rel_acq_sc_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy11">


(*********************************************** <a name="tot">*)
(* 11 - Memory_Model simplified for programs without consumes, relaxed, acquires or releases *)
(*********************************************** *)

let dummy11 = true 
<a name="tot_relations">

let tot_relations Xo Xw =
    let sw    = rel_acq_sc_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.tot in
    let hb    = no_consume_hb Xo.sb sw in
    [ ("hb", hb);
      ("sw", sw) ]
<a name="tot_consistent_total_order">


let tot_consistent_total_order (Xo,Xw,_) =
  strict_total_order_over Xo.actions Xw.tot &amp;&amp;
  (Xo.sb subset Xw.tot &amp;&amp;
  (Xo.asw subset Xw.tot))
<a name="tot_consistent_read_values">


(* NOTE: This predicate should be simplified. *)
let tot_consistent_read_values (Xo,Xw,_) =
  (&forall; (b &isin; Xo.actions).
    (is_read b)&rarr;
    ( let writes_at_same_location = { a | &forall; (a &isin; Xo.actions) | (loc_of a = loc_of b)&amp;&amp; is_write a} in
      if (&exist; (a &isin; Xo.actions).
        adjacent_less_than (set_restrict Xw.tot (writes_at_same_location &cup; {b})) Xo.actions a b)
      then (&exist; (a &isin; Xo.actions).
        ((a,b)&isin; Xw.rf)&amp;&amp;
        adjacent_less_than (set_restrict Xw.tot (writes_at_same_location &cup; {b})) Xo.actions a b)
      else not (&exist; (a &isin; Xo.actions). (a,b)&isin; Xw.rf) ) )
<a name="tot_consistent_locks">


let tot_consistent_locks (Xo,Xw,_) =
    (&forall; ((a,c) &isin; Xw.tot). 
      (is_successful_lock a &amp;&amp; (is_successful_lock c &amp;&amp; (loc_of a = loc_of c)))&rarr;
      (&exist; (b &isin; Xo.actions). (loc_of a = loc_of b)&amp;&amp; (is_unlock b &amp;&amp; ((a,b)&isin; Xw.tot &amp;&amp; ((b,c)&isin; Xw.tot)))))
<a name="tot_consistent_execution">


let tot_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("tot_consistent_locks", Leaf tot_consistent_locks);
         ("tot_consistent_total_order", Leaf tot_consistent_total_order);
         ("well_formed_rf", Leaf well_formed_rf);
         ("tot_consistent_read_values", Leaf tot_consistent_read_values) ]
<a name="dummy111">

(* NOTE: Could the definition of data race be made into the traditional total-order adjacency formulation and be shown to be equivalent? *)

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

let dummy111 = true 
<a name="tot_memory_model">

let tot_memory_model =
  <| consistent = tot_consistent_execution;
     relation_calculation = tot_relations;
(*     protocol = true_protocol;*)
     undefined = separate_lo_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = false;
           sc_flag  = false;
           lo_flag  = None;
           ao_flag  = false;
           tot_flag = true |>
  |>


val tot_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy13">


(*********************************************** *)
(* 13 - Memory_Model simplified, single thread, no atomics 2 *)
(*********************************************** *)

let dummy13 = true 
<a name="single_thread_relations">

let single_thread_relations Xo Xw =
    let hb    = Xo.sb in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse) ]
<a name="single_thread_consistent_execution">

let single_thread_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf) ]) ]
<a name="dummy131">


(*********************************************** *)
(*   - 13.1  - top level judgement *)
(*********************************************** *)

let dummy131 = true 
<a name="single_thread_undefined_behaviour">

let single_thread_undefined_behaviour =
  [ Two ("unsequenced_races", unsequenced_races);
    One ("indeterminate_reads", indeterminate_reads) ]

val single_thread_protocol : protocol_t 
<a name="single_thread_protocol">
let single_thread_protocol (Xo,_,_) =
  &exist; (t &isin; Xo.threads). Xo.threads = {t}&amp;&amp;
  (&forall; (a &isin; Xo.actions). is_NA_load a || is_NA_store a)
<a name="single_thread_memory_model">


let single_thread_memory_model =
  <| consistent = single_thread_consistent_execution;
     relation_calculation = single_thread_relations;
(*     protocol = single_thread_protocol;*)
     undefined = single_thread_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = false;
           sc_flag  = false;
           lo_flag  = None;
           ao_flag  = false;
           tot_flag = false |>
  |>


val single_thread_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy14">


(*********************************************** *)
(* 14 - Memory_Model simplified, multi-thread, no atomics, yes locks *)
(*********************************************** *)

let dummy14 = true 
<a name="locks_only_sw">

let locks_only_sw actions asw lo a b =
  (tid_of a <> tid_of b)&amp;&amp;
  ( (* thread sync *)
    (a,b)&isin; asw ||
    (* mutex sync *)
    (is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo)))
  )
<a name="locks_only_sw_set">

let locks_only_sw_set actions asw lo =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       locks_only_sw actions asw lo a b }
<a name="locks_only_hb">

let locks_only_hb Xo Xw =
    let sw = locks_only_sw_set Xo.actions Xo.asw Xw.lo in
    tc (Xo.sb &cup; sw)
<a name="locks_only_relations">


let locks_only_relations Xo Xw =
    let sw    = locks_only_sw_set Xo.actions Xo.asw Xw.lo in
    let hb    = no_consume_hb Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("sw", sw) ]
<a name="dummy14'">


(* let locks_only_consistent_lo_old (Xo,Xw,("hb",hb)::_) = *)
(*     let mutex_actions = *)
(*       { a | forall (a IN Xo.actions) | is_lock a || is_unlock a } in *)
(*     strict_partial_order mutex_actions Xw.lo && *)
(*     per_location_total mutex_actions Xw.lo && *)
(*     forall ((a,b) IN Xw.lo). *)
(*       a IN mutex_actions && b IN mutex_actions && *)
(*       (loc_of a = loc_of b) && *)
(*       not ((b,a) IN hb) *)

let dummy14' = true 
<a name="locks_only_consistent_lo">

let locks_only_consistent_lo (Xo,Xw,("hb",hb)::_) =
    trans Xo.actions Xw.lo &amp;&amp;
    (irrefl Xo.actions Xw.lo &amp;&amp;
    (&forall; (a &isin; Xo.actions) (b &isin; Xo.actions).
      ((a,b)&isin; Xw.lo)&rarr; (not ((b,a)&isin; hb)&amp;&amp;
      (((a,b)&isin; Xw.lo || ((b,a)&isin; Xw.lo))
      = ( (is_lock a || is_unlock a)&amp;&amp; ((is_lock b || is_unlock b)&amp;&amp;
          ((loc_of a = loc_of b)&amp;&amp;
          is_at_mutex_location Xo.lk a)) )))))
<a name="locks_only_consistent_locks">


let locks_only_consistent_locks (Xo,Xw,("hb",hb)::_) =
    (&forall; ((a,c) &isin; Xw.lo). 
      (is_successful_lock a &amp;&amp; is_successful_lock c)&rarr; 
      (&exist; (b &isin; Xo.actions). is_unlock b &amp;&amp; ((a,b)&isin; Xw.lo &amp;&amp; ((b,c)&isin; Xw.lo))))
<a name="locks_only_consistent_execution">


let locks_only_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("locks_only_consistent_locks", Leaf locks_only_consistent_locks);
         ("locks_only_consistent_lo", Leaf locks_only_consistent_lo);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf) ]) ]
<a name="dummy141">


(*********************************************** *)
(*   - 14.1  - lock only undefined behaviour *)
(*********************************************** *)

let dummy141 = true 
<a name="locks_only_good_mutex_use">

let locks_only_good_mutex_use actions lk sb lo a =
    (* violated requirement: The calling thread shall own the mutex. *)
    ( is_unlock a &rarr;
        ( &exist; (al &isin; actions).
            is_successful_lock al &amp;&amp; ((al,a)&isin; sb &amp;&amp;
            adjacent_less_than lo actions al a) ) )&amp;&amp;
    (* violated requirement: The calling thread does not own the mutex. *)
    ( is_lock a &rarr;
      not ( &exist; (al &isin; actions).
              is_successful_lock al &amp;&amp; ((al,a)&isin; sb &amp;&amp;
              adjacent_less_than lo actions al a) ) )
<a name="locks_only_bad_mutexes">


let locks_only_bad_mutexes (Xo,Xw,_) =
  { a | &forall; (a &isin; Xo.actions) |
    not (locks_only_good_mutex_use Xo.actions Xo.lk Xo.sb Xw.lo a)}
<a name="locks_only_undefined_behaviour">


let locks_only_undefined_behaviour =
  [ Two ("unsequenced_races", unsequenced_races);
    Two ("data_races", data_races);
    One ("indeterminate_reads", indeterminate_reads);
    One ("locks_only_bad_mutexes", locks_only_bad_mutexes) ]
<a name="dummy142">


(*********************************************** *)
(*   - 14.2  - top level judgement *)
(*********************************************** *)

let dummy142 = true

val locks_only_protocol : protocol_t 
<a name="locks_only_protocol">
let locks_only_protocol (Xo,_,_) =
  &forall; (a &isin; Xo.actions).
    is_NA_load a || (is_NA_store a || (is_lock a || is_unlock a))
<a name="locks_only_memory_model">


let locks_only_memory_model =
  <| consistent = locks_only_consistent_execution;
     relation_calculation = locks_only_relations;
(*     protocol = locks_only_protocol;*)
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = false;
           sc_flag  = false;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>

val locks_only_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy14a">


(*********************************************** *)
(* 14a - relaxed - memory_model simplified for programs without sc,
consumes, release or acquire *)
(*********************************************** *)

let dummy14a = true 
<a name="relaxed_only_consistent_execution">

let relaxed_only_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("locks_only_consistent_locks", Leaf locks_only_consistent_locks);
         ("locks_only_consistent_lo", Leaf locks_only_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf", Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity) ]) ]


val relaxed_only_protocol : protocol_t 
<a name="relaxed_only_protocol">
let relaxed_only_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> mo = Relaxed
      | Store _ _ mo _ _        -> mo = Relaxed
      | RMW _ _ mo _ _ _        -> mo = Relaxed
      | Fence _ _ _             -> false
      | Blocked_rmw _ _ _       -> true end 
<a name="dummy14a1">


(*********************************************** *)
(*   - 14a.1  - relaxed-only top level judgement *)
(*********************************************** *)

let dummy14a1 = true 
<a name="relaxed_only_memory_model">

let relaxed_only_memory_model =
  <| consistent = relaxed_only_consistent_execution;
     relation_calculation = locks_only_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = false;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val relaxed_only_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15">


(*********************************************** *)
(* 15 - release acquire - memory_model simplified for programs without sc,
consumes or relaxed *)
(*********************************************** *)

let dummy15 = true

val release_acquire_protocol : protocol_t 
<a name="release_acquire_protocol">
let release_acquire_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> (mo &isin; {NA;Acquire})
      | Store _ _ mo _ _        -> (mo &isin; {NA;Release})
      | RMW _ _ mo _ _ _        -> mo = Acq_rel
      | Fence _ _ _             -> false
      | Blocked_rmw _ _ _       -> true end 
<a name="release_acquire_synchronizes_with">


let release_acquire_synchronizes_with actions sb asw rf lo a b =
  (tid_of a <> tid_of b)&amp;&amp;
  ( (* thread sync *)
    (a,b)&isin; asw ||
    (* mutex sync *)
    ((is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo))) ||
    (* rel/acq sync *)
    ( is_release a &amp;&amp; (is_acquire b &amp;&amp; ((a,b)&isin; rf)) ))
  )
<a name="release_acquire_synchronizes_with_set">

let release_acquire_synchronizes_with_set actions sb asw rf lo =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       release_acquire_synchronizes_with actions sb asw rf lo a b}
<a name="release_acquire_relations">

let release_acquire_relations Xo Xw =
    let sw    = release_acquire_synchronizes_with_set
                  Xo.actions Xo.sb Xo.asw Xw.rf Xw.lo in
    let hb    = no_consume_hb Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("sw", sw) ]
<a name="dummy151">


(*********************************************** *)
(*   - 15.1  - release acquire top level judgement *)
(*********************************************** *)

let dummy151 = true 
<a name="release_acquire_memory_model">

let release_acquire_memory_model =
  <| consistent = relaxed_only_consistent_execution;
     relation_calculation = release_acquire_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = false;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val release_acquire_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15a">


(*********************************************** *)
(* 15a - release_acquire_relaxed - memory_model simplified for programs without sc,
consumes or relaxed *)
(*********************************************** *)

let dummy15a = true

val release_acquire_relaxed_protocol : protocol_t 
<a name="release_acquire_relaxed_protocol">
let release_acquire_relaxed_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> (mo &isin; {NA;Acquire;Relaxed})
      | Store _ _ mo _ _        -> (mo &isin; {NA;Release;Relaxed})
      | RMW _ _ mo _ _ _        -> (mo &isin; {Acq_rel;Acquire;Release;Relaxed})
      | Fence _ _ _             -> false
      | Blocked_rmw _ _ _       -> true end 
<a name="release_acquire_relaxed_synchronizes_with">


let release_acquire_relaxed_synchronizes_with actions sb asw rf lo rs a b =
  (tid_of a <> tid_of b)&amp;&amp;
  ( (* thread sync *)
    (a,b)&isin; asw ||
    (* mutex sync *)
    ((is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo))) ||
    (* rel/acq sync *)
    ( is_release a &amp;&amp; (is_acquire b &amp;&amp;
      (&exist; (c &isin; actions). (a,c)&isin; rs &amp;&amp; ((c,b)&isin; rf))) ))
  )
<a name="release_acquire_relaxed_synchronizes_with_set">

let release_acquire_relaxed_synchronizes_with_set actions sb asw rf lo rs =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       release_acquire_relaxed_synchronizes_with actions sb asw rf lo rs a b}
<a name="release_acquire_relaxed_relations">

let release_acquire_relaxed_relations Xo Xw =
    let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = release_acquire_relaxed_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.lo rs in
    let hb    = no_consume_hb Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("sw", sw);
      ("rs", rs) ]
<a name="dummy15a1">


(*********************************************** *)
(*   - 15a.1  - release acquire relaxed top level judgement *)
(*********************************************** *)

let dummy15a1 = true 
<a name="release_acquire_relaxed_memory_model">

let release_acquire_relaxed_memory_model =
  <| consistent = relaxed_only_consistent_execution;
     relation_calculation = release_acquire_relaxed_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = false;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val release_acquire_relaxed_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15b">


(*********************************************** *)
(* 15b - release_acquire_fenced *)
(*********************************************** *)

let dummy15b = true

val release_acquire_fenced_protocol : protocol_t 
<a name="release_acquire_fenced_protocol">
let release_acquire_fenced_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> (mo &isin; {NA;Acquire;Relaxed})
      | Store _ _ mo _ _        -> (mo &isin; {NA;Release;Relaxed})
      | RMW _ _ mo _ _ _        -> (mo &isin; {Acq_rel;Acquire;Release;Relaxed})
      | Fence _ _ mo            -> (mo &isin; {NA;Acquire;Relaxed})
      | Blocked_rmw _ _ _       -> true end 
<a name="release_acquire_fenced_synchronizes_with">


let release_acquire_fenced_synchronizes_with actions sb asw rf lo rs hrs a b =
  (tid_of a <> tid_of b)&amp;&amp;
  ( (* thread sync *)
    (a,b)&isin; asw ||
    (* mutex sync *)
    ((is_unlock a &amp;&amp; (is_successful_lock b &amp;&amp; ((a,b)&isin; lo))) ||
    (* rel/acq sync *)
    (( is_release a &amp;&amp; (is_acquire b &amp;&amp;
      (&exist; (c &isin; actions). (a,c)&isin; rs &amp;&amp; ((c,b)&isin; rf))) ) ||
    (* fence synchronisation *)
    (( is_fence a &amp;&amp; (is_release a &amp;&amp; (is_fence b &amp;&amp; (is_acquire b &amp;&amp;
      (&exist; (x &isin; actions) (y &isin; actions) (z &isin; actions).
        (a,x)&isin; sb &amp;&amp; ((x,y)&isin; hrs &amp;&amp; ((y,z)&isin; rf &amp;&amp; ((y,b)&isin; sb)))))))) ||
    (( is_fence a &amp;&amp; (is_release a &amp;&amp; (is_acquire b &amp;&amp;
      (&exist; (x &isin; actions) (y &isin; actions).
          (a,x)&isin; sb &amp;&amp; ((x,y)&isin; hrs &amp;&amp; ((y,b)&isin; rf))))) ) ||
    ( is_release a &amp;&amp; (is_fence b &amp;&amp; (is_acquire b &amp;&amp;
      (&exist; (x &isin; actions) (y &isin; actions).
        (a,x)&isin; rs &amp;&amp; ((x,y)&isin; rf &amp;&amp; ((y,b)&isin; sb)))))))))) )
<a name="release_acquire_fenced_synchronizes_with_set">


let release_acquire_fenced_synchronizes_with_set actions sb asw rf lo rs hrs =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       release_acquire_fenced_synchronizes_with actions sb asw rf lo rs hrs a b}
<a name="release_acquire_fenced_relations">

let release_acquire_fenced_relations Xo Xw =
    let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
    let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = release_acquire_fenced_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.lo rs hrs in
    let hb    = no_consume_hb Xo.sb sw in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("sw", sw);
      ("rs", rs);
      ("hrs", hrs) ]
<a name="dummy15b1">


(*********************************************** *)
(*   - 15b.1  - release acquire fenced top level judgement *)
(*********************************************** *)

let dummy15b1 = true 
<a name="release_acquire_fenced_memory_model">

let release_acquire_fenced_memory_model =
  <| consistent = relaxed_only_consistent_execution;
     relation_calculation = release_acquire_fenced_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = false;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val release_acquire_fenced_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15c">


(*********************************************** *)
(* 15c - sc, no sc fences *)
(*********************************************** *)

let dummy15c = true

val sc_accesses_protocol : protocol_t 
<a name="sc_accesses_protocol">
let sc_accesses_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> (mo &isin; {NA;Acquire;Relaxed;Seq_cst})
      | Store _ _ mo _ _        -> (mo &isin; {NA;Release;Relaxed;Seq_cst})
      | RMW _ _ mo _ _ _        -> (mo &isin; {Acq_rel;Acquire;Release;Relaxed;Seq_cst})
      | Fence _ _ mo            -> (mo &isin; {NA;Acquire;Relaxed})
      | Blocked_rmw _ _ _       -> true end 
<a name="sc_accesses_consistent_sc">


let sc_accesses_consistent_sc (Xo,Xw,("hb",hb)::_) =
    trans Xo.actions Xw.sc &amp;&amp;
    (irrefl Xo.actions Xw.sc &amp;&amp;
    (&forall; (a &isin; Xo.actions) (b &isin; Xo.actions).
      ((a,b)&isin; Xw.sc)&rarr; (not ((b,a)&isin; hb &cup; Xw.mo)&amp;&amp;
      (((a,b)&isin; Xw.sc || ((b,a)&isin; Xw.sc)) = (is_seq_cst a &amp;&amp; is_seq_cst b)))))
<a name="dummy15c'">

(* let sc_accesses_consistent_sc_old (Xo,Xw,("hb",hb)::_) = *)
(*     trans Xo.actions Xw.sc && *)
(*     irrefl Xo.actions Xw.sc && *)
(*     forall (a IN Xo.actions) (b IN Xo.actions). *)
(*       (is_seq_cst a && is_seq_cst b) = ((a,b) IN Xw.sc || (b,a) IN Xw.sc) && *)
(*       (a,b) IN Xw.sc --> (not ((b,a) IN hb) && not ((b,a) IN Xw.mo)) *)

let dummy15c' = true 
<a name="sc_accesses_sc_reads_restricted">

let sc_accesses_sc_reads_restricted (Xo,Xw,("hb",hb)::_) =
    &forall; ((w,r) &isin; Xw.rf). is_seq_cst r &rarr;
      (( is_seq_cst w &amp;&amp; ((w,r)&isin; Xw.sc &amp;&amp;
        not (&exist; (w' &isin; Xo.actions).
          is_write w' &amp;&amp; ((loc_of w = loc_of w')&amp;&amp;
          ((w,w')&isin; Xw.sc &amp;&amp; ((w',r)&isin; Xw.sc))) )) ) ||
      ( not (is_seq_cst w)&amp;&amp;
        not (&exist; (w' &isin; Xo.actions).
          is_write w' &amp;&amp; ((loc_of w = loc_of w')&amp;&amp;
          ((w,w')&isin; hb &amp;&amp; ((w',r)&isin; Xw.sc))) ) ))
<a name="sc_accesses_consistent_execution">


let sc_accesses_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("locks_only_consistent_locks", Leaf locks_only_consistent_locks);
         ("locks_only_consistent_lo", Leaf locks_only_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("sc_accesses_consistent_sc", Leaf sc_accesses_consistent_sc);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf", Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_accesses_sc_reads_restricted", Leaf sc_accesses_sc_reads_restricted) ]) ]
<a name="dummy15c1">


(*********************************************** *)
(*   - 15c.1  - sc, no sc fences top level judgement *)
(*********************************************** *)

let dummy15c1 = true 
<a name="sc_accesses_memory_model">

let sc_accesses_memory_model =
  <| consistent = sc_accesses_consistent_execution;
     relation_calculation = release_acquire_fenced_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val sc_accesses_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15d">


(*********************************************** *)
(* 15d - sc_fences, no consume *)
(*********************************************** *)

let dummy15d = true

val sc_fenced_protocol : protocol_t 
<a name="sc_fenced_protocol">
let sc_fenced_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> (mo &isin; {NA;Acquire;Relaxed;Seq_cst})
      | Store _ _ mo _ _        -> (mo &isin; {NA;Release;Relaxed;Seq_cst})
      | RMW _ _ mo _ _ _        -> (mo &isin; {Acq_rel;Acquire;Release;Relaxed;Seq_cst})
      | Fence _ _ mo            -> (mo &isin; {NA;Acquire;Relaxed;Seq_cst})
      | Blocked_rmw _ _ _       -> true end 
<a name="sc_fenced_sc_fences_heeded">


let sc_fenced_sc_fences_heeded (Xo,Xw,("hb",hb)::_) =
    &forall; (f &isin; Xo.actions) (f' &isin; Xo.actions) 
           (r &isin; Xo.actions)
           (w &isin; Xo.actions) (w' &isin; Xo.actions).
      not ( is_fence f &amp;&amp; (is_fence f' &amp;&amp;
            ( (* fence restriction N3291 29.3p4 *)
              ( (w,w')&isin; Xw.mo &amp;&amp;
                ((w',f)&isin; Xw.sc &amp;&amp;
                ((f,r)&isin; Xo.sb &amp;&amp;
                ((w,r)&isin; Xw.rf))) ) ||
              (* fence restriction N3291 29.3p5 *)
              (( (w,w')&isin; Xw.mo &amp;&amp;
                ((w',f)&isin; Xo.sb &amp;&amp;
                ((f,r)&isin; Xw.sc &amp;&amp;
                ((w,r)&isin; Xw.rf))) ) ||
              (* fence restriction N3291 29.3p6 *)
              (( (w,w')&isin; Xw.mo &amp;&amp;
                ((w',f)&isin; Xo.sb &amp;&amp;
                ((f,f')&isin; Xw.sc &amp;&amp;
                ((f',r)&isin; Xo.sb &amp;&amp;
                ((w,r)&isin; Xw.rf)))) ) ||
              (* SC fences impose mo N3291 29.3p7 *)
              (( (w',f)&isin; Xo.sb &amp;&amp;
                ((f,f')&isin; Xw.sc &amp;&amp;
                ((f',w)&isin; Xo.sb &amp;&amp;
                ((w,w')&isin; Xw.mo))) ) ||
              (* N3291 29.3p7, w collapsed first write*)
              (( (w',f)&isin; Xw.sc &amp;&amp;
                ((f,w)&isin; Xo.sb &amp;&amp;
                ((w,w')&isin; Xw.mo)) ) ||
              (* N3291 29.3p7, w collapsed second write*)
              ( (w',f)&isin; Xo.sb &amp;&amp;
                ((f,w)&isin; Xw.sc &amp;&amp;
                ((w,w')&isin; Xw.mo)) ))))) )) )
<a name="sc_fenced_consistent_execution">


let sc_fenced_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("locks_only_consistent_locks", Leaf locks_only_consistent_locks);
         ("locks_only_consistent_lo", Leaf locks_only_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("sc_accesses_consistent_sc", Leaf sc_accesses_consistent_sc);
         ("sc_fenced_sc_fences_heeded", Leaf sc_fenced_sc_fences_heeded);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf", Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_accesses_sc_reads_restricted", Leaf sc_accesses_sc_reads_restricted) ]) ]
<a name="dummy15d1">


(*********************************************** *)
(*   - 15d.1  - sc, no sc fences top level judgement *)
(*********************************************** *)

let dummy15d1 = true 
<a name="sc_fenced_memory_model">

let sc_fenced_memory_model =
  <| consistent = sc_fenced_consistent_execution;
     relation_calculation = release_acquire_fenced_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val sc_fenced_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15e">


(*********************************************** *)
(* 15e - with consume *)
(*********************************************** *)

let dummy15e = true

val with_consume_protocol : protocol_t 
<a name="with_consume_protocol">
let with_consume_protocol (Xo,_,_) =
    &forall; (a &isin; Xo.actions).
      match a with
      | Lock _ _ _ _            -> true
      | Unlock _ _ _            -> true
      | Load _ _ mo _ _         -> (mo &isin; {NA;Acquire;Relaxed;Seq_cst;Consume})
      | Store _ _ mo _ _        -> (mo &isin; {NA;Release;Relaxed;Seq_cst})
      | RMW _ _ mo _ _ _        -> (mo &isin; {Acq_rel;Acquire;Release;Relaxed;Seq_cst})
      | Fence _ _ mo            -> (mo &isin; {NA;Acquire;Relaxed;Seq_cst})
      | Blocked_rmw _ _ _       -> true end 
<a name="with_consume_cad_set">

let with_consume_cad_set actions sb dd rf = tc ( (rf ^cap; sb)&cup; dd )
<a name="with_consume_dob">

let with_consume_dob actions rf rs cad w a =
    &exist; (w' &isin; actions) (r &isin; actions).
      is_consume r &amp;&amp;
      ((w,w')&isin; rs &amp;&amp; ((w',r)&isin; rf &amp;&amp;
      ( (r,a)&isin; cad || (r = a) )))
<a name="with_consume_dob_set">

let with_consume_dob_set actions rf rs cad =
    { (a,b) | &forall; (a &isin; actions) (b &isin; actions) |
       dependency_ordered_before actions rf rs cad a b}
<a name="with_consume_ithb">

let with_consume_ithb actions sb sw dob =
    let r = sw &cup; dob &cup; (compose sw sb) in
      tc (r &cup; (compose sb r))
<a name="with_consume_consistent_ithb">

let with_consume_consistent_ithb
      (Xo,Xw,_::_::("ithb",ithb)::_) =
    irrefl Xo.actions ithb 
<a name="with_consume_hb">

let with_consume_hb actions sb ithb =
    sb &cup; ithb 
<a name="with_consume_relations">

let with_consume_relations Xo Xw =
    let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
    let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = release_acquire_fenced_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.lo rs hrs in
    let cad   = with_consume_cad_set Xo.actions Xo.sb Xo.dd Xw.rf in
    let dob   = with_consume_dob_set Xo.actions Xw.rf rs cad in
    let ithb  = with_consume_ithb Xo.actions Xo.sb sw dob in
    let hb    = with_consume_hb Xo.actions Xo.sb ithb in
    let vse   = visible_side_effect_set Xo.actions hb in
    [ ("hb", hb);
      ("vse", vse);
      ("ithb", ithb);
      ("sw", sw);
      ("rs", rs);
      ("hrs", hrs);
      ("dob", dob);
      ("cad", cad) ]
<a name="with_consume_consistent_execution">


let with_consume_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("locks_only_consistent_locks", Leaf locks_only_consistent_locks);
         ("locks_only_consistent_lo", Leaf locks_only_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("sc_accesses_consistent_sc", Leaf sc_accesses_consistent_sc);
         ("sc_fenced_sc_fences_heeded", Leaf sc_fenced_sc_fences_heeded);
         ("consistent_ithb", Leaf consistent_ithb);
         ("consistent_rf",
           Node [ ("det_read", Leaf det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
                  ("consistent_atomic_rf", Leaf consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_accesses_sc_reads_restricted", Leaf sc_accesses_sc_reads_restricted) ]) ]
<a name="dummy15e1">


(*********************************************** *)
(*   - 15e.1  - with consume top level judgement *)
(*********************************************** *)

let dummy15e1 = true 
<a name="with_consume_memory_model">

let with_consume_memory_model =
  <| consistent = with_consume_consistent_execution;
     relation_calculation = with_consume_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Per_location_order;
           ao_flag  = false;
           tot_flag = false |>
  |>


val with_consume_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy15f">


(*********************************************** *)
(* 15f - the standard model *)
(*********************************************** *)

let dummy15f = true 
<a name="standard_vsses_non_max">


let standard_vsses_non_max actions lk mo hb vse =
  { (v,r) | 
    &forall; (r &isin; actions)
           (v &isin; actions)
           (head &isin; actions) |
    is_at_atomic_location lk r &amp;&amp; ((head,r)&isin; vse &amp;&amp;
    ( v = head ||
      ( (head,v)&isin; mo &amp;&amp; (not ((r,v)&isin; hb)&amp;&amp;
        (&forall; (w &isin; actions).
          ((head,w)&isin; mo &amp;&amp; ((w,v)&isin; mo))&rarr; not ((r,w)&isin; hb)))
      )
    ))
  }
<a name="standard_vsses">


let standard_vsses actions lk mo hb vse =
  { (v,r) | 
    &forall; (r &isin; actions)
           (v &isin; actions)
           (head &isin; actions) |
    is_at_atomic_location lk r &amp;&amp;
    ((head,r)&isin; vse &amp;&amp;
    (not (&exist; (v' &isin; actions). (v',r)&isin; vse &amp;&amp; ((head,v')&isin; mo))&amp;&amp;
    ( v = head ||
      ( (head,v)&isin; mo &amp;&amp; (not ((r,v)&isin; hb)&amp;&amp;
        (&forall; (w &isin; actions).
          ((head,w)&isin; mo &amp;&amp; ((w,v)&isin; mo))&rarr; not ((r,w)&isin; hb)))
      )
    )))
  }
<a name="standard_relations">


let standard_relations Xo Xw =
    let hrs   = hypothetical_release_sequence_set Xo.actions Xo.lk Xw.mo in
    let rs    = release_sequence_set Xo.actions Xo.lk Xw.mo in
    let sw    = release_acquire_fenced_synchronizes_with_set Xo.actions Xo.sb Xo.asw Xw.rf Xw.lo rs hrs in
    let cad   = with_consume_cad_set Xo.actions Xo.sb Xo.dd Xw.rf in
    let dob   = with_consume_dob_set Xo.actions Xw.rf rs cad in
    let ithb  = with_consume_ithb Xo.actions Xo.sb sw dob in
    let hb    = with_consume_hb Xo.actions Xo.sb ithb in
    let vse   = visible_side_effect_set Xo.actions hb in
    let vsses = standard_vsses Xo.actions Xo.lk Xw.mo hb vse in
    [ ("hb", hb);
      ("vse", vse);
      ("ithb", ithb);
      ("vsses", vsses);
      ("sw", sw);
      ("rs", rs);
      ("hrs", hrs);
      ("dob", dob);
      ("cad", cad) ]
<a name="standard_consistent_atomic_rf">


let standard_consistent_atomic_rf (Xo,Xw,_::_::_::("vsses",vsses)::_) =
    &forall; ((w,r) &isin; Xw.rf). is_at_atomic_location Xo.lk r &rarr;
        ((w,r)&isin; vsses)
<a name="standard_det_read">

let standard_det_read (Xo,Xw,("hb",hb)::("vse",vse)::_) =
    &forall; (r &isin; Xo.actions).
      is_read r &rarr;
      ((&exist; (w &isin; Xo.actions).  (w,r)&isin; vse) =
      (&exist; (w' &isin; Xo.actions). (w',r)&isin; Xw.rf))
<a name="standard_consistent_execution">


(* let standard_consistent_locks (Xo,Xw,("hb",hb)::_) = *)
(*     (forall ((a,c) IN Xw.lo).  *)
(*       is_successful_lock a && is_successful_lock c && (loc_of a = loc_of c) *)
(*       -->  *)
(*       (exists (b IN Xo.actions). (loc_of a = loc_of b) && is_unlock b && (a,b) IN Xw.lo && (b,c) IN Xw.lo)) *)


(* let standard_consistent_lo (Xo,Xw,("hb",hb)::_) = *)
(*     let mutex_actions = *)
(*       { a | forall (a IN Xo.actions) | is_lock a || is_unlock a } in *)
(*     strict_partial_order mutex_actions Xw.lo && *)
(*     total mutex_actions Xw.lo && *)
(*     forall ((a,b) IN Xw.lo). *)
(*       a IN mutex_actions && b IN mutex_actions && *)
(*       not ((b,a) IN hb) *)


let standard_consistent_execution =
  Node [ ("well_formed_threads", Leaf well_formed_threads);
         ("well_formed_rf", Leaf well_formed_rf);
         ("locks_only_consistent_locks", Leaf locks_only_consistent_locks);
         ("locks_only_consistent_lo", Leaf locks_only_consistent_lo);
         ("consistent_mo", Leaf consistent_mo);
         ("sc_accesses_consistent_sc", Leaf sc_accesses_consistent_sc);
         ("sc_fenced_sc_fences_heeded", Leaf sc_fenced_sc_fences_heeded);
         ("consistent_ithb", Leaf consistent_ithb);
         ("consistent_rf",
           Node [ ("standard_det_read", Leaf standard_det_read);
                  ("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
                  ("standard_consistent_atomic_rf",
                     Leaf standard_consistent_atomic_rf);
                  ("coherent_memory_use", Leaf coherent_memory_use);
                  ("rmw_atomicity", Leaf rmw_atomicity);
                  ("sc_accesses_sc_reads_restricted",
                     Leaf sc_accesses_sc_reads_restricted) ]) ]
<a name="dummy15f1">

         (* ("consistent_sc", Leaf consistent_sc); *)


(* let standard_good_mutex_use actions lk sb lo a = *)
(*     let lo_at_loc_of_a = { (x,y) | forall ((x,y) IN lo) | *)
(*                         (loc_of x = loc_of a) && (loc_of y = loc_of a) } in *)
(*         (* violated requirement: The calling thread shall own the mutex. *) *)
(*     ( is_unlock a --> *)
(*         ( exists (al IN actions). *)
(*             is_successful_lock al && (al,a) IN sb && *)
(*             adjacent_less_than lo_at_loc_of_a actions al a ) ) && *)
(*     (* violated requirement: The calling thread does not own the mutex. *) *)
(*     ( is_lock a --> *)
(*       not ( exists (al IN actions). *)
(*               is_successful_lock al && (al,a) IN sb && *)
(*               adjacent_less_than lo_at_loc_of_a actions al a ) ) *)

(* let standard_bad_mutexes (Xo,Xw,_) = *)
(*   { a | forall (a IN Xo.actions) | *)
(*     not (standard_good_mutex_use Xo.actions Xo.lk Xo.sb Xw.lo a)} *)

(* let standard_undefined_behaviour = *)
(*   [ Two ("unsequenced_races", unsequenced_races); *)
(*     Two ("data_races", data_races); *)
(*     One ("indeterminate_reads", indeterminate_reads); *)
(*     One ("standard_bad_mutexes", standard_bad_mutexes) ] *)

(*********************************************** *)
(*   - 15f.1  - single lock order top level judgement *)
(*********************************************** *)

let dummy15f1 = true 
<a name="standard_memory_model">

let standard_memory_model =
  <| consistent = standard_consistent_execution;
     relation_calculation = standard_relations;
     undefined = locks_only_undefined_behaviour;
     relation_flags =
       <|  rf_flag  = true;
           mo_flag  = true;
           sc_flag  = true;
           lo_flag  = Some Global_order;
           ao_flag  = false;
           tot_flag = false |>
  |>

val standard_behaviour : opsem_t -> program -> program_behaviours 
<a name="dummy16">


(***********************)
(* - 16 - Meta theorem *)
(***********************)

let dummy16 = true

(*
val thm1 : bool
let {hol; isabelle; coq; tex} thm1 = forall opsem p.
  locks_only_protocol  -->
  (locks_only_behaviour opsem p = release_acquire_behaviour opsem p)  
*)

</pre>
  </body>
</html>