The meaning of triples


Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps permission fslassn fslassnsem.
Require Import GpsSepAlg.

Set Implicit Arguments.

Infix "+!+" := hplus (at level 30, right associativity).

Heap annotations


Inductive hbcase :=
  | hb_sb (e e': nat)
  | hb_rf (e e': nat)
  | hb_sink (e: nat).
Definition is_sb edge :=
  match edge with
    | hb_sb _ _True
    | _False
  end.

Definition is_rf edge :=
  match edge with
    | hb_sb _ _False
    | hb_rf _ _True
    | hb_sink _False
  end.

Definition is_sink edge :=
  match edge with
    | hb_sink _true
    | _false
  end.

Definition hbcase_eq a b :=
  match a, b with
    | hb_sb a1 a2, hb_sb b1 b2(a1 == b1) && (a2 == b2)
    | hb_rf a1 a2, hb_rf b1 b2(a1 == b1) && (a2 == b2)
    | hb_sink a1, hb_sink b1a1 == b1
    | _, _false
  end.

Lemma hbcase_eqP : Equality.axiom hbcase_eq.
Proof.
  induction[] x [y]; ins; vauto; repeat case eqP; ins;
    try constructor; congruence.
Qed.

Canonical Structure hbcase_eqMixin := EqMixin hbcase_eqP.
Canonical Structure hbcase_eqType := Eval hnf in EqType _ hbcase_eqMixin.

Definition hb_fst edge :=
  match edge with hb_sb e _ | hb_rf e _ | hb_sink ee end.

Definition hb_snd edge :=
  match edge with
    | hb_sb _ e | hb_rf _ eSome e
    | hb_sink _None
  end.

Definition ann_sink lab (a : actid) :=
  match lab a with
    | Aalloc _False
    | Afence _False
    | _True
  end.

Definition edge_valid lab sb rf edge :=
  match edge with
    | hb_sb a bsb a b
    | hb_rf a brf b = Some a
    | hb_sink aann_sink lab a
  end.

A list of nodes A is prefix-closed, hist_closed mt lab sb rf A, if is closed with respect to incoming happens-before edges.

Inductive hc_edge (sb : relation actid) rf (a b: actid) : Prop :=
  | hc_edge_sb (HB_SB: sb a b)
  | hc_edge_rf (HB_RF: rf b = Some a).

Definition hist_closed sb rf (A: list actid) :=
   a (IN: In a A) b (HB: hc_edge sb rf b a), In b A.

Definition happens_before_union_rf sb rf := clos_trans _ (hc_edge sb rf).

Definition IrreflexiveHBuRF sb rf := irreflexive (happens_before_union_rf sb rf).

We proceed to the definition of local heap annotation validity at a node e.

Definition RMW_rel_condition PS PSg typ (hrel: heap PS PSg) :=
  HlabeledExact hrel HLtriangle (typ ATrlx typ ATacq HlabeledExact hrel HLnormal).

Definition RMW_acq_condition PS PSg typ (hacq': heap PS PSg) :=
   HlabeledExact hacq' HLnabla (typ ATrlx typ ATrel HlabeledExact hacq' HLnormal).

Definition hmap_valid PS PSg lab sb rf (hmap: hbcase heap PS PSg) (ga : val option actid) (e: actid) :=
   (gnew : ghost_resource), << NG: x, gnew x None ga x = Some e >>
  match lab e with
    | Astore typ l v
       pre post hf g,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << pEQ : hmap (hb_sb pre e) = Hdef hf g >>
        << DISJ :
         (<< IV : is_lvalue (hf l) >>
          << qEQ : Perm,
                   hmap (hb_sb e post) = Hdef (hupd hf l (lvalue _ _ Perm v)) g +!+ gheap _ _ gnew >>
          << DEF : hmap (hb_sb e post) Hundef >>
          << rEQ : e', hmap (hb_rf e e') = hemp >>
          << sEQ : hmap (hb_sink e) = hemp >>)
         (<< NA : typ ATna >> rfs hr hF (P: assn_mod PS PSg) sbg rfg,
          << UPD: Hdef (initialize hf l) g =
                  hsingl _ _ l (HVra (hupd Wemp v P) Remp false (Some HLCnormal) (Some HLCnormal))
                  +!+ hF +!+ hr >>
          << qEQ: hmap (hb_sb e post) =
                  hsingl _ _ l (HVra (hupd Wemp v P) Remp false (Some HLCnormal) (Some HLCnormal))
                  +!+ hF +!+ sbg >>
          << DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e)
                   Hundef >>
          << rfsSIM: Hsim ((hsum (map hmap (map (hb_rf e) rfs))) +!+ hmap (hb_sink e)) (hr +!+ rfg) >>
          << ghostEQ: sbg +!+ rfg = gheap _ _ gnew >>
          << TRAN: assn_sem (Anabla (sval P)) ((hsum (map hmap (map (hb_rf e) rfs))) +!+ hmap (hb_sink e)) >>
          << TYP: HlabeledExact hr HLtriangle
                  (typ ATrlx typ ATacq HlabeledExact hr HLnormal) >>
          << rfsND: NoDup rfs >>
          << rfsOK: x, In x rfs rf x = Some e >>) >>
    | Aload typ l v
       pre post hf g,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << qD : hmap (hb_sb e post) Hundef >>
        << pEQ: hmap (hb_sb pre e) = Hdef hf g >>
        << DISJ :
         (<< IV : is_rvalueV (hf l) v >>
          << qEQ: hmap (hb_sb e post) = hmap (hb_sb pre e) +!+ gheap _ _ gnew >>
          << rEQ: e', hmap (hb_rf e' e) = hemp >>
          << sEQ: hmap (hb_sink e) = hemp >>)
         (<< NA : typ ATna >> rfs hr hF P,
          << rfsND: NoDup rfs >>
          << rfsOK: x, In x rfs rf e = Some x >>
          << TRAN: assn_sem (Anabla (sval P)) (hsum (map hmap (map (hb_rf^~ e) rfs))) >>
          << rfsSIM: Hsim (hsum (map hmap (map (hb_rf^~ e) rfs))) hr >>
          << sEQ: hmap (hb_sink e) = hsingl _ _ l (HVra Wemp (hupd Remp v P) false None None ) >>
          << pEQ': hsingl _ _ l (HVra Wemp (hupd Remp v P) false None (Some HLCnormal)) +!+ hF
                   = Hdef hf g >>
          << qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra Wemp Remp false None (Some HLCnormal))
                                         +!+ hr +!+ hF +!+ gheap _ _ gnew >>
          << TYP: HlabeledExact hr HLnabla
                  (typ ATrlx typ ATrel HlabeledExact hr HLnormal) >>
          << PREC: precise (sval P) >>
          << NORM: normalizable (sval P) >>) >>
    | Askip
       pres posts,
        << pND: NoDup pres >>
        << pOK: x, In x pres sb x e >>
        << qND: NoDup posts >>
        << qOK: x, In x posts sb e x >>
        << DEF: hsum (map hmap (map (hb_sb e) posts)) +!+ hmap (hb_sink e) Hundef >>
        << EQ: hsum (map hmap (map (hb_sb^~ e) pres)) +!+ gheap _ _ gnew =
                hsum (map hmap (map (hb_sb e) posts)) +!+ hmap (hb_sink e) >>
    | Aalloc l
       pre post hf g,
        << pU : unique (sb^~ e) pre >>
        << qU : unique (sb e) post >>
        << pEQ : hmap (hb_sb pre e) = Hdef hf g >>
        << NALL: hf l = HVnone >>
        << DEF : hmap (hb_sb e post) Hundef >>
        << qEQ : hmap (hb_sb e post) = Hdef (hupd hf l (HVuval HLnormal)) g +!+ gheap _ _ gnew
                  QQ isrmw,
                    hmap (hb_sb e post) = Hdef (hupd hf l (HVra QQ QQ isrmw (Some HLCnormal) None)) g
                                          +!+ gheap _ _ gnew >>
    | Armw typ l v v'
       pre post rfsIn rfsOut,
        << AT: typ ATna >>
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << rfsInND: NoDup rfsIn >>
        << rfsOutND: NoDup rfsOut >>
        << rfsInOK: x, In x rfsIn rf e = Some x >>
        << rfsOutOK: x, In x rfsOut rf x = Some e >>
        << DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e)
                 Hundef >>
         P QQ hrel hrel' hacq hacq' ht hF sbg rfg,
        << pEQ: hmap (hb_sb pre e) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                     +!+ hrel +!+ hF >>
        << rInEQ: hsum (map hmap (map (hb_rf^~ e) rfsIn)) = hacq +!+ ht >>
        << qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                      +!+ hacq' +!+ hF +!+ sbg >>
        << rOutEQ: hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e) = hrel' +!+ ht +!+ rfg >>
        << ghostEQ: sbg +!+ rfg = gheap _ _ gnew >>
        << TRANin: assn_sem (Anabla (sval (QQ v))) (hacq +!+ ht) >>
        << TRANout: assn_sem (Anabla (sval P)) (hrel' +!+ ht) >>
        << RELsim: Hsim hrel hrel' >>
        << ACQsim: Hsim hacq hacq' >>
        << RELlabel: RMW_rel_condition typ hrel >>
        << ACQlabel: RMW_acq_condition typ hacq' >>
    | Afence typ
       pre post,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << DEF: hmap (hb_sb e post) Hundef >>
         hF hrel hrel' hacq hacq',
        << pEQ: hmap (hb_sb pre e) = hF +!+ hrel +!+ hacq >>
        << qEQ: hmap (hb_sb e post) = hF +!+ hrel' +!+ hacq' +!+ gheap _ _ gnew >>
        << RELlabel : HlabeledExact hrel HLnormal >>
        << RELlabel': HlabeledExact hrel' HLtriangle >>
        << ACQlabel : HlabeledExact hacq HLnabla >>
        << ACQlabel': HlabeledExact hacq' HLnormal >>
        << RELsim: Hsim hrel hrel' >>
        << ACQsim: Hsim hacq hacq' >>
        << NA: typ ATna >>
        << RLX: typ ATrlx >>
        << REL: typ = ATrel hacq = hemp >>
        << ACQ: typ = ATacq hrel = hemp >>
  end.

Definition hmap_valids PS PSg lab sb rf hmap A :=
  ga, << GAfin: max, n, max < n ga n = None >>
            << VLD: e (IN: In e A), @hmap_valid PS PSg lab sb rf hmap ga e >>.

Definition is_sb_out edge A := is_sb edge In (hb_fst edge) A.

Definition hmap_valids_strong PS PSg lab sb rf hmap A :=
  << VALIDS: hmap_valids lab sb rf hmap A >>
  << RESTR: e (NIN: ¬ In e A) edge,
                  (hb_fst edge = e (hb_snd edge = Some e ¬ is_sb_out edge A)
                   hmap edge = @hemp PS PSg) >>.

Configuration safety

agrees V hmap hmap' asserts that the two heap maps hmap and hmap' agree on the annotations of the edges for which V is responsible.

Definition agrees PS PSg (sb: relation actid) rf V (hmap hmap': hbcase heap PS PSg) :=
   a (IN: In a V) b,
    (sb a b hmap (hb_sb a b) = hmap' (hb_sb a b))
    (rf a = Some b hmap (hb_rf b a) = hmap' (hb_rf b a)).

A logical configuration is a heap-annotated execution that is locally valid on a prefix-closed set of nodes, V. Such a logical configuration is safe for n steps, if n=0 or the following three conditions hold:
  • If the configuration is a final configuration, it satisfies the postcondition; and
  • Adding any well-annotated executable context event to the configuration preserves safety for another n-1 steps; and
  • Adding any executable program event to the configuration preserves safety for another n-1 steps.

Fixpoint safe PS PSg acts_cmd acts_ctx lab (sb : relation actid)
    rf n V hmap lst (Q : heap PS PSg Prop) :=
  match n with 0 ⇒ True | S n'
    << POST: (IN: In lst V) next (SB: sb lst next),
               Q (hmap (hb_sb lst next)) >>
    << RELY: a (INctx: In a acts_ctx) (NIN: ¬ In a V)
                    (HC': hist_closed sb rf (a :: V)) hmap'
                    (HEQ : agrees sb rf V hmap hmap')
                    (VALID' : hmap_valids_strong lab sb rf hmap' (a :: V)),
               safe acts_cmd acts_ctx lab sb rf n' (a :: V) hmap' lst Q >>
    << GUAR: a (INcmd: In a acts_cmd) (NIN: ¬ In a V)
                    (HC': hist_closed sb rf (a :: V)),
                hmap',
                 << HEQ : agrees sb rf V hmap hmap' >>
                 << VALID : hmap_valids_strong lab sb rf hmap' (a :: V) >>
                 << SAFE : safe acts_cmd acts_ctx lab sb rf n' (a :: V) hmap' lst Q >> >>
  end.

The meaning of triples


Definition no_rlx_writes_global lab :=
   x : actid, ¬ is_rlx_write (lab x).

Definition no_rlx_writes (acts : list actid) lab :=
   x (IN: In x acts), ¬ is_rlx_write (lab x).

The meaning of an RSL triple {P} C {y. QQ(y)} is defined in terms of configuration safety as follows.

Definition with_opt PS PSg o (QQ : nat heap PS PSg Prop) :=
  match o with
    | Nonefun _True
    | Some xQQ x
  end.

Definition triple PS PSg P e QQ :=
   acts_cmd res lab sb fst lst
    (SEM : exp_sem e res acts_cmd lab sb fst lst),
  ( acts_ctx rf mo sc
     (CONS : weakConsistent (acts_cmd ++ acts_ctx) lab sb rf mo sc Model_hb_rf_acyclic)
     (UNIQ : NoDup (acts_cmd ++ acts_ctx)) prev
     (FST : unique (sb^~ fst) prev) next
     (LST : unique (sb lst) next) n V
     (V_PREV: In prev V)
     (V_CTX : x, In x V In x acts_ctx)
     (HC : hist_closed sb rf V) hmap
     (VALID : hmap_valids_strong lab sb rf hmap V)
     (pDEF : hmap (hb_sb prev fst) @Hundef PS PSg) hp hFR
     (pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
     (pSAT : assn_sem P hp),
   safe acts_cmd acts_ctx lab sb rf n V hmap lst
     (with_opt res
       (fun res h hFR' hq, h @Hundef PS PSg h = hq +!+ hFR +!+ hFR'
                                 assn_sem (QQ res) hq))).


This page has been generated by coqdoc