C/C++ memory model definitions
(*========================================================================*)
(* *)
(* 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-*- *)
(*
Log:
20/03/13 - a savage and hasty tidy, following r10282
--- 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.1 - Well formed action
- 3.2 - Well formed threads
4 - Memory_Model simplified, single thread, no atomics
5 - Memory_Model simplified, multi-thread, no atomics, yes locks
6 - relaxed - memory_model simplified for programs without sc,
consumes, release or acquire
7 - release acquire - memory_model simplified for programs without sc,
consumes or relaxed
8 - release_acquire_relaxed - memory_model simplified for programs without sc,
consumes or relaxed
9 - release_acquire_fenced
10 - sc, no sc fences
11 - sc_fences, no consume
12 - with consume
13 - the standard model
14 - Meta-theory
15 - release acquire, no locks - memory_model simplified for programs without sc,
consumes, relaxed or locks
*)
(*************************************************** *)
(* 1 - Relational definitions *)
(*************************************************** *)
let irrefl ord = ∀ ((x,y) ∈ ord). not (x = y)
let trans ord = ∀ ((w,x) ∈ ord) ((y,z) ∈ ord). (x = y)→ ((w,z)∈ ord)
(* Set.cross s t exists for hol and isabelle*)
let cross S T = { (s,t) | ∀ (s ∈ S) (t ∈ T) | true}
(* indreln {isabelle} *)
(* forall r x y. r (x, y) ==> tc' r (x, y) and *)
(* forall r x y. (exist z. tc' r (x,z) && tc' r (z,y)) ==> tc' r (x,y) *)
(* let {isabelle} tc r = *)
(* let r' = fun (x,y) -> ((x,y) IN r) in *)
(* { (x,y) | forall ((x,y) IN r) | tc' r' (x,y) } *)
val tc : ∀ 'a. set ('a * 'a) -> set ('a * 'a)
let set_restrict rel s = (rel)^cap; (cross s s)
let strict_partial_order ord = irrefl ord && trans ord
let relation_over s rel = ∀ ((a,b) ∈ rel). a ∈ s && (b ∈ s)
let inj_on f A =
(∀ (x ∈ A). (∀ (y ∈ A). (f x = f y)→ (x = y)))
let total s ord =
(∀ (x ∈ s) (y ∈ s). (x,y)∈ ord || ((y,x)∈ ord || (x = y)))
let strict_total_order_over s ord =
relation_over s ord &&
(
strict_partial_order ord &&
total s ord)
let adjacent_less_than ord s x y =
(x,y)∈ ord && not (∃ (z ∈ s). (x,z)∈ ord && ((z,y)∈ ord))
let adjacent_less_than_such_that pred ord s x y =
pred x && ((x,y)∈ ord && not (∃ (z ∈ s). pred z && ((x,z)∈ ord && ((z,y)∈ ord))))
val finite : ∀ 'a. set 'a -> bool
val finite_prefixes : ∀ 'a. set ('a * 'a) -> set 'a -> bool
(*************************************************** *)
(* 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
(*********************************************** *)
(* - 2.2 - Execution records *)
(*********************************************** *)
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) ;
|>
type order_kind =
Global_order
| Per_location_order
type relation_usage_flags =
<| rf_flag : bool;
mo_flag : bool;
sc_flag : bool;
lo_flag : bool;
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 observable_execution = (pre_execution * execution_witness)
type program_behaviours =
Defined of set observable_execution
| Undefined
type rf_observable_execution = (pre_execution * set (action * action))
type rf_program_behaviours =
rf_Defined of set rf_observable_execution
| rf_Undefined
type named_predicate_tree =
Leaf of (complete_execution -> bool)
| Node of list (string * named_predicate_tree)
val named_predicate_tree_measure : named_predicate_tree -> num
let rec apply_tree pred_tree X =
match pred_tree with
| Leaf p -> p X
| Node l -> List.for_all (fun (name, branch) -> apply_tree branch X) l
end
type fault_setgen =
One of (string * (complete_execution -> set action))
| Two of (string * (complete_execution -> set (action * action)))
let is_fault faults_list (Xo,Xw,rl) a =
let is_particular_fault f =
match f with
One (_name,setgen) -> (a ∈ (setgen (Xo,Xw,rl)))
| Two (_name,setgen) ->
∃ (b ∈ Xo.actions).
((a,b)∈ (setgen (Xo,Xw,rl))) || ((b,a)∈ (setgen (Xo,Xw,rl))) end in
List.exist is_particular_fault faults_list
let each_empty faults_list X =
let faults_empty f =
match f with
One (_name,setgen) -> Set.is_empty (setgen X)
| Two (_name,setgen) -> Set.is_empty (setgen X) end in
List.for_all faults_empty faults_list
type opsem_t = program -> pre_execution -> bool
type protocol_t = complete_execution -> bool
let true_protocol _ = true
val statically_satisfied : protocol_t -> opsem_t -> program -> bool
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 observable_filter : set complete_execution -> set observable_execution
val behaviour : memory_model -> protocol_t -> opsem_t -> program -> program_behaviours
val rf_observable_filter : set complete_execution -> set rf_observable_execution
val rf_behaviour : memory_model -> protocol_t -> opsem_t -> program -> rf_program_behaviours
(*
val behaviour : memory_model -> memory_model -> protocol_t -> opsem_t -> program -> program_behaviours
let rf_equivalent M M' =
*)
(*************************************************** *)
(* - 2.3 - Projection functions *)
(*************************************************** *)
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
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
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
let value_read_by a =
match a with
Load _ _ _ _ v -> Some v
| RMW _ _ _ _ v _ -> Some v
| _ -> None
end
let value_written_by a =
match a with
Store _ _ _ _ v -> Some v
| RMW _ _ _ _ _ v -> Some v
| _ -> None
end
let is_lock a =
match a with
Lock _ _ _ _ -> true
| _ -> false
end
let is_successful_lock a =
match a with
Lock _ _ _ Locked -> true
| _ -> false
end
let is_blocked_lock a =
match a with
Lock _ _ _ Blocked -> true
| _ -> false
end
let is_unlock a =
match a with
Unlock _ _ _ -> true
| _ -> false
end
let is_atomic_load a =
match a with
Load _ _ mo _ _ -> mo <> NA
| _ -> false
end
let is_atomic_store a =
match a with
Store _ _ mo _ _ -> mo <> NA
| _ -> false
end
let is_RMW a =
match a with
RMW _ _ _ _ _ _ -> true
| _ -> false
end
let is_blocked_rmw a =
match a with
Blocked_rmw _ _ _ -> true
| _ -> false
end
let is_NA_load a =
match a with
Load _ _ mo _ _ -> mo = NA
| _ -> false
end
let is_NA_store a =
match a with
Store _ _ mo _ _ -> mo = NA
| _ -> false
end
let is_load a =
match a with
Load _ _ _ _ _ -> true
| _ -> false
end
let is_store a =
match a with
Store _ _ _ _ _ -> true
| _ -> false
end
let is_fence a =
match a with
Fence _ _ _ -> true
| _ -> false
end
let is_atomic_action a =
match a with
Load _ _ mo _ _ -> mo <> NA
| Store _ _ mo _ _ -> mo <> NA
| RMW _ _ _ _ _ _ -> true
| _ -> false
end
let is_read a =
match a with
Load _ _ _ _ _ -> true
| RMW _ _ _ _ _ _ -> true
| _ -> false
end
let is_write a =
match a with
Store _ _ _ _ _ -> true
| RMW _ _ _ _ _ _ -> true
| _ -> false
end
(* It is important to note that seq_cst atomics are both acquires and releases *)
let is_acquire a =
match a with
Load _ _ mo _ _ -> mo ∈ {Acquire;Seq_cst}
| RMW _ _ mo _ _ _ -> mo ∈ {Acquire;Acq_rel;Seq_cst}
| Fence _ _ mo -> mo ∈ {Acquire;Consume;Acq_rel;Seq_cst}
| _ -> false
end
let is_release a =
match a with
Store _ _ mo _ _ -> mo ∈ {Release;Seq_cst}
| RMW _ _ mo _ _ _ -> mo ∈ {Release;Acq_rel;Seq_cst}
| Fence _ _ mo -> mo ∈ {Release;Acq_rel;Seq_cst}
| _ -> false
end
let is_consume a =
match a with
Load _ _ mo _ _ -> mo = Consume
| _ -> false
end
let is_seq_cst a =
match a with
Load _ _ mo _ _ -> mo = Seq_cst
| Store _ _ mo _ _ -> mo = Seq_cst
| RMW _ _ mo _ _ _ -> mo = Seq_cst
| Fence _ _ mo -> mo = Seq_cst
| _ -> false
end
let threadwise s rel = ∀ ((a,b) ∈ rel). tid_of a = tid_of b
let locationwise s rel = ∀ ((a,b) ∈ rel). loc_of a = loc_of b
let per_location_total s rel =
∀ (a ∈ s) (b ∈ s). ( loc_of a = loc_of b)→
((a,b)∈ rel || ((b,a)∈ rel || (a = b)))
(**************************************** *)
(* - 2.4 - Location kinds *)
(**************************************** *)
let actions_respect_location_kinds actions lk =
∀ (a ∈ actions). match a with
| Lock _ _ l _ -> lk l = Mutex
| Unlock _ _ l -> lk l = Mutex
| Load _ _ mo l _ ->
(mo = NA && (lk l = Non_Atomic)) || (mo <> NA && (lk l = Atomic))
| Store _ _ mo l _ ->
(mo = NA && (lk l = Non_Atomic)) || (lk l = Atomic)
| RMW _ _ _ l _ _ -> lk l = Atomic
| Fence _ _ _ -> true
| Blocked_rmw _ _ l -> lk l = Atomic
end
let is_at_mutex_location lk a =
match loc_of a with
Some l -> (lk l = Mutex)
| None -> false
end
let is_at_non_atomic_location lk a =
match loc_of a with
Some l -> (lk l = Non_Atomic)
| None -> false
end
let is_at_atomic_location lk a =
match loc_of a with
Some l -> (lk l = Atomic)
| None -> false
end
(**************************************** *)
(* - 3.1 - Well formed action *)
(**************************************** *)
(* used in cppmem *)
let locations_of actions =
{ l | ∀ (Some l ∈ { (loc_of a) | ∀ (a ∈ actions) | true }) | true}
let well_formed_action a =
match a with
| Load _ _ mo _ _ -> mo ∈ {NA;Relaxed;Acquire;Seq_cst;Consume}
| Store _ _ mo _ _ -> mo ∈ {NA;Relaxed;Release;Seq_cst}
| RMW _ _ mo _ _ _ -> mo ∈ {Relaxed;Release;Acquire;Acq_rel;Seq_cst}
| Fence _ _ mo -> mo ∈ {Relaxed;Release;Acquire;Acq_rel;Consume;Seq_cst}
| _ -> true
end
(*********************************************** *)
(* - 3.2 - Well formed threads *)
(*********************************************** *)
let assumptions (Xo,Xw,_) =
finite_prefixes Xo.sb Xo.actions &&
(
finite_prefixes Xo.asw Xo.actions &&
(
finite_prefixes Xw.rf Xo.actions &&
(
finite_prefixes Xw.mo Xo.actions &&
(
finite_prefixes Xw.sc Xo.actions &&
(
finite_prefixes Xw.lo Xo.actions &&
(
relation_over Xo.actions Xo.asw &&
(∀ ((a,b) ∈ Xo.asw). tid_of a <> tid_of b)))))))
(* finite_prefixes (tc (Xo.sb union Xo.asw)) Xo.actions && *)
(* irrefl (tc (Xo.sb union Xo.asw)) &&*)
(*finite {Xo.threads} &&*)
(* forall (b IN Xo.actions).
finite { a | forall (a IN Xo.actions) |
(tid_of a = tid_of b) && not ((a,b) IN Xo.sb || (b,a) IN Xo.sb) }
*)
(*
Finite prefixes thoughts.
I need to union and then tc two relations. The first is tc (sb U asw). I know that has finite prefixes, and is acyclic. First consider adding in lock order
( hb SUBSET (tc(sb union asw union lo)) /\
finite_prefixes Xo.actions tc(sb union asw) /\
trans Xw.lo /\
irrefl Xw.lo /\
forall (a IN Xo.actions) (b IN Xo.actions).
(a,b) IN Xw.lo --> not ((b,a) IN hb)
) ==>
*)
let blocking_observed actions sb =
(∀ (a ∈ actions).
(is_blocked_rmw a || is_blocked_lock a)→
not (∃ (b ∈ actions). (a,b)∈ sb))
(* Indeterminate sequencing from 1.9p15, noting that all atomic and
lock calls are functions. *)
let indeterminate_sequencing Xo =
∀ (a ∈ Xo.actions) (b ∈ Xo.actions).
((tid_of a = tid_of b)&& ((a <> b)&&
not (is_at_non_atomic_location Xo.lk a && is_at_non_atomic_location Xo.lk b)))→
((a,b)∈ Xo.sb || ((b,a)∈ Xo.sb))
let well_formed_threads (Xo,_,_) =
(∀ (a ∈ Xo.actions). well_formed_action a)&&
(
actions_respect_location_kinds Xo.actions Xo.lk &&
(
blocking_observed Xo.actions Xo.sb &&
(
inj_on aid_of Xo.actions &&
(
relation_over Xo.actions Xo.sb &&
(
relation_over Xo.actions Xo.asw &&
(
threadwise Xo.actions Xo.sb &&
(
strict_partial_order Xo.sb &&
(
strict_partial_order Xo.dd &&
(Xo.dd subset Xo.sb &&
indeterminate_sequencing Xo)))))))))
(*********************************************** *)
(* 4 - Memory_Model simplified, single thread, no atomics *)
(*********************************************** *)
let visible_side_effect_set actions hb =
{ (a,b) | ∀ ((a,b) ∈ hb) |
is_write a && ( is_read b && ((loc_of a = loc_of b)&&
not ( ∃ (c ∈ actions). not (c ∈ {a;b})&&
(
is_write c && ((loc_of c = loc_of b)&&
((a,c)∈ hb && ((c,b)∈ hb))))))) }
let det_read (Xo,Xw,_::("vse",vse)::_) =
∀ (r ∈ Xo.actions).
is_load r →
((∃ (w ∈ Xo.actions). (w,r)∈ vse) =
(∃ (w' ∈ Xo.actions). (w',r)∈ Xw.rf))
let consistent_non_atomic_rf (Xo,Xw,_::("vse",vse)::_) =
∀ ((w,r) ∈ Xw.rf). is_at_non_atomic_location Xo.lk r →
((w,r)∈ vse)
let well_formed_rf (Xo,Xw,_) =
∀ ((a,b) ∈ Xw.rf).
a ∈ Xo.actions && (b ∈ Xo.actions &&
(
loc_of a = loc_of b &&
(
is_write a && ( is_read b &&
(
value_read_by b = value_written_by a &&
(∀ (a' ∈ Xo.actions). ((a',b)∈ Xw.rf)→ (a = a')))))))
let sc_mo_lo_empty (_,Xw,_) = Set.is_empty Xw.sc && ( Set.is_empty Xw.mo && Set.is_empty Xw.lo)
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) ]
let single_thread_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("sc_mo_lo_empty", Leaf sc_mo_lo_empty);
("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) ]) ]
(*********************************************** *)
let indeterminate_reads (Xo,Xw,_) =
{b | ∀ (b ∈ Xo.actions) | is_read b && not (∃ (a ∈ Xo.actions). (a,b)∈ Xw.rf)}
let unsequenced_races (Xo,_,_) =
{ (a,b) | ∀ (a ∈ Xo.actions) (b ∈ Xo.actions) |
is_at_non_atomic_location Xo.lk a &&
(
not (a = b)&& ((loc_of a = loc_of b)&& ((is_write a || is_write b)&&
((tid_of a = tid_of b)&&
not ((a,b)∈ Xo.sb || ((b,a)∈ Xo.sb)))))) }
let single_thread_undefined_behaviour =
[ Two ("unsequenced_races", unsequenced_races);
One ("indeterminate_reads", indeterminate_reads) ]
val single_thread_protocol : protocol_t
let single_thread_protocol ((Xo,_,_):complete_execution) =
∃ (b ∈ Xo.actions). ∀ (a ∈ Xo.actions).
(tid_of a = tid_of b)&&
match (loc_of a) with
None -> false
| Some l -> (Xo.lk l = Non_Atomic)
end
let single_thread_memory_model =
<| consistent = single_thread_consistent_execution;
relation_calculation = single_thread_relations;
undefined = single_thread_undefined_behaviour;
relation_flags =
<| rf_flag = true;
mo_flag = false;
sc_flag = false;
lo_flag = false;
ao_flag = false;
tot_flag = false |>
|>
val single_thread_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 5 - Memory_Model simplified, multi-thread, no atomics, yes locks *)
(*********************************************** *)
let locks_only_sw actions asw lo a b =
(tid_of a <> tid_of b)&&
( (* thread sync *)
(a,b)∈ asw ||
(* mutex sync *)
(is_unlock a && ( is_successful_lock b && ((a,b)∈ lo)))
)
let locks_only_sw_set actions asw lo =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
locks_only_sw actions asw lo a b }
let no_consume_hb sb sw =
tc (sb ∪ sw)
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) ]
let sc_mo_empty (_,Xw,_) = Set.is_empty Xw.sc && Set.is_empty Xw.mo
let locks_only_consistent_lo (Xo,Xw,("hb",hb)::_) =
relation_over Xo.actions Xw.lo &&
(
trans Xw.lo &&
(
irrefl Xw.lo &&
(∀ (a ∈ Xo.actions) (b ∈ Xo.actions).
((a,b)∈ Xw.lo)→ ( not ((b,a)∈ hb)&&
(((a,b)∈ Xw.lo || ((b,a)∈ Xw.lo))
= ( (not (a = b))&&
((is_lock a || is_unlock a)&& ((is_lock b || is_unlock b)&&
((loc_of a = loc_of b)&&
is_at_mutex_location Xo.lk a))) ))))))
let locks_only_consistent_locks (Xo,Xw,_) =
(∀ ((a,c) ∈ Xw.lo).
(
is_successful_lock a && is_successful_lock c)→
(∃ (b ∈ Xo.actions). is_unlock b && ((a,b)∈ Xw.lo && ((b,c)∈ Xw.lo))))
let consistent_hb (Xo,_,("hb",hb)::_) =
irrefl (tc hb)
let locks_only_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("sc_mo_empty", Leaf sc_mo_empty);
("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_hb", Leaf consistent_hb);
("consistent_rf",
Node [ ("det_read", Leaf det_read);
("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf) ]) ]
(*********************************************** *)
let locks_only_good_mutex_use actions lk sb lo a =
(* violated requirement: The calling thread shall own the mutex. *)
( is_unlock a →
( ∃ (al ∈ actions).
is_successful_lock al && ((al,a)∈ sb &&
adjacent_less_than lo actions al a) ) )&&
(* violated requirement: The calling thread does not own the mutex. *)
( is_lock a →
not ( ∃ (al ∈ actions).
is_successful_lock al && ((al,a)∈ sb &&
adjacent_less_than lo actions al a) ) )
let locks_only_bad_mutexes (Xo,Xw,_) =
{ a | ∀ (a ∈ Xo.actions) |
not (locks_only_good_mutex_use Xo.actions Xo.lk Xo.sb Xw.lo a)}
let data_races (Xo,Xw,("hb",hb)::_) =
{ (a,b) | ∀ (a ∈ Xo.actions) (b ∈ Xo.actions) |
not (a = b)&& ((loc_of a = loc_of b)&& ((is_write a || is_write b)&&
((tid_of a <> tid_of b)&&
(
not (is_atomic_action a && is_atomic_action b)&&
not ((a,b)∈ hb || ((b,a)∈ hb)))))) }
let good_mutex_use actions lk sb lo a =
let mutexes_at_l =
{a' | ∀ (a' ∈ actions) | (is_lock a' || is_unlock a')&& (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 → ( ∃ (al ∈ actions).
is_successful_lock al && ((al,a)∈ sb &&
adjacent_less_than lock_order actions al a) ) )&&
(* violated requirement: The calling thread does not own the mutex. *)
( is_lock a →
not ( ∃ (al ∈ actions).
is_successful_lock al && ((tid_of a = tid_of al)&&
adjacent_less_than lock_order actions al a) ) )
let bad_mutexes (Xo,Xw,_) =
{ a | ∀ (a ∈ Xo.actions) | not (good_mutex_use Xo.actions Xo.lk Xo.sb Xw.sc a)}
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) ]
(*********************************************** *)
val locks_only_protocol : protocol_t
let locks_only_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match (loc_of a) with
None -> false
| Some l -> (Xo.lk l ∈ {Mutex;Non_Atomic})
end
let locks_only_memory_model =
<| consistent = locks_only_consistent_execution;
relation_calculation = locks_only_relations;
undefined = locks_only_undefined_behaviour;
relation_flags =
<| rf_flag = true;
mo_flag = false;
sc_flag = false;
lo_flag = true;
ao_flag = false;
tot_flag = false |>
|>
val locks_only_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 6 - relaxed - memory_model simplified for programs without sc,
consumes, release or acquire *)
(*********************************************** *)
let sc_empty (_,Xw,_) = (Set.is_empty Xw.sc)
let consistent_atomic_rf (Xo,Xw,("hb",hb)::_) =
∀ ((w,r) ∈ Xw.rf). ( is_at_atomic_location Xo.lk r && is_load r)→
not ((r,w)∈ hb)
let rmw_atomicity (Xo,Xw,_) =
∀ (b ∈ Xo.actions) (a ∈ Xo.actions).
is_RMW b → (adjacent_less_than Xw.mo Xo.actions a b = ((a,b)∈ Xw.rf))
let coherent_memory_use (Xo,Xw,("hb",hb)::_) =
(* CoRR *)
( not ( ∃ ((a,b) ∈ Xw.rf) ((c,d) ∈ Xw.rf).
(b,d)∈ hb && ((c,a)∈ Xw.mo) ) )&&
(* CoWR *)
(( not ( ∃ ((a,b) ∈ Xw.rf) (c ∈ Xo.actions).
(c,b)∈ hb && ((a,c)∈ Xw.mo) ) )&&
(* CoRW *)
(( not ( ∃ ((a,b) ∈ Xw.rf) (c ∈ Xo.actions).
(b,c)∈ hb && ((c,a)∈ Xw.mo) ) )&&
(* CoWW *)
( not (∃ ((a,b) ∈ hb). (b,a)∈ Xw.mo) )))
let consistent_mo (Xo,Xw,_) =
relation_over Xo.actions Xw.mo &&
(
trans Xw.mo &&
(
irrefl Xw.mo &&
(∀ (a ∈ Xo.actions) (b ∈ Xo.actions).
((a,b)∈ Xw.mo || ((b,a)∈ Xw.mo))
= ( (not (a = b))&&
(
is_write a && ( is_write b &&
((loc_of a = loc_of b)&&
is_at_atomic_location Xo.lk a))) ))))
let relaxed_only_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("sc_empty", Leaf sc_empty);
("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_hb", Leaf consistent_hb);
("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
let relaxed_only_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> mo ∈ {NA;Relaxed}
| Store _ _ mo _ _ -> mo ∈ {NA;Relaxed}
| RMW _ _ mo _ _ _ -> mo ∈ {Relaxed}
| Fence _ _ _ -> false
| Blocked_rmw _ _ _ -> true end
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val relaxed_only_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 7 - release acquire - memory_model simplified for programs without sc,
consumes or relaxed *)
(*********************************************** *)
(* Unused in this model currently, causes me to encounter the non-atomic LB writes problem, which can be solved for the simpler model. *)
let release_acquire_coherent_memory_use (Xo,Xw,("hb",hb)::_) =
(* CoWR *)
( not ( ∃ ((a,b) ∈ Xw.rf) (c ∈ Xo.actions).
(c,b)∈ hb && ((a,c)∈ Xw.mo) ) )&&
(* CoWW *)
( not (∃ ((a,b) ∈ hb). (b,a)∈ Xw.mo) )
let atomic_initialisation_first (Xo,_,_) =
∀ (a ∈ Xo.actions) (b ∈ Xo.actions).
(
is_at_atomic_location Xo.lk a && ( is_NA_store a &&
(
is_write b && (loc_of a = loc_of b))))→
(((a,b)∈ tc (Xo.sb ∪ Xo.asw))&& not (is_NA_store b))
(* Deprecated, TODO remove, rework proofs *)
let atomic_unsequenced_races (Xo,_,_) =
{ (a,b) | ∀ (a ∈ Xo.actions) (b ∈ Xo.actions) |
is_at_atomic_location Xo.lk a &&
(
not (a = b)&& ((loc_of a = loc_of b)&& ((is_write a || is_write b)&&
((tid_of a = tid_of b)&&
not ((a,b)∈ Xo.sb || ((b,a)∈ Xo.sb)))))) }
val release_acquire_protocol : protocol_t
let release_acquire_protocol ((Xo,Xw,rl):complete_execution) =
atomic_initialisation_first (Xo,Xw,rl)&&
(
Set.is_empty (atomic_unsequenced_races (Xo,Xw,rl))&&
(∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release})
| RMW _ _ mo _ _ _ -> mo = Acq_rel
| Fence _ _ _ -> false
| Blocked_rmw _ _ _ -> true end))
let release_acquire_synchronizes_with actions sb asw rf lo a b =
(tid_of a <> tid_of b)&&
( (* thread sync *)
(a,b)∈ asw ||
(* mutex sync *)
((is_unlock a && ( is_successful_lock b && ((a,b)∈ lo))) ||
(* rel/acq sync *)
( is_release a && ( is_acquire b && ((a,b)∈ rf)) ))
)
let release_acquire_synchronizes_with_set actions sb asw rf lo =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
release_acquire_synchronizes_with actions sb asw rf lo a b}
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) ]
(*********************************************** *)
(* Unused currently, see R/A coherence above *)
let release_acquire_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("sc_empty", Leaf sc_empty);
("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_hb", Leaf consistent_hb);
("consistent_rf",
Node [ ("det_read", Leaf det_read);
("consistent_non_atomic_rf", Leaf consistent_non_atomic_rf);
("consistent_atomic_rf", Leaf consistent_atomic_rf);
("release_acquire_coherent_memory_use", Leaf release_acquire_coherent_memory_use);
("rmw_atomicity", Leaf rmw_atomicity) ]) ]
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val release_acquire_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 8 - release_acquire_relaxed - memory_model simplified for programs without sc,
consumes or relaxed *)
(*********************************************** *)
val release_acquire_relaxed_protocol : protocol_t
let release_acquire_relaxed_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire;Relaxed})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release;Relaxed})
| RMW _ _ mo _ _ _ -> (mo ∈ {Acq_rel;Acquire;Release;Relaxed})
| Fence _ _ _ -> false
| Blocked_rmw _ _ _ -> true end
let release_acquire_relaxed_synchronizes_with actions sb asw rf lo rs a b =
(tid_of a <> tid_of b)&&
( (* thread sync *)
(a,b)∈ asw ||
(* mutex sync *)
((is_unlock a && ( is_successful_lock b && ((a,b)∈ lo))) ||
(* rel/acq sync *)
( is_release a && ( is_acquire b &&
(∃ (c ∈ actions). (a,c)∈ rs && ((c,b)∈ rf))) ))
)
let rs_element head a =
(tid_of a = tid_of head) || is_RMW a
let release_sequence_set actions lk mo =
{ (rel,b) | ∀ (rel ∈ actions) (b ∈ actions) |
is_release rel &&
( (b = rel) ||
( (rel,b)∈ mo &&
(
rs_element rel b &&
(∀ (c ∈ actions).
((rel,c)∈ mo && ((c,b)∈ mo))→ rs_element rel c)) ) ) }
let release_acquire_relaxed_synchronizes_with_set actions sb asw rf lo rs =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
release_acquire_relaxed_synchronizes_with actions sb asw rf lo rs a b}
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) ]
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val release_acquire_relaxed_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 9 - release_acquire_fenced *)
(*********************************************** *)
val release_acquire_fenced_protocol : protocol_t
let release_acquire_fenced_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire;Relaxed})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release;Relaxed})
| RMW _ _ mo _ _ _ -> (mo ∈ {Acq_rel;Acquire;Release;Relaxed})
| Fence _ _ mo -> (mo ∈ {Release;Acquire;Relaxed})
| Blocked_rmw _ _ _ -> true end
let release_acquire_fenced_synchronizes_with actions sb asw rf lo rs hrs a b =
(tid_of a <> tid_of b)&&
( (* thread sync *)
(a,b)∈ asw ||
(* mutex sync *)
((is_unlock a && ( is_successful_lock b && ((a,b)∈ lo))) ||
(* rel/acq sync *)
(( is_release a && ( is_acquire b &&
(∃ (c ∈ actions). (a,c)∈ rs && ((c,b)∈ rf))) ) ||
(* fence synchronisation *)
(( is_fence a && ( is_release a && ( is_fence b && ( is_acquire b &&
(∃ (x ∈ actions) (z ∈ actions) (y ∈ actions).
(a,x)∈ sb && ((x,z)∈ hrs && ((z,y)∈ rf && ((y,b)∈ sb)))))))) ||
(( is_fence a && ( is_release a && ( is_acquire b &&
(∃ (x ∈ actions) (y ∈ actions).
(a,x)∈ sb && ((x,y)∈ hrs && ((y,b)∈ rf))))) ) ||
( is_release a && ( is_fence b && ( is_acquire b &&
(∃ (y ∈ actions) (x ∈ actions).
(a,y)∈ rs && ((y,x)∈ rf && ((x,b)∈ sb)))))))))) )
let hypothetical_release_sequence_set actions lk mo =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
is_atomic_action a &&
(
is_write a &&
( (b = a) ||
( (a,b)∈ mo &&
(
rs_element a b &&
(∀ (c ∈ actions).
((a,c)∈ mo && ((c,b)∈ mo))→ rs_element a c)) ) )) }
let release_acquire_fenced_synchronizes_with_set actions sb asw rf lo rs hrs =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
release_acquire_fenced_synchronizes_with actions sb asw rf lo rs hrs a b}
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) ]
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val release_acquire_fenced_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 10 - sc, no sc fences *)
(*********************************************** *)
val sc_accesses_protocol : protocol_t
let sc_accesses_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire;Relaxed;Seq_cst})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release;Relaxed;Seq_cst})
| RMW _ _ mo _ _ _ -> (mo ∈ {Acq_rel;Acquire;Release;Relaxed;Seq_cst})
| Fence _ _ mo -> (mo ∈ {Release;Acquire;Relaxed})
| Blocked_rmw _ _ _ -> true end
let sc_accesses_consistent_sc (Xo,Xw,("hb",hb)::_) =
relation_over Xo.actions Xw.sc &&
(
trans Xw.sc &&
(
irrefl Xw.sc &&
(∀ (a ∈ Xo.actions) (b ∈ Xo.actions).
(((a,b)∈ Xw.sc)→ not ((b,a)∈ hb ∪ Xw.mo))&&
( ((a,b)∈ Xw.sc || ((b,a)∈ Xw.sc)) =
( (not (a = b))&& ( is_seq_cst a && is_seq_cst b))
))))
let sc_accesses_sc_reads_restricted (Xo,Xw,("hb",hb)::_) =
∀ ((w,r) ∈ Xw.rf). is_seq_cst r →
(( is_seq_cst w && ((w,r)∈ Xw.sc &&
not (∃ (w' ∈ Xo.actions).
is_write w' && ((loc_of w = loc_of w')&&
((w,w')∈ Xw.sc && ((w',r)∈ Xw.sc))) )) ) ||
( not (is_seq_cst w)&&
not (∃ (w' ∈ Xo.actions).
is_write w' && ((loc_of w = loc_of w')&&
((w,w')∈ hb && ((w',r)∈ Xw.sc))) ) ))
let sc_accesses_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("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_hb", Leaf consistent_hb);
("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) ]) ]
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val sc_accesses_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 11 - sc_fences, no consume *)
(*********************************************** *)
val sc_fenced_protocol : protocol_t
let sc_fenced_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire;Relaxed;Seq_cst})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release;Relaxed;Seq_cst})
| RMW _ _ mo _ _ _ -> (mo ∈ {Acq_rel;Acquire;Release;Relaxed;Seq_cst})
| Fence _ _ mo -> (mo ∈ {Release;Acquire;Relaxed;Seq_cst})
| Blocked_rmw _ _ _ -> true end
let sc_fenced_sc_fences_heeded (Xo,Xw,_) =
∀ (f ∈ Xo.actions) (f' ∈ Xo.actions)
(r ∈ Xo.actions)
(w ∈ Xo.actions) (w' ∈ Xo.actions).
not ( is_fence f && ( is_fence f' &&
( (* fence restriction N3291 29.3p4 *)
( (w,w')∈ Xw.mo &&
((w',f)∈ Xw.sc &&
((f,r)∈ Xo.sb &&
((w,r)∈ Xw.rf))) ) ||
(* fence restriction N3291 29.3p5 *)
(( (w,w')∈ Xw.mo &&
((w',f)∈ Xo.sb &&
((f,r)∈ Xw.sc &&
((w,r)∈ Xw.rf))) ) ||
(* fence restriction N3291 29.3p6 *)
(( (w,w')∈ Xw.mo &&
((w',f)∈ Xo.sb &&
((f,f')∈ Xw.sc &&
((f',r)∈ Xo.sb &&
((w,r)∈ Xw.rf)))) ) ||
(* SC fences impose mo N3291 29.3p7 *)
(( (w',f)∈ Xo.sb &&
((f,f')∈ Xw.sc &&
((f',w)∈ Xo.sb &&
((w,w')∈ Xw.mo))) ) ||
(* N3291 29.3p7, w collapsed first write*)
(( (w',f)∈ Xw.sc &&
((f,w)∈ Xo.sb &&
((w,w')∈ Xw.mo)) ) ||
(* N3291 29.3p7, w collapsed second write*)
( (w',f)∈ Xo.sb &&
((f,w)∈ Xw.sc &&
((w,w')∈ Xw.mo)) ))))) )) )
let sc_fenced_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("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_hb", Leaf consistent_hb);
("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) ]) ]
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val sc_fenced_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 12 - with consume *)
(*********************************************** *)
val with_consume_protocol : protocol_t
let with_consume_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire;Relaxed;Seq_cst;Consume})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release;Relaxed;Seq_cst})
| RMW _ _ mo _ _ _ -> (mo ∈ {Acq_rel;Acquire;Release;Relaxed;Seq_cst})
| Fence _ _ mo -> (mo ∈ {Release;Acquire;Relaxed;Seq_cst})
| Blocked_rmw _ _ _ -> true end
let with_consume_cad_set actions sb dd rf = tc ( (rf ^cap; sb)∪ dd )
let with_consume_dob actions rf rs cad w a =
tid_of w <> tid_of a &&
(∃ (w' ∈ actions) (r ∈ actions).
is_consume r &&
((w,w')∈ rs && ((w',r)∈ rf &&
( (r,a)∈ cad || (r = a) ))))
let dependency_ordered_before actions rf rs cad a d =
a ∈ actions && (d ∈ actions &&
( ∃ (b ∈ actions). is_release a && ( is_consume b &&
((∃ (e ∈ actions). (a,e)∈ rs && ((e,b)∈ rf))&&
( (b,d)∈ cad || (b = d) ))) ))
let with_consume_dob_set actions rf rs cad =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
dependency_ordered_before actions rf rs cad a b}
let compose R1 R2 =
{ (w,z) | ∀ ((w,x) ∈ R1) ((y,z) ∈ R2) | (x = y) }
let inter_thread_happens_before actions sb sw dob =
let r = sw ∪ dob ∪ (compose sw sb) in
tc (r ∪ (compose sb r))
let happens_before actions sb ithb =
sb ∪ ithb
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 = 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);
("sw", sw);
("rs", rs);
("hrs", hrs);
("dob", dob);
("cad", cad) ]
let with_consume_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("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_hb", Leaf consistent_hb);
("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) ]) ]
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val with_consume_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 13 - the standard model *)
(*********************************************** *)
let standard_vsses actions lk mo hb vse =
{ (v,r) |
∀ (r ∈ actions)
(v ∈ actions)
(head ∈ actions) |
is_at_atomic_location lk r &&
((head,r)∈ vse &&
(
not (∃ (v' ∈ actions). (v',r)∈ vse && ((head,v')∈ mo))&&
( v = head ||
( (head,v)∈ mo && ( not ((r,v)∈ hb)&&
(∀ (w ∈ actions).
((head,w)∈ mo && ((w,v)∈ mo))→ not ((r,w)∈ hb)))
)
)))
}
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 = 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 = 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) ]
let standard_consistent_atomic_rf (Xo,Xw,_::_::_::("vsses",vsses)::_) =
∀ ((w,r) ∈ Xw.rf). ( is_at_atomic_location Xo.lk r && is_load r)→
((w,r)∈ vsses)
let standard_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("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_hb", Leaf consistent_hb);
("consistent_rf",
Node [ ("det_read", Leaf 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) ]) ]
(*********************************************** *)
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 = true;
ao_flag = false;
tot_flag = false |>
|>
val standard_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 14 - release acquire SC - memory_model simplified for programs without
consumes or relaxed *)
(*********************************************** *)
(* No longer applicable: If Nick was going to use this, I would want to strengthen up SC fences, and think some more about the SC fence absorbsion mismatch. I would also need to cut down hb to hthe SC portion that Nick discussed. *)
val release_acquire_SC_protocol : protocol_t
let release_acquire_SC_protocol ((Xo,Xw,rl):complete_execution) =
atomic_initialisation_first (Xo,Xw,rl)&&
(
Set.is_empty (atomic_unsequenced_races (Xo,Xw,rl))&&
(∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire;Seq_cst})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release;Seq_cst})
| RMW _ _ mo _ _ _ -> (mo ∈ {Acq_rel;Seq_cst})
| Fence _ _ mo -> (mo ∈ {Seq_cst})
| Blocked_rmw _ _ _ -> true end))
(*********************************************** *)
let release_acquire_SC_memory_model =
<| consistent = sc_fenced_consistent_execution;
relation_calculation = release_acquire_relations;
undefined = locks_only_undefined_behaviour;
relation_flags =
<| rf_flag = true;
mo_flag = true;
sc_flag = true;
lo_flag = true;
ao_flag = false;
tot_flag = false |>
|>
val release_acquire_SC_behaviour : opsem_t -> program -> program_behaviours
val release_acquire_SC_rf_behaviour : opsem_t -> program -> rf_program_behaviours
(*********************************************** *)
(* 15 - SC - memory_model simplified for programs without release, acquire,
consumes or relaxed *)
(*********************************************** *)
val SC_protocol : protocol_t
let SC_protocol ((Xo,Xw,rl):complete_execution) =
atomic_initialisation_first (Xo,Xw,rl)&&
(
Set.is_empty (atomic_unsequenced_races (Xo,Xw,rl))&&
(∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Seq_cst})
| Store _ _ mo _ _ -> (mo ∈ {NA;Seq_cst})
| RMW _ _ mo _ _ _ -> (mo ∈ {Seq_cst})
| Fence _ _ mo -> false
| Blocked_rmw _ _ _ -> true end))
(*********************************************** *)
let SC_memory_model =
<| consistent = sc_accesses_consistent_execution;
relation_calculation = release_acquire_relations;
undefined = locks_only_undefined_behaviour;
relation_flags =
<| rf_flag = true;
mo_flag = true;
sc_flag = true;
lo_flag = true;
ao_flag = false;
tot_flag = false |>
|>
val SC_behaviour : opsem_t -> program -> program_behaviours
(*********************************************** *)
(* 16 - tot - sequential consistency *)
(*********************************************** *)
val tot_protocol : protocol_t
let tot_protocol ((Xo,Xw,rl):complete_execution) =
( true (* Something to stop rf hb cycles *) )&&
(
atomic_initialisation_first (Xo,Xw,rl)&&
(
Set.is_empty (atomic_unsequenced_races (Xo,Xw,rl))&&
(∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> true
| Unlock _ _ _ -> true
| Load _ _ mo _ _ -> (mo ∈ {NA;Seq_cst})
| Store _ _ mo _ _ -> (mo ∈ {NA;Seq_cst})
| RMW _ _ mo _ _ _ -> (mo ∈ {Seq_cst})
| Fence _ _ mo -> false
| Blocked_rmw _ _ _ -> true end)))
(* How closely do I model hb in this model? I don't necessarily want to require tot to have finite prefixes, because I don't have that for hb, do I have to? I don't think so. Things have cahnged somewhat since I last thought about that. Now I know that atomics and locks are never unordered by sb, for instance. *)
let tot_relations Xo Xw =
let sw = release_acquire_synchronizes_with_set
Xo.actions Xo.sb Xo.asw Xw.rf Xw.tot in
let hb = no_consume_hb Xo.sb sw in
let vse = visible_side_effect_set Xo.actions Xw.tot in
[ ("empty", {});
("vse", vse);
]
let tot_consistent_rf (Xo,Xw,_::("vse",vse)::_) =
∀ ((w,r) ∈ Xw.rf). (w,r)∈ vse
let tot_consistent_locks (Xo,Xw,_) =
(∀ ((a,c) ∈ Xw.tot).
(
is_successful_lock a && ( is_successful_lock c && (loc_of a = loc_of c)))→
(∃ (b ∈ Xo.actions). (loc_of a = loc_of b)&& ( is_unlock b && ((a,b)∈ Xw.tot && ((b,c)∈ Xw.tot)))))
let tot_conistent_tot (Xo,Xw,_) =
relation_over Xo.actions Xw.tot &&
(
trans Xw.tot &&
(
irrefl Xw.tot &&
(
total Xo.actions Xw.tot &&
(Xo.sb subset Xw.tot &&
(Xo.asw subset Xw.tot)))))
let tot_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("well_formed_threads", Leaf well_formed_threads);
("well_formed_rf", Leaf well_formed_rf);
("tot_conistent_tot", Leaf tot_conistent_tot);
("tot_consistent_locks", Leaf tot_consistent_locks);
("consistent_rf",
Node [ ("det_read", Leaf det_read);
("tot_consistent_rf", Leaf tot_consistent_rf)
]
)
]
let tot_bad_mutexes (Xo,Xw,_) =
{ a | ∀ (a ∈ Xo.actions) |
let lo = { (a,b) | ∀ (a ∈ Xo.actions) (b ∈ Xo.actions) |
((a,b)∈ Xw.tot)&& ((loc_of a = loc_of b)&&
is_at_mutex_location Xo.lk a)
} in
not (locks_only_good_mutex_use Xo.actions Xo.lk Xo.sb lo a)}
let tot_data_races (Xo,Xw,_) =
{ (a,b) | ∀ (a ∈ Xo.actions) (b ∈ Xo.actions) |
not (a = b)&& ((loc_of a = loc_of b)&& ((is_write a || is_write b)&&
((tid_of a <> tid_of b)&&
(
not (is_atomic_action a && is_atomic_action b)&&
not (∃ (c ∈ Xo.actions). ((a,c)∈ Xw.tot)&& ((c,b)∈ Xw.tot)))))) }
let tot_undefined_behaviour =
[ Two ("unsequenced_races", unsequenced_races);
Two ("data_races", data_races);
One ("indeterminate_reads", indeterminate_reads);
One ("tot_bad_mutexes", tot_bad_mutexes) ]
(*********************************************** *)
let tot_memory_model =
<| consistent = tot_consistent_execution;
relation_calculation = tot_relations;
undefined = locks_only_undefined_behaviour;
relation_flags =
<| rf_flag = true;
mo_flag = false;
sc_flag = false;
lo_flag = false;
ao_flag = false;
tot_flag = true; |>
|>
val tot_behaviour : opsem_t -> program -> program_behaviours
val tot_rf_behaviour : opsem_t -> program -> rf_program_behaviours
(***********************)
(* - 16 - Meta-theory *)
(***********************)
val thm0 : bool
val thm1 : bool
val thm2 : bool
val thm3 : bool
val thm4 : bool
val thm6 : bool
val thm7 : bool
val thm8 : bool
val thm9 : bool
val thm10 : bool
val thm5 : bool
val thm11 : bool
val thm12 : bool
val bigthm : bool
(*********************************************** *)
(* 17 - release acquire, no locks - memory_model simplified for programs without sc,
consumes, relaxed or locks *)
(*********************************************** *)
val release_acquire_no_locks_protocol : protocol_t
let release_acquire_no_locks_protocol ((Xo,_,_):complete_execution) =
∀ (a ∈ Xo.actions).
match a with
| Lock _ _ _ _ -> false
| Unlock _ _ _ -> false
| Load _ _ mo _ _ -> (mo ∈ {NA;Acquire})
| Store _ _ mo _ _ -> (mo ∈ {NA;Release})
| RMW _ _ mo _ _ _ -> mo = Acq_rel
| Fence _ _ _ -> false
| Blocked_rmw _ _ _ -> true end
let release_acquire_no_locks_synchronizes_with actions sb asw rf a b =
(tid_of a <> tid_of b)&&
( (* thread sync *)
(a,b)∈ asw ||
(* rel/acq sync *)
( is_release a && ( is_acquire b && ((a,b)∈ rf)) )
)
let release_acquire_no_locks_synchronizes_with_set actions sb asw rf =
{ (a,b) | ∀ (a ∈ actions) (b ∈ actions) |
release_acquire_no_locks_synchronizes_with actions sb asw rf a b}
let release_acquire_no_locks_relations Xo Xw =
let sw = release_acquire_no_locks_synchronizes_with_set
Xo.actions Xo.sb Xo.asw Xw.rf 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) ]
let sc_lo_empty (_,Xw,_) = Set.is_empty Xw.sc && Set.is_empty Xw.lo
let release_acquire_no_locks_consistent_execution =
Node [ ("assumptions", Leaf assumptions);
("sc_lo_empty", Leaf sc_empty);
("well_formed_threads", Leaf well_formed_threads);
("well_formed_rf", Leaf well_formed_rf);
("consistent_mo", Leaf consistent_mo);
("consistent_hb", Leaf consistent_hb);
("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) ]) ]
(*********************************************** *)
let release_acquire_no_locks_undefined_behaviour =
[ Two ("unsequenced_races", unsequenced_races);
Two ("data_races", data_races);
One ("indeterminate_reads", indeterminate_reads); ]
let release_acquire_no_locks_memory_model =
<| consistent = release_acquire_no_locks_consistent_execution;
relation_calculation = release_acquire_no_locks_relations;
undefined = release_acquire_no_locks_undefined_behaviour;
relation_flags =
<| rf_flag = true;
mo_flag = true;
sc_flag = false;
lo_flag = true;
ao_flag = false;
tot_flag = false |>
|>
val release_acquire_no_locks_behaviour : opsem_t -> program -> program_behaviours