The meaning of triples


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

Set Implicit Arguments.

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

Heap annotations


Inductive hbcase :=
  | hb_sb (e : nat)
  | hb_rf (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.

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 hmap_valid lab sb rf (hmap: hbcaseheap) (e: actid) :=
  match lab e with
    | Astore typ l v
       pre post hf,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << pEQ : hmap (hb_sb pre e) = Hdef hf >>
        << DISJ :
         (<< IV : is_val (hf l) >>
          << qEQ : hmap (hb_sb e post) = Hdef (hupd hf l (HVval v HLnormal)) >>
          << rEQ : , hmap (hb_rf e ) = hemp >>
          << sEQ : hmap (hb_sink e) = hemp >>)
         (<< NA : typ ATna >> rfs hr hF (P: assn_mod),
          << UPD: Hdef (initialize hf l) = hmap (hb_sb e post) +!+ hr >>
          << qEQ: hmap (hb_sb e post) =
                   hsingl l (HVra (hupd Wemp v P) Remp false (Some HLCnormal) (Some HLCnormal)) +!+ hF >>
          << rfsSIM: Hsim ((hsum (map hmap (map (hb_rf e) rfs))) +!+ hmap (hb_sink e)) hr >>
          << 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,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << pEQ: hmap (hb_sb pre e) = Hdef hf >>
        << DISJ :
         (<< IV : hf l = HVval v HLnormal >>
          << qEQ: hmap (hb_sb e post) = hmap (hb_sb pre e) >>
          << rEQ: , hmap (hb_rf 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 >>
          << qD : hmap (hb_sb e post) Hundef >>
          << qEQ: hmap (hb_sb e post) = hsingl l (HVra Wemp Remp false None (Some HLCnormal)) +!+ hr +!+ hF >>
          << TYP: HlabeledExact hr HLnabla
                  (typ ATrlx typ ATrel HlabeledExact hr HLnormal) >>
          << PREC: precise (sval P) >>
          << NORM: normalizable (sval P) >>) >>
    | Askip
       pres posts hf,
        << pND: NoDup pres >>
        << pOK: x, In x pres sb x e >>
        << qND: NoDup posts >>
        << qOK: x, In x posts sb e x >>
        << pEQ: hsum (map hmap (map (hb_sb^~ e) pres)) = Hdef hf >>
        << qEQ: Hdef hf = hsum (map hmap (map (hb_sb e) posts)) +!+ hmap (hb_sink e) >>
    | Aalloc l
       pre post hf,
        << pU : unique (sb^~ e) pre >>
        << qU : unique (sb e) post >>
        << pEQ : hmap (hb_sb pre e) = Hdef hf >>
        << NALL: hf l = HVnone >>
        << qEQ : hmap (hb_sb e post) = Hdef (hupd hf l (HVuval HLnormal)) QQ isrmw,
                 hmap (hb_sb e post) = Hdef (hupd hf l (HVra QQ QQ isrmw (Some HLCnormal) None)) >>
    | Armw typ l v False
    | Afence typ
       pre post,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << DEF: hmap (hb_sb pre e) Hundef >>
         hF hrel hrel´ hacq hacq´,
        << pEQ: hmap (hb_sb pre e) = hF +!+ hrel +!+ hacq >>
        << qEQ: hmap (hb_sb e post) = hF +!+ hrel´ +!+ hacq´ >>
        << 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 = ATrelhacq = hemp >>
        << ACQ: typ = ATacqhrel = hemp >>
  end.


Definition hmap_valids lab sb rf hmap A := e (IN: In e A), hmap_valid lab sb rf hmap e.

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

Definition hmap_valids_strong 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) >>.

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 (sb: relation actid) rf V (hmap hmap´: hbcaseheap) :=
   a (IN: In a V) b,
    (sb a bhmap (hb_sb a b) = hmap´ (hb_sb a b))
    (rf a = Some bhmap (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 acts_cmd acts_ctx lab (sb : relation actid)
    rf n V hmap lst (Q : heapProp) :=
  match n with 0 ⇒ True | S
    << 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 (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 (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 o (QQ : natheapProp) :=
  match o with
    | Nonefun _True
    | Some xQQ x
  end.

Definition triple 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 VIn 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) 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 h = hq +!+ hFR +!+ hFR´
                                 assn_sem (QQ res) hq))).


This page has been generated by coqdoc