Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple.
Require Import ihc drf memsafe initread.

Set Implicit Arguments.

Lemma clos_rt_inclusion A R Q:
  inclusion A R Qinclusion A (clos_refl_trans A R) (clos_refl_trans A Q).

Lemma clos_t_inclusion A R Q:
  inclusion A R Qinclusion A (clos_trans A R) (clos_trans A Q).

Lemma release_seq_implies_hbUrf lab sb rf mo a b:
  release_seq lab sb rf mo a b
  clos_refl_trans _ (happens_before_union_rf sb rf) a b.

Lemma hb_implies_hbUrf lab sb rf mo a b:
  happens_before lab sb rf mo a b
  happens_before_union_rf sb rf a b.

Adequacy

The consistent executions of a closed program are given as follows.

Definition prg_sem e res acts lab sb rf mo sc :=
   fst lst pre post acts´,
    acts = pre :: acts´
    << pNIN: ¬ In pre acts´ >>
    << qNIN: ¬ In post acts´ >>
    << NEQ : pre post >>
    << ESEM: exp_sem e res acts´ lab sb fst lst >>
    << CONS: Consistent (post :: acts) lab sb rf mo sc Model_hb_rf_acyclic >>
    << pSB1: x, ¬ sb x pre >>
    << pSB2: x, sb pre xx = fst >>
    << pSB : unique (sb^~ fst) pre >> << pL : lab pre = Askip >>
    << qSB : unique (sb lst) post >> << qL : lab post = Askip >>.

Adequacy states that all consistent executions of closed programs, e, satisfying the triple {Atrue} e {y. QQ y}, are memory safe and race free. Moreover, the programs never read from uninitialized locations, and their return value satisfies the post-condition.

Theorem adequacy :
   e QQ (T: triple Atrue e QQ) reso acts lab sb rf mo sc
    (SEM : prg_sem e reso acts lab sb rf mo sc),
    mem_safe acts lab sb rf mo
    race_free acts lab sb rf mo
    initialized_reads acts lab rf
    ( res, reso = Some res h, assn_sem (QQ res) h).

Soundness of the proof rules

We now proceed with the proofs of the various RSL proof rules. For conciseness, all the internal lemmas used in these proofs are in rslmodel.v.

Frame


Theorem rule_frame :
   P E QQ (T: triple P E QQ) F,
    triple (Astar P F) E (fun yAstar (QQ y) F).

Consequence


Lemma conseq_helper :
   acts_cmd acts_ctx lab sb rf n (hmap : hbcaseheap) (V : list actid) lst res (Q : natheapProp)
  (IMP: res h, Q res h res h),
  safe acts_cmd acts_ctx lab sb rf n V hmap lst (with_opt res Q) →
  safe acts_cmd acts_ctx lab sb rf n V hmap lst (with_opt res ).

Theorem rule_conseq :
   P E QQ (T: triple P E QQ)
             (PI: implies P)
            QQ´ (QI: y, implies (QQ y) (QQ´ y)),
    triple E QQ´.

Disjunction


Theorem rule_disj :
   P1 E QQ (T1: triple P1 E QQ)
            P2 (T2: triple P2 E QQ),
    triple (Adisj P1 P2) E QQ.

Existential quantification


Theorem rule_exists :
   PP E QQ (T: x, triple (PP x) E QQ),
    triple (Aexists PP) E QQ.

Values


Theorem rule_value v QQ :
  triple (QQ v) (Evalue v) QQ.

Sequential composition (let)


Theorem rule_let :
   P e QQ (T1: triple P e QQ)
         RR (T2: x, triple (QQ x) ( x) RR),
    triple P (Elet e ) RR.

Parallel composition


Theorem rule_par :
   P1 e1 QQ1 (T1: triple P1 e1 QQ1)
         P2 e2 Q2 (T2: triple P2 e2 (fun xQ2)),
    triple (Astar P1 P2) (Epar e1 e2) (fun xAstar (QQ1 x) Q2).

Loops


Theorem rule_repeat :
   P e QQ (T: triple P e QQ) (IMP: implies (QQ 0) P),
    triple P (Erepeat e) (fun xif x == 0 then Afalse else QQ x).

Non-atomic allocations


Theorem rule_alloc_na :
  triple (Aemp) (Ealloc) (fun xAptu x).

Non-atomic stores


Theorem rule_store_na1 :
   typ E E´´,
  triple (Apt E ) (Estore typ E E´´) (fun xApt E E´´).

Theorem rule_store_na2 :
   typ E E´´,
  triple (Aptu E) (Estore typ E E´´) (fun xApt E E´´).

Non-atomic loads


Theorem rule_load_na :
   typ E ,
  triple (Apt E ) (Eload typ E)
            (fun xif x == then Apt E else Afalse).

Atomic allocations


Theorem rule_alloc_atom_acq QQ :
  triple (Aemp) (Ealloc) (fun xAstar (Arel x QQ) (Aacq x QQ)).

Theorem rule_alloc_atom_rmwacq QQ :
  triple (Aemp) (Ealloc) (fun xAstar (Arel x QQ) (Armwacq x QQ)).

Fences


Theorem rule_fence_acq typ P (TYP : acquire_typ typ) :
  triple (Anabla P) (Efence typ) (fun _P).

Theorem rule_fence_rel typ P (TYP : release_typ typ) (NORM: normalizable P) :
  triple (P) (Efence typ) (fun _Atriangle P).


This page has been generated by coqdoc