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 Q → inclusion A (clos_refl_trans A R) (clos_refl_trans A Q).

Lemma clos_t_inclusion A R Q:
  inclusion A R Q → inclusion 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 x → x = 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 y ⇒ Astar (QQ y) F).

Consequence

Lemma conseq_helper :
  ∀ acts_cmd acts_ctx lab sb rf n (hmap : hbcase → heap) (V : list actid) lst res (Q Q´ : nat → heap → Prop)
  (IMP: ∀ res h, Q res h → Q´ 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 Q´).

Theorem rule_conseq :
  ∀ P E QQ (T: triple P E QQ)
            P´ (PI: implies P´ P)
            QQ´ (QI: ∀ y, implies (QQ y) (QQ´ y)),
    triple P´ 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 e´ (T2: ∀ x, triple (QQ x) (e´ x) RR),
    triple P (Elet e e´) RR.

Parallel composition

Theorem rule_par :
  ∀ P1 e1 QQ1 (T1: triple P1 e1 QQ1)
         P2 e2 Q2 (T2: triple P2 e2 (fun x ⇒ Q2)),
    triple (Astar P1 P2) (Epar e1 e2) (fun x ⇒ Astar (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 x ⇒ if x == 0 then Afalse else QQ x).

Non-atomic allocations

Theorem rule_alloc_na :
triple (Aemp) (Ealloc) (fun x ⇒ Aptu x).

Non-atomic stores

Theorem rule_store_na1 :
  ∀ typ E E´ E´´,
  triple (Apt E E´) (Estore typ E E´´) (fun x ⇒ Apt E E´´).

Theorem rule_store_na2 :
  ∀ typ E E´´,
  triple (Aptu E) (Estore typ E E´´) (fun x ⇒ Apt E E´´).

Non-atomic loads

Theorem rule_load_na :
  ∀ typ E E´,
  triple (Apt E E´) (Eload typ E)
            (fun x ⇒ if x == E´ then Apt E E´ else Afalse).

Atomic allocations

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

Theorem rule_alloc_atom_rmwacq QQ :
triple (Aemp) (Ealloc) (fun x ⇒ Astar (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