(* Help emacs fontification -*-caml-*- *) (*********************************************** *) (*********************************************** *) (*********************************************** *) (* set-theoretic preliminaries *) let irrefl s ord = forall (x IN s). not ((x,x) IN ord) let trans s ord = forall (x IN s) (y IN s) (z IN s). (((x,y) IN ord) && ((y,z) IN ord)) --> ((x,z) IN ord) (*val cross : forall 'a. 'a set -> 'a set -> ('a * 'a) set*) let cross S T = { (s,t) | forall (s IN S) (t IN T) | true} indreln {isabelle} forall r x y. r (x, y) ==> tc' r (x, y) and forall r x y. (exist z. tc' r (x,z) && tc' r (z,y)) ==> tc' r (x,y) val tc : forall 'a. ('a * 'a) set -> ('a * 'a) set let {isabelle} tc r = let r' = fun (x,y) -> ((x,y) IN r) in { (x,y) | forall ((x,y) IN r) | tc' r' (x,y) } let rec {ocaml} tc r = let one_step = { (x,z) | forall ((x,y) IN r) ((y',z) IN r) | y = y' } in if one_step subset r then r else tc (one_step union r) sub [hol] tc = tc let restrict_relation_set rel s = (rel) inter (cross s s) let strict_preorder s ord = irrefl s (ord) && trans s (ord) let relation_over s rel = forall ((a,b) IN rel). a IN s && b IN s (*domain rel s subset s && range rel subset s*) let inj_on f A = (forall (x IN A). (forall (y IN A). (f x = f y) --> (x = y))) let total_order_over s ord = relation_over s ord && (forall (x IN s) (y IN s). (x,y) IN ord || (y,x) IN ord || (x = y)) let strict_total_order_over s ord = strict_preorder s ord && total_order_over s ord let adjacent_less_than ord s x y = (x,y) IN ord && not (exist (z IN s). (x,z) IN ord && (z,y) IN ord) let adjacent_less_than_such_that pred ord s x y = pred x && (x,y) IN ord && not (exist (z IN s). pred z && (x,z) IN ord && (z,y) IN ord) (*********************************************** *) (*********************************************** *) (*********************************************** *) (* basic model - NB, presumably this is *with* vsses, whereas we now primarily use the no-vsses variant below *) type action_id = num type thread_id = num type location = num type value = num type memory_order = Mo_seq_cst | Mo_relaxed | Mo_release | Mo_acquire | Mo_consume | Mo_acq_rel type lock_outcome = Success | Blocked type action = | Lock of action_id * thread_id * location * lock_outcome | Unlock of action_id * thread_id * location | Atomic_load of action_id * thread_id * memory_order * location * value | Atomic_store of action_id * thread_id * memory_order * location * value | Atomic_rmw of action_id * thread_id * memory_order * location * value * value | Load of action_id * thread_id * location * value | Store of action_id * thread_id * location * value | Fence of action_id * thread_id * memory_order | Blocked_rmw of action_id * thread_id * location let action_id_of a = match a with | Lock aid _ _ _ -> aid | Unlock aid _ _ -> aid | Atomic_load aid _ _ _ _ -> aid | Atomic_store aid _ _ _ _ -> aid | Atomic_rmw aid _ _ _ _ _ -> aid | Load aid _ _ _ -> aid | Store aid _ _ _ -> aid | Fence aid _ _ -> aid | Blocked_rmw aid _ _ -> aid end let thread_id_of a = match a with Lock _ tid _ _ -> tid | Unlock _ tid _ -> tid | Atomic_load _ tid _ _ _ -> tid | Atomic_store _ tid _ _ _ -> tid | Atomic_rmw _ tid _ _ _ _ -> tid | Load _ tid _ _ -> tid | Store _ tid _ _ -> tid | Fence _ tid _ -> tid | Blocked_rmw _ tid _ -> tid end let memory_order_of a = match a with Atomic_load _ _ mo _ _ -> Some mo | Atomic_store _ _ mo _ _ -> Some mo | Atomic_rmw _ _ mo _ _ _ -> Some mo | Fence _ _ mo -> Some mo | _ -> None end let location_of a = match a with Lock _ _ l _ -> Some l | Unlock _ _ l -> Some l | Atomic_load _ _ _ l _ -> Some l | Atomic_store _ _ _ l _ -> Some l | Atomic_rmw _ _ _ l _ _ -> Some l | Load _ _ l _ -> Some l | Store _ _ l _ -> Some l | Fence _ _ _ -> None | Blocked_rmw _ _ l -> Some l end let value_read_by a = match a with Atomic_load _ _ _ _ v -> Some v | Atomic_rmw _ _ _ _ v _ -> Some v | Load _ _ _ v -> Some v | _ -> None end let value_written_by a = match a with Atomic_store _ _ _ _ v -> Some v | Atomic_rmw _ _ _ _ _ v -> Some v | Store _ _ _ v -> Some v | _ -> None end let is_lock a = match a with Lock _ _ _ _ -> true | _ -> false end let is_successful_lock a = match a with Lock _ _ _ Success -> true | _ -> false end let is_blocked_lock a = match a with Lock _ _ _ Blocked -> true | _ -> false end let is_unlock a = match a with Unlock _ _ _ -> true | _ -> false end let is_atomic_load a = match a with Atomic_load _ _ _ _ _ -> true | _ -> false end let is_atomic_store a = match a with Atomic_store _ _ _ _ _ -> true | _ -> false end let is_atomic_rmw a = match a with Atomic_rmw _ _ _ _ _ _ -> true | _ -> false end let is_blocked_rmw a = match a with Blocked_rmw _ _ _ -> true | _ -> false end let is_load a = match a with Load _ _ _ _ -> true | _ -> false end let is_store a = match a with Store _ _ _ _ -> true | _ -> false end let is_fence a = match a with Fence _ _ _ -> true | _ -> false end (**************************************** *) let is_lock_or_unlock a = is_lock a || is_unlock a let is_atomic_action a = is_atomic_load a || is_atomic_store a || is_atomic_rmw a let is_load_or_store a = is_load a || is_store a let is_read a = is_load a || is_atomic_load a || is_atomic_rmw a let is_write a = is_store a || is_atomic_store a || is_atomic_rmw a let is_acquire a = match memory_order_of a with Some Mo_acquire -> is_read a || is_fence a | Some Mo_acq_rel -> is_read a || is_fence a | Some Mo_seq_cst -> is_read a || is_fence a | Some Mo_consume -> is_fence a | None -> is_lock a | _ -> false end let is_consume a = is_read a && (memory_order_of a = Some Mo_consume) let is_release a = match memory_order_of a with Some Mo_release -> is_write a || is_fence a | Some Mo_acq_rel -> is_write a || is_fence a | Some Mo_seq_cst -> is_write a || is_fence a | None -> is_unlock a | _ -> false end let is_seq_cst a = (memory_order_of a = Some Mo_seq_cst) (**************************************** *) type location_kind = Mutex | Non_atomic | Atomic let actions_respect_location_kinds actions lk = forall (a IN actions). match location_of a with Some l -> match lk l with Mutex -> is_lock_or_unlock a | Non_atomic -> is_load_or_store a | Atomic -> is_load_or_store a || is_atomic_action a || is_blocked_rmw a end | None -> true end let is_at_location_kind lk a lk0 = match location_of a with Some l -> (lk l = lk0) | None -> false end let is_at_mutex_location lk a = is_at_location_kind lk a Mutex let is_at_non_atomic_location lk a = is_at_location_kind lk a Non_atomic let is_at_atomic_location lk a = is_at_location_kind lk a Atomic (**************************************** *) let same_thread a b = (thread_id_of a = thread_id_of b) let threadwise_relation_over s rel = relation_over s rel && (forall (x IN rel). same_thread (fst x) (snd x)) let same_location a b = (location_of a = location_of b) let locations_of actions = { l | forall (Some l IN { (location_of a) | forall (a IN actions) | true }) | true} let well_formed_action a = match a with Atomic_load _ _ mem_ord _ _ -> mem_ord = Mo_relaxed || mem_ord = Mo_acquire || mem_ord = Mo_seq_cst || mem_ord = Mo_consume | Atomic_store _ _ mem_ord _ _ -> mem_ord = Mo_relaxed || mem_ord = Mo_release || mem_ord = Mo_seq_cst | Atomic_rmw _ _ mem_ord _ _ _ -> mem_ord = Mo_relaxed || mem_ord = Mo_release || mem_ord = Mo_acquire || mem_ord = Mo_acq_rel || mem_ord = Mo_seq_cst || mem_ord = Mo_consume | _ -> true end (*********************************************** *) (*********************************************** *) (*********************************************** *) let well_formed_threads actions threads lk sb asw dd cd = inj_on action_id_of (actions) && (forall (a IN actions). well_formed_action a) && threadwise_relation_over actions sb && threadwise_relation_over actions dd && threadwise_relation_over actions cd && strict_preorder actions sb && strict_preorder actions dd && strict_preorder actions cd && (forall (a IN actions). thread_id_of a IN threads) && actions_respect_location_kinds actions lk && dd subset sb && relation_over actions asw && (forall (a IN actions). (is_blocked_rmw a || is_blocked_lock a) --> not (exist (b IN actions). (a,b) IN sb)) let consistent_locks actions lo hb = let mutex_actions = {a | forall (a IN actions) | (is_lock a || is_unlock a)} in let lo_happens_before = restrict_relation_set hb mutex_actions in strict_total_order_over mutex_actions lo && lo_happens_before subset lo && (forall ((a,c) IN lo). is_successful_lock a && is_successful_lock c && same_location a c --> (exist (b IN actions). same_location a b && is_unlock b && (a,b) IN lo && (b,c) IN lo)) let well_formed_reads_from_mapping actions lk rf = relation_over actions rf && ( forall (a1 IN actions) (a2 IN actions) (b IN actions). ((a1,b) IN rf && (a2,b) IN rf) --> (a1 = a2) ) && ( forall (a IN actions) (b IN actions). (a,b) IN rf --> same_location a b && ( value_read_by b = value_written_by a ) && not (a = b) && not (is_fence a) && not (is_fence b) && ( is_at_mutex_location lk a --> false ) && ( is_at_non_atomic_location lk a --> is_store a && is_load b ) && ( is_at_atomic_location lk a --> (is_atomic_store a || is_atomic_rmw a || is_store a) && (is_atomic_load b || is_atomic_rmw b || is_load b) ) ) let rs_element rs_head a = same_thread a rs_head || is_atomic_rmw a let release_sequence actions lk mo a_rel b = is_at_atomic_location lk b && is_release a_rel && ( (b = a_rel) || ( rs_element a_rel b && (a_rel,b) IN mo && (forall (c IN actions). ((a_rel,c) IN mo && (c,b) IN mo) --> rs_element a_rel c) ) ) let release_sequence_set actions lk mo = { (a,b) | forall (a IN actions) (b IN actions) | release_sequence actions lk mo a b} let hypothetical_release_sequence actions lk mo a b = is_at_atomic_location lk b && ( (b = a) || ( rs_element a b && (a,b) IN mo && (forall (c IN actions). ((a,c) IN mo && (c,b) IN mo) --> rs_element a c) ) ) let hypothetical_release_sequence_set actions lk mo = { (a,b) | forall (a IN actions) (b IN actions) | hypothetical_release_sequence actions lk mo a b} let synchronizes_with actions sb asw rf lo rs hrs a b = (* thread sync *) (a,b) IN asw || ( same_location a b && a IN actions && b IN actions && ( (* mutex sync *) (is_unlock a && is_successful_lock b && (a,b) IN lo) || (* rel/acq sync *) ( is_release a && is_acquire b && not (same_thread a b) && (exist (c IN actions). (a,c) IN rs && (c,b) IN rf ) ) || (* fence sync *) ( not (same_thread a b) && is_fence a && is_release a && is_fence b && is_acquire b && ( exist (x IN actions) (y IN actions). same_location x y && is_atomic_action x && is_atomic_action y && is_write x && (a,x) IN sb && (y,b) IN sb && ( exist (z IN actions). (x,z) IN hrs && (z,y) IN rf) ) ) || ( not (same_thread a b) && is_fence a && is_release a && is_atomic_action b && is_acquire b && ( exist (x IN actions). same_location x b && is_atomic_action x && is_write x && (a,x) IN sb && ( exist (z IN actions). (x,z) IN hrs && (z,b) IN rf ) ) ) || ( not (same_thread a b) && is_atomic_action a && is_release a && is_fence b && is_acquire b && ( exist (x IN actions). same_location a x && is_atomic_action x && (x,b) IN sb && ( exist (z IN actions). (a,z) IN rs && (z,x) IN rf ) ) ) ) ) let synchronizes_with_set actions sb asw rf lo rs hrs = { (a,b) | forall (a IN actions) (b IN actions) | synchronizes_with actions sb asw rf lo rs hrs a b} let carries_a_dependency_to_set actions sb dd rf = tc ( (rf inter sb) union dd ) let dependency_ordered_before actions rf rs cad a d = a IN actions && d IN actions && ( exist (b IN actions). is_release a && is_consume b && (exist (e IN actions). (a,e) IN rs && (e,b) IN rf) && ( (b,d) IN cad || (b = d) ) ) let dependency_ordered_before_set actions rf rs cad = { (a,b) | forall (a IN actions) (b IN actions) | dependency_ordered_before actions rf rs cad a b} let compose R1 R2 = { (w,z) | forall ((w,x) IN R1) ((y,z) IN R2) | (x = y) } let inter_thread_happens_before actions sb sw dob = let r = sw union dob union (compose sw sb) in tc (r union (compose sb r)) let consistent_inter_thread_happens_before actions ithb = irrefl actions ithb let happens_before actions sb ithb = sb union ithb let all_sc_actions actions = {a | forall (a IN actions) | is_seq_cst a || is_lock a || is_unlock a} let consistent_sc_order actions mo sc hb = let sc_happens_before = restrict_relation_set hb (all_sc_actions actions) in let sc_mod_order = restrict_relation_set mo (all_sc_actions actions) in strict_total_order_over (all_sc_actions actions) sc && sc_happens_before subset sc && sc_mod_order subset sc let consistent_modification_order actions lk sb mo hb = (forall (a IN actions) (b IN actions). (a,b) IN mo --> (same_location a b && is_write a && is_write b)) && ( forall (l IN locations_of actions). match lk l with Atomic -> ( let actions_at_l = {a | forall (a IN actions) | location_of a = Some l} in let writes_at_l = {a | forall (a IN actions_at_l) | is_write a} in strict_total_order_over writes_at_l (restrict_relation_set mo actions_at_l) && (* hb is a subset of mo at l *) restrict_relation_set hb writes_at_l subset mo ) | _ -> ( let actions_at_l = {a | forall (a IN actions) | location_of a = Some l} in Set.is_empty (restrict_relation_set mo actions_at_l) ) end ) let visible_side_effect actions hb a b = (a,b) IN hb && is_write a && is_read b && same_location a b && not ( exist (c IN actions). not (c = a) && not (c = b) && is_write c && same_location c b && (a,c) IN hb && (c,b) IN hb) let visible_side_effect_set actions sb hb = { (a,b) | forall ((a,b) IN hb) | visible_side_effect actions hb a b} let visible_sequence_of_side_effects_tail actions mo hb vsse_head b = { c | forall (c IN actions) | (vsse_head,c) IN mo && not ((b,c) IN hb) && ( forall (a IN actions). ((vsse_head,a) IN mo && (a,c) IN mo) --> not ((b,a) IN hb) ) } let visible_sequence_of_side_effects actions lk mo hb vsse_head b = (b , if is_at_atomic_location lk b then {vsse_head} union visible_sequence_of_side_effects_tail actions mo hb vsse_head b else {}) let visible_sequences_of_side_effects_set actions lk mo hb vse = { visible_sequence_of_side_effects actions lk mo hb vsse_head b | forall (vsse_head IN actions) (b IN actions) | is_at_atomic_location lk b && is_read b && ((vsse_head,b) IN vse) } let consistent_non_atomic_read_values actions lk rf vse = forall (b IN actions). (is_read b && is_at_non_atomic_location lk b) --> ( if (exist (a_vse IN actions). (a_vse,b) IN vse) then (exist (a_vse IN actions). (a_vse,b) IN vse && (a_vse,b) IN rf) else not (exist (a IN actions). (a,b) IN rf) ) let consistent_atomic_read_values actions lk rf vsses = forall (b IN actions). (is_read b && is_at_atomic_location lk b) --> ( if (exist ((b',v) IN vsses). b = b') then ( exist ((b',v) IN vsses). b = b' && (exist (c IN v). (c,b) IN rf) ) else not (exist (a IN actions). (a,b) IN rf) ) let coherent_memory_use actions lk rf mo hb = (* CoRR *) ( forall ((x,a) IN rf) ((y,b) IN rf). ((a,b) IN hb && same_location a b && is_at_atomic_location lk b) --> ((x = y) || (x,y) IN mo) ) && (* CoWR *) ( forall ((a,b) IN hb) (c IN actions). ((c,b) IN rf && is_write a && same_location a b && is_at_atomic_location lk b) --> ((c = a) || (a,c) IN mo) ) && (* CoRW *) ( forall ((a,b) IN hb) (c IN actions). ((c,a) IN rf && is_write b && same_location a b && is_at_atomic_location lk a) --> ((c,b) IN mo) ) let rmw_atomicity actions rf mo = forall ((a,b) IN rf). is_atomic_rmw b --> adjacent_less_than mo actions a b let sc_reads_restricted actions rf sc mo hb = forall ((a,b) IN rf). is_seq_cst b --> ( adjacent_less_than_such_that (fun c -> is_write c && same_location b c) sc actions a b ) || ( not (is_seq_cst a) && ( forall (x IN actions). (adjacent_less_than_such_that (fun c -> is_write c && same_location b c) sc actions x b) --> not ((a,x) IN hb) ) ) let sc_fences_heeded actions sb rf sc mo = (* fence restriction N3291 29.3p4 *) ( forall (a IN actions) ((x,b) IN sb) (y IN actions). ( is_write a && is_fence x && adjacent_less_than sc actions a x && is_atomic_action b && same_location a b && (y,b) IN rf) --> ((y = a) || (a,y) IN mo) ) && (* fence restriction N3291 29.3p5 *) ( forall ((a,x) IN sb) ((y,b) IN rf). ((is_atomic_action a && is_write a && is_fence x && is_atomic_action b && (x,b) IN sc && same_location a b) --> ((y = a) || (a,y) IN mo) ) ) && (* fence restriction N3291 29.3p6 *) ( forall ((a,x) IN sb) ((y,b) IN sb) (z IN actions). ( is_atomic_action a && is_write a && is_fence x && is_fence y && (x,y) IN sc && is_atomic_action b && same_location a b && (z,b) IN rf) --> ((z = a) || (a,z) IN mo) ) && (* SC fences impose mo N3291 29.3p7 *) ( forall ((a,x) IN sb) ((y,b) IN sb). ( is_atomic_action a && is_write a && is_atomic_action b && is_write b && is_fence x && is_fence y && (x,y) IN sc && same_location a b --> (a,b) IN mo) ) && (* SC fences impose mo N3291 29.3p7, w collapsed first write*) ( forall (a IN actions) ((y,b) IN sb). ( is_atomic_action a && is_write a && is_fence y && (a,y) IN sc && is_atomic_action b && is_write b && same_location a b --> (a,b) IN mo) ) && (* SC fences impose mo N3291 29.3p7, w collapsed second write*) ( forall ((a,x) IN sb) (b IN actions). ( is_atomic_action a && is_write a && is_fence x && is_atomic_action b && is_write b && (x,b) IN sc && same_location a b --> (a,b) IN mo) ) let consistent_reads_from_mapping actions lk sb rf sc mo hb vse vsses = consistent_non_atomic_read_values actions lk rf vse && consistent_atomic_read_values actions lk rf vsses && coherent_memory_use actions lk rf mo hb && rmw_atomicity actions rf mo && sc_reads_restricted actions rf sc mo hb && sc_fences_heeded actions sb rf sc mo let all_data_dependency_of actions rf cad = tc (rf union cad) let consistent_control_dependency actions threads lk sb asw dd cd rf cad = irrefl (tc (cd union all_data_dependency_of actions rf cad)) let consistent_execution actions threads lk sb asw dd cd rf mo sc lo = well_formed_threads actions threads lk sb asw dd cd && ( let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = synchronizes_with_set actions sb asw rf lo rs hrs in let cad = carries_a_dependency_to_set actions sb dd rf in let dob = dependency_ordered_before_set actions rf rs cad in let ithb = inter_thread_happens_before actions sb sw dob in let hb = happens_before actions sb ithb in let vse = visible_side_effect_set actions sb hb in let vsses = visible_sequences_of_side_effects_set actions lk mo hb vse in consistent_locks actions lo hb && consistent_inter_thread_happens_before actions ithb && consistent_sc_order actions mo sc hb && consistent_modification_order actions lk sb mo hb && well_formed_reads_from_mapping actions lk rf && consistent_reads_from_mapping actions lk sb rf sc mo hb vse vsses) let indeterminate_reads actions rf = {b | forall (b IN actions) | is_read b && not (exist (a IN actions). (a,b) IN rf)} let unsequenced_races actions sb = { (a,b) | forall (a IN actions) (b IN actions) | not (a = b) && same_location a b && (is_write a || is_write b) && same_thread a b && not ((a,b) IN sb || (b,a) IN sb) } let data_races actions hb = { (a,b) | forall (a IN actions) (b IN actions) | not (a = b) && same_location a b && (is_write a || is_write b) && not (same_thread a b) && not (is_atomic_action a && is_atomic_action b) && not ((a,b) IN hb || (b,a) IN hb) } let data_races' actions threads lk sb asw dd cd rf mo sc lo = let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = synchronizes_with_set actions sb asw rf lo rs hrs in let cad = carries_a_dependency_to_set actions sb dd rf in let dob = dependency_ordered_before_set actions rf rs cad in let ithb = inter_thread_happens_before actions sb sw dob in let hb = happens_before actions sb ithb in data_races actions hb let good_mutex_use actions lk sb lo a = let mutexes_at_l = {a' | forall (a' IN actions) | (is_successful_lock a' || is_unlock a') && (location_of a' = location_of a)} in let lock_order = restrict_relation_set lo mutexes_at_l in (* violated requirement: The calling thread shall own the mutex. *) ( is_unlock a --> ( exist (al IN actions). is_successful_lock al && (location_of al = location_of a) && (al,a) IN sb && adjacent_less_than lock_order actions al a ) ) && (* violated requirement: The calling thread does not own the mutex. *) ( is_lock a --> not ( exist (al IN actions). is_successful_lock al && (location_of a = location_of al) && same_thread a al && adjacent_less_than lock_order actions al a ) ) let bad_mutexes actions lk sb lo = { a | forall (a IN actions) | not (good_mutex_use actions lk sb lo a)} (*********************************************** *) (*********************************************** *) (*********************************************** *) (* SECTION *) (* model with less vsse's *) let no_vsse_consistent_atomic_read_values actions lk rf hb vse = (* need to be careful that we cant read from a write that the read happens before *) forall (b IN actions). (is_read b && is_at_atomic_location lk b) --> ( if (exist (a_vse IN actions). (a_vse,b) IN vse) then (exist (a IN actions). ((a,b) IN rf) && not ((b,a) IN hb)) else not (exist (a IN actions). (a,b) IN rf) ) let no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse = consistent_non_atomic_read_values actions lk rf vse && no_vsse_consistent_atomic_read_values actions lk rf hb vse && coherent_memory_use actions lk rf mo hb && rmw_atomicity actions rf mo && sc_reads_restricted actions rf sc mo hb && sc_fences_heeded actions sb rf sc mo let no_vsse_consistent_execution actions threads lk sb asw dd cd rf mo sc lo = well_formed_threads actions threads lk sb asw dd cd && ( let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = synchronizes_with_set actions sb asw rf lo rs hrs in let cad = carries_a_dependency_to_set actions sb dd rf in let dob = dependency_ordered_before_set actions rf rs cad in let ithb = inter_thread_happens_before actions sb sw dob in let hb = happens_before actions sb ithb in let vse = visible_side_effect_set actions sb hb in consistent_locks actions lo hb && consistent_inter_thread_happens_before actions ithb && consistent_sc_order actions mo sc hb && consistent_modification_order actions lk sb mo hb && no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse && well_formed_reads_from_mapping actions lk rf ) (*********************************************** *) (*********************************************** *) (*********************************************** *) (* SECTION *) (* model with seperate per-location lock orders *) let multi_lo_consistent_locks actions lk lo hb = let mutex_actions = {a | forall (a IN actions) | (is_lock a || is_unlock a)} in let lo_happens_before = restrict_relation_set hb mutex_actions in lo_happens_before subset lo && (forall ((a,c) IN lo). is_successful_lock a && is_successful_lock c && same_location a c --> (exist (b IN actions). same_location a b && is_unlock b && (a,b) IN lo && (b,c) IN lo)) && forall (l IN locations_of actions). let actions_at_l = {a | forall (a IN actions) | location_of a = Some l} in match lk l with Mutex -> strict_total_order_over actions_at_l (restrict_relation_set lo actions_at_l) | _ -> Set.is_empty (restrict_relation_set lo actions_at_l) end let no_vsse_multi_lo_consistent_execution actions threads lk sb asw dd cd rf mo sc lo = well_formed_threads actions threads lk sb asw dd cd && ( let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = synchronizes_with_set actions sb asw rf lo rs hrs in let cad = carries_a_dependency_to_set actions sb dd rf in let dob = dependency_ordered_before_set actions rf rs cad in let ithb = inter_thread_happens_before actions sb sw dob in let hb = happens_before actions sb ithb in let vse = visible_side_effect_set actions sb hb in multi_lo_consistent_locks actions lk lo hb && consistent_inter_thread_happens_before actions ithb && consistent_sc_order actions mo sc hb && consistent_modification_order actions lk sb mo hb && no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse && well_formed_reads_from_mapping actions lk rf ) (*********************************************** *) (*********************************************** *) (*********************************************** *) (* SECTION *) (* single mutex synchronization step *) let lo_single_synchronizes_with actions sb asw rf lo rs hrs a b = (* thread sync *) (a,b) IN asw || ( same_location a b && a IN actions && b IN actions && ( (* mutex sync *) (is_unlock a && is_successful_lock b && (a,b) IN lo && not (exist (c IN actions). (a,c) IN lo && (c,b) IN lo)) || (* rel/acq sync *) ( is_release a && is_acquire b && not (same_thread a b) && (exist (c IN actions). (a,c) IN rs && (c,b) IN rf ) ) || (* fence sync *) ( not (same_thread a b) && is_fence a && is_release a && is_fence b && is_acquire b && ( exist (x IN actions) (y IN actions). same_location x y && is_atomic_action x && is_atomic_action y && is_write x && (a,x) IN sb && (y,b) IN sb && ( exist (z IN actions). (x,z) IN hrs && (z,y) IN rf) ) ) || ( not (same_thread a b) && is_fence a && is_release a && is_atomic_action b && is_acquire b && ( exist (x IN actions). same_location x b && is_atomic_action x && is_write x && (a,x) IN sb && ( exist (z IN actions). (x,z) IN hrs && (z,b) IN rf ) ) ) || ( not (same_thread a b) && is_atomic_action a && is_release a && is_fence b && is_acquire b && ( exist (x IN actions). same_location a x && is_atomic_action x && (x,b) IN sb && ( exist (z IN actions). (a,z) IN rs && (z,x) IN rf ) ) ) ) ) let lo_single_synchronizes_with_set actions sb asw rf lo rs hrs = { (a,b) | forall (a IN actions) (b IN actions) | lo_single_synchronizes_with actions sb asw rf lo rs hrs a b} let no_vsse_multi_lo_single_sw_consistent_execution actions threads lk sb asw dd cd rf mo sc lo = well_formed_threads actions threads lk sb asw dd cd && ( let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = lo_single_synchronizes_with_set actions sb asw rf lo rs hrs in let cad = carries_a_dependency_to_set actions sb dd rf in let dob = dependency_ordered_before_set actions rf rs cad in let ithb = inter_thread_happens_before actions sb sw dob in let hb = happens_before actions sb ithb in let vse = visible_side_effect_set actions sb hb in multi_lo_consistent_locks actions lk lo hb && consistent_inter_thread_happens_before actions ithb && consistent_sc_order actions mo sc hb && consistent_modification_order actions lk sb mo hb && no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse && well_formed_reads_from_mapping actions lk rf ) let los_single_sw_data_races' actions threads lk sb asw dd cd rf mo sc lo = let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = lo_single_synchronizes_with_set actions sb asw rf lo rs hrs in let cad = carries_a_dependency_to_set actions sb dd rf in let dob = dependency_ordered_before_set actions rf rs cad in let ithb = inter_thread_happens_before actions sb sw dob in let hb = happens_before actions sb ithb in data_races actions hb (*********************************************** *) (*********************************************** *) (*********************************************** *) (* SECTION *) (* model without consume *) (* check there are no consume actions *) let no_vsse_consume_happens_before actions sb sw = tc (sb union sw) let no_vsse_consume_consistent_happens_before actions hb = irrefl actions hb let no_vsse_consume_consistent_execution actions threads lk sb asw dd cd rf mo sc lo = well_formed_threads actions threads lk sb asw dd cd && ( let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = synchronizes_with_set actions sb asw rf lo rs hrs in let hb = no_vsse_consume_happens_before actions sb sw in let vse = visible_side_effect_set actions sb hb in consistent_locks actions lo hb && no_vsse_consume_consistent_happens_before actions hb && consistent_sc_order actions mo sc hb && consistent_modification_order actions lk sb mo hb && no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse && well_formed_reads_from_mapping actions lk rf ) let no_vsse_consume_data_races' actions threads lk sb asw dd cd rf mo sc lo = let rs = release_sequence_set actions lk mo in let hrs = hypothetical_release_sequence_set actions lk mo in let sw = synchronizes_with_set actions sb asw rf lo rs hrs in let hb = no_vsse_consume_happens_before actions sb sw in data_races actions hb (*********************************************** *) (*********************************************** *) (*********************************************** *) (* SECTION *) (* model without relaxed *) (* Without relaxed, can release sequences go? Unfortunately not. This model is NOT equvalent. *) let no_vsse_consume_relaxed_synchronizes_with actions sb asw rf sc lo a b = (* thread sync *) (a,b) IN asw || ( same_location a b && a IN actions && b IN actions && ( (* mutex sync *) (is_unlock a && is_lock b && (a,b) IN lo) || (* rel/acq sync *) ( is_release a && is_acquire b && not (same_thread a b) && (a,b) IN rf ) ) ) let no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc lo = { (a,b) | forall (a IN actions) (b IN actions) | no_vsse_consume_relaxed_synchronizes_with actions sb asw rf sc lo a b} let no_vsse_consume_relaxed_consistent_execution actions threads lk sb asw dd cd rf mo sc lo = well_formed_threads actions threads lk sb asw dd cd && ( let sw = no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc lo in let hb = no_vsse_consume_happens_before actions sb sw in let vse = visible_side_effect_set actions sb hb in consistent_locks actions lo hb && no_vsse_consume_consistent_happens_before actions hb && consistent_sc_order actions mo sc hb && consistent_modification_order actions lk sb mo hb && no_vsse_consistent_reads_from_mapping actions lk sb rf sc mo hb vse && well_formed_reads_from_mapping actions lk rf ) let no_vsse_consume_relaxed_data_races' actions threads lk sb asw dd cd rf mo sc lo = let sw = no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf sc lo in let hb = no_vsse_consume_happens_before actions sb sw in data_races actions hb (*********************************************** *) (*********************************************** *) (*********************************************** *) (* SECTION *) (* model for SC only *) let consistent_total_order actions sb asw tot = strict_total_order_over actions tot && sb subset tot && asw subset tot let tot_consistent_reads_from_mapping actions lk rf tot = (forall (b IN actions). (is_read b) --> ( let writes_at_same_location = { a | forall (a IN actions) | (same_location a b) && is_write a} in ( if (exist (a IN actions). adjacent_less_than (restrict_relation_set tot (writes_at_same_location union {b})) actions a b) then (exist (a IN actions). ((a,b) IN rf) && adjacent_less_than (restrict_relation_set tot (writes_at_same_location union {b})) actions a b) else not (exist (a IN actions). (a,b) IN rf) ) ) ) let tot_consistent_execution actions threads lk sb asw dd cd rf tot = let lo = restrict_relation_set tot { a | forall (a IN actions) | is_lock a || is_unlock a } in well_formed_threads actions threads lk sb asw dd cd && consistent_total_order actions sb asw tot && tot_consistent_reads_from_mapping actions lk rf tot && well_formed_reads_from_mapping actions lk rf let tot_hb_data_races actions sb asw rf tot = let sc = tot inter { (a,b) | forall (a IN actions) (b IN actions) | is_seq_cst a && is_seq_cst b} in let mo = tot inter { (a,b) | forall (a IN actions) (b IN actions) | (same_location a b) && is_write a && is_write b} in let sw = no_vsse_consume_relaxed_synchronizes_with_set actions sb asw rf tot tot in let hb = no_vsse_consume_happens_before actions sb sw in data_races actions hb let tot_data_races actions tot = { (a,b) | forall (a IN actions) (b IN actions) | not (a = b) && same_location a b && (is_write a || is_write b) && not (same_thread a b) && not (is_atomic_action a && is_atomic_action b) && (adjacent_less_than tot actions a b || adjacent_less_than tot actions b a) } (* Two memory operations conflict if they access the same memory location, and at least one of them is a store, atomic store, or atomic read-modify-write operation. In a sequentially consistent execution, two memory operations from different threads form a type 1 data race if they conflict, at least one of them is a data operation, and they are adjacent in