<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
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


*)