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 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 b1 ⇒ a1 == 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 e ⇒ e end.

Definition hb_snd edge :=
  match edge with
    | hb_sb _ e | hb_rf _ e ⇒ Some 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 b ⇒ sb a b
    | hb_rf a b ⇒ rf b = Some a
    | hb_sink a ⇒ ann_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: hbcase → heap) (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 : ∀ e´, hmap (hb_rf e 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: ∀ 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 >> ∧
          << 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 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 = ATrel → hacq = hemp >> ∧
        << ACQ: typ = ATacq → hrel = 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´: hbcase → heap) :=
  ∀ 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 acts_cmd acts_ctx lab (sb : relation actid)
    rf n V hmap lst (Q : heap → 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 o (QQ : nat → heap → Prop) :=
  match o with
    | None ⇒ fun _ ⇒ True
    | Some x ⇒ QQ 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 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) 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