<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 MachineDefTypes
open Atomic
open Intermediate_actions
open Statement

(* Let comp be a threadwise_good_compiler and let c_prog be drf. *)
val comp : c_program -> p_program * p_thread_id set
val c_prog : c_program

let _ = threadwise_good_compiler comp
let _ = drf c_prog

let (power_prog, p_tids) = comp c_prog

(* Let t be in machine_executions p tids. *)

val t : trace
let _ = t IN machine_executions power_prog p_tids

(* By threadwise_good_compiler, we have: *)

val actions : c_action set
val c_tids : c_thread_id set
val o : opinfo
val rf : c_action reln

(* such that *)

let _ = obs t actions rf
let _ = (actions, c_tids, o) IN opsem c_prog
let _ = preserved_po t actions o.sb
let _ = preserved_dd t actions o.dd
let _ = preserved_xsync t Hwsync actions
let _ = preserved_xsync t Lwsync actions
let _ = preserved_ctrlisync t actions
let _ = preserved_cd t actions o.cd

(* Let mo be such that *)

val mo : c_action reln
let _ = good_mo t actions o.lk mo

(* Such an mo exists because for each Power address a, trace_to_co is a total
order (by construction), and action_to_i_action is injective. *)

(* Let sc be such that *)

val sc : c_action reln
let _ = good_sc t actions sc

(*
Such an sc exists because build_sc_order.lem proves that 
- trace_to_co t union trace_to_po t union extended_rf union fr
(with extended_rf and fr defined as in good_sc) is acyclic and because
action_to_i_action is injective.  *)


(* Now we case split on *)

let _ = rf_in_hb_condition actions o mo rf

(* If the above holds, then by power_to_consistent_ex.lem (and that opsem
implies opsem_prefix and machine_execution implies machine_execution_prefix)
we have *)

let _ = consistent_ex actions o rf mo sc

(* and we are finished. *)

(* So assume *)

let _ = not (rf_in_hb_condition actions o mo rf)

(* Define an ordering on c_actions following the Power trace *)

