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

Set Implicit Arguments.

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 PS PSg :
  ∀ e QQ (T: triple (@Atrue PS PSg) 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 PS PSg :
∀ (P: assn PS PSg) E QQ (T: triple P E QQ) F,
triple (Astar P F) E (fun y ⇒ Astar (QQ y) F).

Consequence

Lemma conseq_helper PS PSg :
  ∀ acts_cmd acts_ctx lab sb rf n (hmap : hbcase → heap PS PSg)
    (V : list actid) lst res (Q Q' : nat → heap PS PSg → 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 PS PSg :
  ∀ (P: assn PS PSg) 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 PS PSg :
  ∀ (P1: assn PS PSg) E QQ (T1: triple P1 E QQ)
            P2 (T2: triple P2 E QQ),
    triple (Adisj P1 P2) E QQ.

Existential quantification

Theorem rule_exists PS PSg :
∀ (PP: val → assn PS PSg) E QQ (T: ∀ x, triple (PP x) E QQ),
triple (Aexists PP) E QQ.

Values

Theorem rule_value PS PSg v (QQ: val → assn PS PSg) :
triple (QQ v) (Evalue v) QQ.

Sequential composition (let)

Theorem rule_let PS PSg :
  ∀ (P: assn PS PSg) 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 PS PSg :
  ∀ (P1: assn PS PSg) 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 PS PSg :
∀ (P: assn PS PSg) 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

Require Import permission.

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

Non-atomic stores

Program Definition Apt_full PS PSg Perm (IN: In Perm PS) l v := @Apt PS PSg Perm IN (Pfull Perm) _ l v.

Theorem rule_store_na1 PS PSg :
  ∀ typ E E' E'' Perm Perm' (IN: In Perm PS) (IN': In Perm' PS),
  triple (Apt_full PS PSg Perm IN E E') (Estore typ E E'') (fun x ⇒ Apt_full PS PSg Perm' IN' E E'').

Theorem rule_store_na2 PS PSg :
  ∀ typ E E'' Perm (IN: In Perm PS),
  triple (@Aptu PS PSg E) (Estore typ E E'') (fun x ⇒ Apt_full PS PSg Perm IN E E'').

Non-atomic loads

Theorem rule_load_na PS PSg :
  ∀ typ Perm (IN: In Perm PS) p E E' (NONZERO: p ≠ Pzero Perm) (DEF: p ≠ Pundef Perm),
  triple (@Apt PS PSg Perm IN p (conj DEF NONZERO) E E') (Eload typ E)
            (fun x ⇒ if x == E' then @Apt PS PSg Perm IN p (conj DEF NONZERO) E E' else @Afalse PS PSg).

Atomic allocations

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

Theorem rule_alloc_atom_rmwacq PS PSg QQ :
triple (@Aemp PS PSg) (Ealloc) (fun x ⇒ Astar (Arel x QQ) (Armwacq x QQ)).

Fences

Theorem rule_fence_acq PS PSg typ (P: assn PS PSg) (TYP : acquire_typ typ) :
  triple (Anabla P) (Efence typ) (fun _ ⇒ P).

Theorem rule_fence_rel PS PSg typ (P: assn PS PSg) (TYP : release_typ typ) (NORM: normalizable P):
  triple P (Efence typ) (fun _ ⇒ Atriangle P).

Theorem rule_fence_ar PS PSg typ (P Q: assn PS PSg) (TYP : acquire_release_typ typ) (NORM: normalizable P):
  triple (Astar P (Anabla Q)) (Efence typ) (fun _ ⇒ Astar (Atriangle P) Q).

This page has been generated by coqdoc