<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 Sc_statement

val maximal_elements : forall 'a. 'a set -> ('a * 'a) set -> 'a set

(* This file follows the style of c_add_read.lem. Instead of the
restricted model in that proof, which lacks atomic read modify writes,
this applies to a restricted model that has rmw's but lacks
non-seq-cst atomics *)

(* 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 c_tids o_ac rf_ac mo_ac sc_ac

(* suppose further that r is maximal in sequenced before. *)
let _ = r IN maximal_elements acr o_acr.sb

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 hb_acr = build_hb acr o_acr rf_ac mo_ac sc_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_at_atomic_location o_acr.lk 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 mo_acr' =
      if is_atomic_rmw r then
        mo_ac union { (a,r') | forall (a IN ac) | is_write a && same_location a r' }
      else
        mo_ac
    in
    let hb_acr' = build_hb acr' o_acr' rf_acr' mo_acr' sc_acr' 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 relationship *)
      (forall ((a,b) IN hb_acr' \ reln_subst hb_acr r' r). 
         b = r' &&
         (exist a' w w'.
            (a = w || (a,w) IN hb_acr') && 
            (w = w' || (w,w') IN mo_acr') && 
            (is_atomic_action r && w' = Set.choose candidate_writes))) &&
      (* And the new execution is consistent *)
      consistent_ex acr' c_tids 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 mo_acr' =
  if is_atomic_rmw r then
    mo_ac union { (a,r') | forall (a IN ac) | is_write a && same_location a r' }
  else
    mo_ac

let hb_acr' = build_hb acr' o_acr' rf_acr' mo_acr'

(* 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 hb is by adding to the
synchronizes-with relation. 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 hb dependency on r.

To add synchronizes with, r' must be seq_cst atomic, and by the
initial assumptions is o_acr'.sb maximal. If r' is not a read modify
write, then it has no hb successors and we are done. If it is a RMW,
then if there were a sucessor it would have to be a seq_cst atomic
read to synchronize with r'. This read is in the consistent execution
of ac and has not changed so cannot possibly read from r'.  Hence, r'
has no hb successors.

Note that this argument also guarantees that r' is maximal in hb_acr'.

Now we must check that the execution is consistent

We have well_formed_threads over acr, and altering a read value
doesn't affect that, so we have well_formed_threads.

We are adding a read, so the locks remain precisely the same as in the
ac case. Consistent_locks in the acr' case follows from consistency in
the ac case.

no_vsse_consume_consistent_happens_before follows from r' being maximal in
hb_acr'.

consistent_sc_order follows because (if it is SC) r' is maximal in mo_acr',
hb_acr' and sc_acr'.

consistent_modification_order follows because in the atomic seq_cst RMW case, 
r' is maximal in mo_acr', hb_acr' and sc_acr'. Any other sort of r' affects
nothing regarding the writes (by the hb restriction fact we have just proved).

well_formed_reads_from_mapping follows by construction.

consistent_non_atomic_read_values is true by construction.

no_vsse_consistent_atomic_read_values follows from the fact that r' is hb_acr' maximal.

For coherent_memory_use, there are three cases, CoRR, CoWR and CoRW.
The CoRW case doesn't apply to r' because it is hb_acr' maximal.  CoRR
and CoWR follow by construction (r' reads an mo_ac maximal write).

rmw_atomicity, sc_reads_restricted and sc_fences_heeded all follow by
construction (r' reads an mo_ac maximal write).

*)