val action_order : c_action reln
let action_order =
  { (a,b) 
    | forall (a IN actions) (b IN actions)
    | exist ((a',b') IN trace_to_order t).
        (action_to_i_action a IN image snd (commit_to_inter a')) &&
        (action_to_i_action b IN image snd (commit_to_inter b')) }

let lemma1 = strict_total_order_over actions action_order
(*
Proof:
commit_to_inter is injective as a function from t to its image on t (i.e., no
read or write is committed twice, by the commit rule preconditions). 

Furthermore, action_to_i_action is injective as a function from actions to its
image on actions, and by the initial assumption that actions and t have the same
observable behaviour, the two images are equal.  action_order lifts the
trace order on commit labels through these mappings to actions.
QED
*)

let lemma2 = forall ((a,b) IN rf). (a,b) IN action_order
(*
By rf_to from power_to_consistent_ex.lem 
*) 

let lemma3 = forall ((a,b) IN o.dd). (a,b) IN action_order
(*
By addr+data_to from power_to_consistent_ex.lem 
*) 


let lemma4 = forall ((a,b) IN o.cd). (a,b) IN action_order
(*
By control_dependency_lemma from power_thread_lemmas.lem 
*) 


(* Choose the maximal read r (by action_order) such that the set of all actions
less than r make 3) true (when all of rf_in_hb_condition's arguments are
restricted to this set). Let w be the write that r reads from and let ac
be the set of actions less than r *)

val r : c_action
val w : c_action
let _ = (w,r) IN rf
let ac = { a | (a,r) IN action_order }
let o_ac = restrict_opinfo o ac
let mo_ac = rrestrict mo ac
let rf_ac = rrestrict rf ac
let sc_ac = rrestrict sc ac
let _ = 
  r IN maximal_elements 
         { r | c_is_read r && rf_in_hb_condition ac o_ac mo_ac rf_ac }
         action_order

(* Such an r must exist by Lemmas 1 and 2, by the assumption that
rf_in_hb_condition does not hold for the entire execution, and by the definition
of rf_in_hb_condition *)

(* Thus *)

let _ = rf_in_hb_condition ac o_ac mo_ac rf_ac

(* Let l be the unique read commit label that corresponds to r (as outlined in the
proof of Lemma 1) and let t' be the part of t preceding l.  *)

val l : trans
let _ = action_to_i_action r IN image snd (commit_to_inter l)
val t' : trace

(* then *)

let _ = t' IN machine_execution_prefix power_prog p_tids 
let _ = obs t' ac rf_ac

(* by construction and Lemma 2 *)

(* We need to show the following to apply power_to_consistent_ex.lem and
conclude that ac is a consistent execution *)
let _ = opsem_prefix c_prog ac actions c_tids o
let _ = preserved_po t' ac o_ac.sb
let _ = preserved_dd t' ac o_ac.dd
let _ = preserved_xsync t' Hwsync ac
let _ = preserved_xsync t' Lwsync ac
let _ = preserved_ctrlisync t' ac
let _ = preserved_cd t' ac o_ac.cd
let _ = good_mo t' ac o_ac.lk mo_ac
let _ = good_sc t' ac sc_ac
(*
The first follows from Lemmas 1, 3 and 4.  The rest are straightforward.
*)

(* Now we have *)

let _ = consistent_ex ac o_ac rf_ac mo_ac sc_ac

(* Furthermore, r is maximal in dependency ordering (and in sb if it is SC or
acquire), and r is not followed by any SC, release or same-location actions *)
let acr = ac union {r}
let o_acr = restrict_opinfo o acr
let rf_acr = rrestrict rf acr
let _ = r IN maximal_elements acr (tc (o_ac.dd union o_ac.cd))
let _ = (is_seq_cst r || is_acquire r) --> r IN maximal_elements acr o_ac.sb
let _ = forall ((r,a) IN o_acr.sb). 
          not (is_seq_cst r) && not (is_release r) && not (same_location r a)

(* The first holds because ac is downward closed under  (tc (o_ac.dd union
o_ac.cd)) by the definition of opsem_prefix 

The second holds by no_branch_in_hole_lemma from power_thread_lemmas and
preserved_ctrlisync

The third holds by no_barrier_in_hole_lemma and memory_location_dependency_lemma
from power_thread_lemmas.lem and preserved_xsync.
*)

let hb_acr = build_hb acr o_acr rf_ac mo_ac
let vse_acr = { w | visible_side_effect acr hb_acr w r }
let candidate_writes = 
  if is_atomic_action r && vse_acr <> {} then
    maximal_elements { w | forall (w IN acr) | c_is_write w && same_location w r } mo_ac
  else
    vse_acr

(* Now we apply the c_add_read.lem to add r back (possibly reading a different
value) and get a consistent execution with a data race or indeterminate read) *)

val r' : c_action
let _ = r' IN all_values r

let acr' = ac union {r'}
let o_acr' = subst_opinfo (restrict_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
let ithb_acr' = build_ithb acr' o_acr' rf_acr' mo_ac

let _ = reln_subst hb_acr r' r subset hb_acr'
let _ = 
  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' = 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)))

let _ = consistent_ex acr' o_acr' rf_acr' mo_ac sc_acr'

(* Since r' is a read which doesn't occur in modification order we have *)
let _ = mo_ac = rrestrict mo acr'

(* Now we show that this acr' execution has a data race or indeterminate read.
*)

let _ = data_races acr' hb_acr' <> {} || indeterminate_reads acr' rf_acr' <> {}

(* If r' is atomic, then there is no (w',r') IN hb_acr where w' is to the same
location (since rf_in_hb_condition doesn't hold), and hence candidate_writes =
{}, and r' doesn't read from anything.

If r' is non-atomic, then we have *)

let _ = not ((w,r) IN hb_acr)

(* We also have *)
let _ = not ((r,w) IN hb_acr)
(* By rf_to, hb_POWERshape, and to_lemma of power_to_consistent_ex.lem *)

(* Thus, by the conditions on hb_acr' \ hb_acr, not ((r',w) IN hb_acr') and the
only possible way for (w,r') IN hb_acr' is for 

w --ithb_acr--> a --sb--> b --rs--> c --rf_acr--> d --dd--> w' --sb--> r

where b is a release, and c is in the release sequence headed by b.

This cannot happen on the Power trace.  Here, w --ithb_acr--> w', and we can
employ lemmas from power_to_consistent_ex.lem to show that r cannot read from w:

By ithb_POWERshape and propBefore_write, (w,w') IN propBefore.
By the definition of propBefore, for same-thread reads, (w',r) IN propBefore.
By propBefore2_rf_to, w propagates to r's thread before w' does.

Hence, r cannot have read from w in the original trace.

*)

(* Now we have built a racy consistent execution of acr', we need to add r' to
ac using opsem_add_read_axiom.  We need to know that all actions that r has a
data or control dependency on are already in ac, which Lemmas 3 and 4 guarantee.

This gives new_actions and new_o such that 
*)

val new_o : opinfo
val new_actions : c_action set
val staying_actions : c_action set

let _ = (staying_actions union {r'} union new_actions, c_tids, new_o) IN opsem c_prog

(*
with staying_actions and new_o defined as in the axiom.
*)

(* We now show that acr' is not only a consistent execution with a race, but
also an opsem prefix of some execution of c_prog *)

let _ = opsem_prefix c_prog acr' (staying_actions union {r'} union new_actions) c_tids new_o

(*
Proof of the above:
It suffices that acr' is down closed under (tc (new_o.dd union new_o.cd)).
Let (e,a) IN tc (new_o.dd union new_o.cd) where a IN acr'.  We must show
that e IN acr'.  Proceed by induction on the transitive closure.

Base case:
  (e,a) IN new_o.dd union new_o.cd.  By the axiom's 2nd clause, e NOTIN
new_actions, and so e IN staying_actions union {r'}.  If e IN acr', then we are
done, so we can assume that e IN unchanged_actions.  By the first clause of the
axiom, (e,a) IN o.dd union o.cd (if a <> r') or (e,r) IN o.dd union o.cd (if a =
r').  The second case contradicts the above fact (that allowed us to apply the
axiom) that ac contains all actions that r depends on.  The first contradicts
the fact that ac is down closed under tc (o.dd union o.cd).

Inductive case:
  (e,e') IN tc (new_o.dd union new_o.cd) and 
  (e',a) IN tc (new_o.dd union new_o.cd).
  By inductive hypothesis applied to the second, e' IN acr' and so by the
  inductive hypothesis applied to the first, e IN acr'.
QED

Now we need to add actions until sb down closed (while keeping the race).  Any
such missing action is in staying_actions.  We will repeatedly pick an sb
minimal one to add.

If it is a read, follow the above plan, to apply c_add_read.lem.  Because the
read has an SB successor already in the execution, we need that is isn't release
or acquire or to the same location as one of those SB successors.  As above,
this follows by no_branch_in_hole_lemma, no_barrier_in_hole_lemma,
memory_location_dependency_lemma, and preserved_ctrlisync and preserved_xsync.
We can apply the latter two because the staying actions are all present in the
original trace.  The race is preserved because the added read is maximal in
ithb.

We rely on the opsem_read_axiom to ensure that we can always still do actions
that have no dependency on reads whose value we change, and we rely on the Power
speculation mechanism to ensure that we have no dependencies on the sb-missing
actions.

If it is a write, opsem_add_write_lem, which shows that it can be added to the
opsem_prefix, although it might be writing a different value than before.  
Add it to the end of modification order for that location (if it is to an atomic
location).  Inter-thread happens before is unchanged, and so the conditions of
consistent_ex all follow immediately.  Furthermore, the race is preserved.

Now we have an SB-downclosed consistent prefix execution with a race or
indeterminate read.  Build a complete consistent execution by following the
opsem using the reasoning above to add reads and writes. This process is simpler
because we always pick an SB-so-far maximal action to add.

*)