<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 />
(* -------------------- Lem preliminaries -------------------- *) 

(* Paths through labelled transition systems, following the HOL4 path theory. *) 
(* Should be in Lem's library *)

(* The type of paths with 'a state components and 'b labels *)
type ('a, 'b) path

(* Checks that a path is through the (curried) relation *)
val okpath : forall 'a 'b. ('a->'b->'a->bool) -> ('a,'b) path -> bool

(* Is the path finite *)
val is_stopped : forall 'a 'b. ('a,'b) path -> bool

(* The set of all number that can be used to index the path (i.e., all numbers
for infinite paths, and those less than the length for other paths) *)
val PL : forall 'a 'b. ('a,'b) path -> num set

val first : forall 'a 'b. ('a,'b) path -> 'a
val last : forall 'a 'b. ('a,'b) path -> 'a
val nth : forall 'a 'b. num -> ('a,'b) path -> 'a 
val nth_label : forall 'a 'b. num -> ('a,'b) path -> 'b

(* Some relation theory that should be in Lem's library *)
type 'a reln = ('a * 'a) set

val rrestrict : forall 'a. 'a reln -> 'a set -> 'a reln
let rrestrict r s = { (x,y) | forall ((x,y) IN r) | x IN s && y IN s }

val down_closed : forall 'a. 'a set -> 'a reln -> bool
let down_closed s r = forall x (y IN s). (x,y) IN r --> x IN s

(* Relation composition *)
val (@@) : forall 'a. 'a reln -> 'a reln -> 'a reln
let (@@) r1 r2 = { (x,z) | exist y. (x,y) IN r1 && (y,z) IN r2 } 
let rc r s = r union { (x,x) | forall (x IN s) | true }

val tc : forall 'a. 'a reln -> 'a reln

val reln_subst : forall 'a. 'a reln -> 'a -> 'a -> 'a reln
(* Replace x with x' in relation r *)
let reln_subst r x' x = 
  { (a,b) | forall ((a,b) IN r) | a <> x && b <> x } union
  { (a,x') | forall a | (a,x) IN r } union
  { (x',a) | forall a | (x,a) IN r }

(* extend to a strict linear order; should only be applied to strict partial
orders *)
val strict_linearize : forall 'a. 'a reln -> 'a reln

val is_acyclic : forall 'a. 'a reln -> bool

val image : forall 'a 'b. ('a -> 'b) -> 'a set -> 'b set
let image f xs = { f x | forall (x IN xs) | true }


(* -------------------- Naming preliminaries -------------------- *)

type c_action = Atomic.action
(*type p_action = MachineDefTypes`action
type i_action = intermediate_actions`action*)

type c_thread_id = Atomic.thread_id
(*type p_thread_id = MachineDefTypes`thread_id*)

type c_value = Atomic.value
(*type p_value = MachineDefValue`value*)

let c_happens_before = Atomic.happens_before

let c_is_write = Atomic.is_write
let c_is_load = Atomic.is_load
let c_is_read = Atomic.is_read

open Atomic
(*open atomic_simple
open MachineDefTypes 
open MachineDefSystem
open MachineDefValue
open intermediate_actions*)

(* -------------------- C++ thread semantics -------------------- *)

(* opinfo collects the information that arises from the thread semantics

The lk field contains the dynamic kind of each location (i.e., Atomic or
Non_atomic).

The sb, asw, and dd fields contains the sequenced before, additional
synchronizes with, and data dependence information information required by the
memory model.  The cd field contains a semantic notion of control dependence
that compilation must respect, and which is necessary in opsem_add_read_axiom
below.

*)

type opinfo = 
  <| lk : location -> location_kind;
     sb : c_action reln; 
     asw : c_action reln; 
     dd : c_action reln; 
     cd : c_action reln; |>

let restrict_opinfo o actions =
  <| lk = o.lk;
     sb = rrestrict o.sb actions;
     asw = rrestrict o.asw actions;
     dd = rrestrict o.dd actions;
     cd = rrestrict o.cd actions; |>

let subst_opinfo o x' x =
  <| lk = o.lk;
     sb = reln_subst o.sb x' x;
     asw = reln_subst o.asw x' x;
     dd = reln_subst o.dd x' x;
     cd = reln_subst o.cd x' x; |>

(* We'll fix an abstract type of single-threaded C++ programs *)

type c_program_thread

(* And we'll fix a semantics for the thread-local behaviour of such programs *)

val single_thread_opsem : c_program_thread -> (c_action set * opinfo) set

(* Given a single-threaded C++ program, single_thread_opsem returns a (possibly
infinite) set of results of that program.  Each result contains the set of
actions that occurred, and the other relevant operational information.  The
intention is that memory reads can non-deterministically read any value; this is
captured formally in opsem_add_read_axiom below. *)

(* A C++ program is a mapping from thread ids to single-threaded C++ programs *)
type c_program = (c_thread_id, c_program_thread) Pmap.map

(* opsem combines the single-threaded results *)
val opsem : c_program -> (c_action set * c_thread_id set * opinfo) set
let opsem p =
  let c_tids = { tid | Pmap.mem tid p } in 
  { (actions, c_tids, o)
    | forall actions o
    | { thread_id_of a | forall (a IN actions) | true } subset c_tids &&
      (forall ((a,b) IN o.sb). thread_id_of a = thread_id_of b) &&
      (forall ((a,b) IN o.asw). thread_id_of a = thread_id_of b) &&
      (forall ((a,b) IN o.dd). thread_id_of a = thread_id_of b) &&
      (forall ((a,b) IN o.cd). thread_id_of a = thread_id_of b) &&
      (forall (c_tid IN c_tids).
         let t_actions = { a | forall (a IN actions) | thread_id_of a = c_tid } in
           ((t_actions, restrict_opinfo o t_actions) IN single_thread_opsem (Pmap.find c_tid p))) }

(* Is the set actions' a subset of a complete opsem that respects data and
control dependency, but not necessarily sequenced-before *)
val opsem_prefix : 
  c_program -> c_action set -> c_action set -> c_thread_id set -> opinfo -> bool
let opsem_prefix p actions' actions c_tids o =
  (actions, c_tids, o) IN opsem p &&
  actions' subset actions &&
  down_closed actions' (tc (o.dd union o.cd))

(* Replaces the value read or written by an action with all possibilities *)
val all_values : c_action -> c_action set
let all_values a = match a with
  | Load aid tid loc v -> { Load aid tid loc v' | forall v' | true }
  | Atomic_load aid tid mo loc v -> { Atomic_load aid tid mo loc v' | forall v' | true }
  | Store aid tid loc v -> { Store aid tid loc v' | forall v' | true }
  | Atomic_store aid tid mo loc v -> { Atomic_store aid tid mo loc v' | forall v' | true }
end

(* We require this property of opsem that allows the value read at a certain
point to be changed arbitrarily without disturbing future data+control
independent actions *)
let opsem_add_read_axiom =
  forall p actions' actions c_tids o (a IN actions \ actions') (a' IN all_values a).
    opsem_prefix p actions' actions c_tids o &&
    c_is_read a &&
    (forall (b IN actions). (b,a) IN tc (o.dd union o.cd) --> b IN actions')
    -->
    (exist new_actions new_o.
       let unchanged_actions = 
         { b | forall (b IN actions \ actions') 
             | b <> a && not ((a,b) IN tc (o.dd union o.cd)) }
       in
       let staying_actions = actions' union unchanged_actions in
         (new_actions inter staying_actions = {}) &&
         (subst_opinfo (restrict_opinfo o (staying_actions union {a})) a' a =
          restrict_opinfo new_o (staying_actions union {a'})) &&
         (forall ((x,y) IN tc (new_o.dd union new_o.cd)). 
            x IN new_actions --> not (y IN staying_actions union {a'})) &&
         (staying_actions union {a'} union new_actions, c_tids, new_o) IN opsem p)
        
(* The following lemma lets us add writes to an opsem_prefix, without changing
their value.  It follows immediately from the definition of opsem_prefix *)
let opsem_add_write_lem = 
  forall p actions' actions c_tids o (a IN actions \ actions').
    opsem_prefix p actions' actions c_tids o &&
    (c_is_write a) &&
    (forall (b IN actions). (b,a) IN tc (o.dd union o.cd) --> b IN actions')
    -->
    (let actions'' = {a} union actions' in
       opsem_prefix p actions'' actions c_tids o)

(* We also require that the operational semantics produces well-formed threads
*)
let opsem_wfthreads_axiom =
  forall p actions c_tids o. 
    (actions, c_tids, o) IN opsem p 
    -->
    well_formed_threads actions c_tids o.lk o.sb o.asw o.dd o.cd

(* -------------------- C++ memory model prelimiaries -------------------- *)

let build_sw actions o rf mo sc =
  synchronizes_with_set actions o.sb o.asw rf sc
                        (release_sequence_set actions o.lk mo) 
                        (hypothetical_release_sequence_set actions o.lk mo)

let build_hb actions o rf mo sc = 
  no_vsse_consume_happens_before actions o.sb (build_sw actions o rf mo sc)

(* The memory model, simplified for the situation we treat in this proof *)
let consistent_ex actions c_tids o rf mo sc =
  no_vsse_consume_consistent_execution actions c_tids o.lk o.sb o.asw o.dd o.cd rf mo sc

(* Programs that have no undefined behaviour *)
val drf : c_program -> bool
let drf p =
  let executions =
    { (actions,c_tids,o,rf,mo,sc) |
      (actions,c_tids,o) IN opsem p && consistent_ex actions c_tids o rf mo sc }
  in
    (forall ((actions,c_tids,o,rf,mo,sc) IN executions).
       indeterminate_reads actions rf = {} &&
       unsequenced_races actions o.sb = {} &&
       data_races actions (build_hb actions o rf mo sc) = {})

val c_semantics : c_program -> (c_action set * c_action reln) set option
let c_semantics p =
  if drf p then
    Some { (actions,rf) | exist c_tids o mo sc. 
                            (actions,c_tids,o) IN opsem p &&
                            consistent_ex actions c_tids o rf mo sc }
  else
    None


(* --------------------  -------------------- *)  

(* A predicate checking whether the C++ reads from follows happens-before.
This is the property that a C++ execution requires, but might not be respected
by a Power trace.  However, in that case, we can show that the program is racy. *)
val rf_in_hb_condition : (c_action set) -> opinfo -> c_action reln -> c_action reln -> c_action reln -> bool
let rf_in_hb_condition actions o rf mo sc =
  let hb = build_hb actions o rf mo sc in
    forall ((x,y) IN rf). 
      (is_atomic_load y --> (exist x'. c_is_write x' && same_location x' y && (x',y) IN hb)) &&
      (c_is_load y --> (x,y) IN hb)