open Atomic open Statement (* In this file, we show that a read can be added to a consistent execution to get a new consistent execution (under some further conditions) *) (* Suppose we have some well formed threads *) val acr : c_action set val c_tids : c_thread_id set val o_acr : opinfo let _ = well_formed_threads acr c_tids o_acr.lk o_acr.sb o_acr.asw o_acr.dd o_acr.cd (* and for some read r, the execution is consistent without it *) val ac : c_action set val r : c_action let _ = c_is_read r let _ = acr = ac union {r} && not (r IN ac) let o_ac = restrict_opinfo o_acr ac val rf_ac : c_action reln val mo_ac : c_action reln val sc_ac : c_action reln let _ = consistent_ex ac o_ac rf_ac mo_ac sc_ac (* suppose further that r is maximal in dependency order, and if acquire or sequentially consistent that it is also maximal in sequenced-before, and there is no sc or release or same_location action following in sb *) let _ = r IN maximal_elements acr (tc (o_acr.dd union o_acr.cd)) let _ = (is_seq_cst r || is_acquire r) --> r IN maximal_elements acr o_acr.sb let _ = forall ((r,a) IN o_acr.sb). not (is_seq_cst r) && not (is_release r) && not (same_location r a) let hb_ac = build_hb ac o_ac rf_ac mo_ac (* Note that we define hb_acr with respect to rf_ac and not rf_acr *) let ithb_acr = build_ithb acr o_acr rf_ac mo_ac let hb_acr = build_hb acr o_acr rf_ac mo_ac let vse_acr = { w | visible_side_effect acr hb_acr w r } (* then, there exists a read r', with possibly a different value read, that can be consistently appended to the candidate execution. *) let candidate_writes = if is_atomic_action r && vse_acr <> {} then maximal_elements { w | forall (w IN acr) | is_write w && same_location w r } mo_ac else vse_acr let _ = exist (r' IN all_values r). let acr' = ac union {r'} in let o_acr' = subst_opinfo o_acr r' r in let rf_acr' = if candidate_writes = {} then rf_ac else rf_ac union { (Set.choose candidate_writes, r') } in let sc_acr' = if is_seq_cst r then sc_ac union { (a,r') | forall (a IN ac) | is_seq_cst a } else sc_ac in let hb_acr' = build_hb acr' o_acr' rf_acr' mo_ac in let ithb_acr' = build_ithb acr' o_acr' rf_acr' mo_ac in (* Adding the new rf doesn't remove any hb dependency *) reln_subst hb_acr r' r subset hb_acr' && (* And any new hb dependency caused by the rf is to the rf through a new synchronizes with, or dependency ordered before relationship *) (forall ((a,b) IN hb_acr' \ reln_subst hb_acr r' r). b = r' && (exist a' w w'. (a = a' || (a,a') IN ithb_acr) && ((a' = w) || (a',w) IN o_acr'.sb) && (w = w' || (w,w') IN mo_ac) && is_release w && (* w' is in a release sequence headed by w *) (is_atomic_action r && w' = Set.choose candidate_writes || (exist a' w w' r'' w''. (w',r'') IN rf_ac && (r'',w'') IN carries_a_dependency_to_set ac o_ac.sb o_ac.dd rf_ac && w'' = Set.choose candidate_writes)))) && (* And the new execution is consistent *) consistent_ex acr' o_acr' rf_acr' mo_ac sc_acr' (* Proof: *) (* Choose r' such that it is the same as r, but reads a value of written by some write in candidate_writes. Thus we have *) val r' : c_action let acr' = ac union {r'} let o_acr' = subst_opinfo o_acr r' r let rf_acr' = if candidate_writes = {} then rf_ac else rf_ac union { (Set.choose candidate_writes, r') } let sc_acr' = if is_seq_cst r then sc_ac union { (a,r') | forall (a IN ac) | is_seq_cst a } else sc_ac let hb_acr' = build_hb acr' o_acr' rf_acr' mo_ac (* The first conclusion is trivial, since adding to the rfmap can only add happens-before dependencies. To prove the second conclusion, note that the only way the addition of r' to the reads-from map can change ithb is by adding to the synchronizes-with or dependency-ordered before relations. The second (existential) part of the this conclusion covers the cases where this happens, so we only need to prove the first part, that there is no new ithb dependency on r. To add synchronizes with, r' must be sc or acquire, and by the initial assumptions is o_acr'.sb maximal. Hence, r' has no ithb successors (since r' is not a write either). To add to dependency-ordered before, r' is either consume, or involved in carries-a-dependency-to. In the first case, there can be no ithb successors of r'. If r' is not maximal in o_acr'.sb, then (since r' is not a write) the only successor must arise from an o_acr'.sb successor write that is a sw or dob predecessor of the the purported ithb successor. This write has to be SC or release, contradicting our assumption that r has no such sb successors. By the same reasoning, if the addition of r' extends a carries-a-dependency-to-chain, there can be no data-dependence successors or other inter-thread happens before successors of r'. Note that this argument also guarantees that r' is maximal in ithb_acr' (since r must be maximal in ithb_acr because any sb successors of r must not be release or SC). Now we must check that the execution is consistent consistent_inter_thread_happens_before follows from r' being maximal in ithb_acr'. consistent_sc_order follows because (if it is SC) r' is maximal in both ithb_acr' and SC order and by assumption it is maximal in sequenced before, and hence is maximal in happens before. consistent_modification_order_simple follows because the addition of r' affects nothing regarding the writes (by the hb restriction fact we have just proved). well_formed_reads_from_mapping_simple follows by constructions consistent_non_atomic_read_values no_vsse_consistent_atomic_read_values coherent_memory_use sc_reads_restricted Candidate_writes is constructed so that each of these must hold, relative to hb_acr: here we need to show that they hold relative to hb_acr'. The only cases that are not immediate from the maximality of r' in ithb_acr', the first (subset) conclusion above, and the fact that there are no sb-successors of r' on the same location are: 1) (from consistent_non_atomic_read_values) w --hb_acr'--> w' --hb_acr'--> r' | ^ |------------rf_acr'-----------| We know that w' --ithb_acr--> a' --sb--> w'' --mo_ac--> w --rf_acr'--> r' or w' --ithb_acr--> a' --sb--> w'' --mo_ac--> w --rf_acr'--> r'' --cad_to--> w --rf_acr'--> r' In the latter case, w'--ithb_acr-->w, a contradiction. In the former, it must be that w' --mo_ac--> w, a contradiction. 2) (from coherent_memory_use) w --mo_ac--> w' --hb_acr'--> r' | ^ |----------rf_acr'-----------| Contradicts the choice of w as maximal in mo_ac 3) (from coherent_memory_use) w ----mo_ac---> w' | | rf_acr' rf_acr' | | v v r' <--hb_acr'-- r'' Contradicts the choice of w as maximal in mo_ac *)