The meaning of triples


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

Set Implicit Arguments.

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

Heap annotations


Inductive hbcase :=
  | hb_sw (e e': nat)
  | hb_sb (e e': nat).

Definition hbcase_eq a b :=
  match a, b with
    | hb_sw a1 a2, hb_sw b1 b2(a1 == b1) && (a2 == b2)
    | hb_sb a1 a2, hb_sb b1 b2(a1 == b1) && (a2 == b2)
    | _, _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_sw e _ | hb_sb e _e end.

Definition hb_snd edge :=
  match edge with hb_sw _ e | hb_sb _ ee end.

We do not annotate all sw edges, but rather only the rf edges from a release-write to an acquire-read.

Definition ann_sw lab rf (a b: actid) :=
  is_release (lab a) is_acquire (lab b) rf b = Some a.

Definition edge_valid lab sb rf edge :=
  match edge with
    | hb_sb a bsb a b
    | hb_sw a bann_sw lab rf a b
  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 mt lab (sb : relation actid) rf mo (a b: actid) : Prop :=
  | hc_edge_sb (HB_SB: sb a b)
  | hc_edge_sw (HB_SW: synchronizes_with lab sb rf mo a b)
  | hc_edge_rf (HB_RF: rf b = Some a)
      (SIDE: mt = Model_hb_rf_acyclic is_na (lab a) is_na (lab b)).

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

View shift implication: currently, vshift h h' h = h', but we have made most of the proofs not depend directly on this definition, so as to allow view shifts that change the logical heaps.

Definition vshift_one (h h' : heap) := False.

Definition vshift := clos_refl_trans _ vshift_one.

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)) >>
          << wEQ : e', hmap (hb_sw e e') = hemp >>)
         (<< NA : typ ATna >> h (P: assn_mod) sws hsink,
          << UPD: vshift (Hdef (initialize hf l))
                         (hsingl l (HVra (hupd Wemp v P) Remp false true) +!+
                          hmap (hb_sb e post) +!+
                          hsum (map hmap (map (hb_sw e) sws)) +!+ hsink) >>
          << TRAN: assn_sem (sval P) h >>
          << swsND: NoDup sws >>
          << swsOK: x, In x sws ann_sw lab rf e x >>
          << swsEQ: hsum (map hmap (map (hb_sw e) sws)) +!+ hsink = h >>
          << RLX: typ = ATrlx typ = ATacq sval P = Aemp >>) >>
    | 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 >>
          << qEQ: hmap (hb_sb e post) = hmap (hb_sb pre e) >>
          << wEQ: e', hmap (hb_sw e' e) = hemp >>)
         (<< NA : typ ATna >> sws hw hF P,
          << swsND: NoDup sws >>
          << swsOK: x, In x sws ann_sw lab rf x e >>
          << swsEQ: hsum (map hmap (map (hb_sw^~ e) sws)) = Hdef hw >>
          << pEQ': hsingl l (HVra Wemp (hupd Remp v P) false true) +!+ hF
                   = Hdef hf >>
          << qD : hmap (hb_sb e post) Hundef >>
          << qEQ: hmap (hb_sb e post) = hsingl l (HVra Wemp Remp false true)
                                             +!+ Hdef hw +!+ hF >>
          << TRAN: assn_sem (sval P) (Hdef hw) >>
          << PREC: precise (sval P) >>) >>
    | Askip
       pres posts hf hsink,
        << 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: vshift (Hdef hf)
                       (hsum (map hmap (map (hb_sb e) posts)) +!+ hsink) >>
    | 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) QQ isrmw,
                 hmap (hb_sb e post) = Hdef (hupd hf l (HVra QQ QQ isrmw false)) >>
    | Armw typ l v v'
       pre post swsIn swsOut,
        << pU: unique (sb^~ e) pre >>
        << qU: unique (sb e) post >>
        << swsInOK: x, In x swsIn ann_sw lab rf x e >>
        << swsOutOK: x, In x swsOut ann_sw lab rf e x >>
        << swsInND: NoDup swsIn >>
        << swsOutND: NoDup swsOut >>
        << NA : typ ATna >>
         PP QQ PP' hp hi hsink,
        << pEQ: hmap (hb_sb pre e) = Hdef hp >>
        << pEQ': hp l = HVra PP QQ true true >>
        << iEQ: hmap (hb_sb pre e) +!+ hsum (map hmap (map (hb_sw^~ e) swsIn)) = Hdef hi >>
        << UPD: vshift (Hdef hi)
                       (hsingl l (HVra PP' Remp false false) +!+ hmap (hb_sb e post) +!+
                        hsum (map hmap (map (hb_sw e) swsOut)) +!+ hsink) >>
        << TRAN: assn_sem (sval (QQ v))
                    (hsum (map hmap (map (hb_sw^~ e) swsIn))) >>
        << TRAN': assn_sem (sval (PP' v'))
                    (hsum (map hmap (map (hb_sw e) swsOut)) +!+ hsink) >>
        << RLX: typ = ATrlx typ = ATacq sval (PP' v') = Aemp >>
  end.

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

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 lab (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))
    (ann_sw lab rf b a hmap (hb_sw b a) = hmap' (hb_sw 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 mt acts_cmd acts_ctx lab (sb : relation actid)
    rf mo 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 mt lab sb rf mo (a :: V)) hmap'
                    (HEQ : agrees lab sb rf V hmap hmap')
                    (VALID' : e (IN: In e (a :: V)),
                                hmap_valid lab sb rf hmap' e),
               safe mt acts_cmd acts_ctx lab sb rf mo n' (a :: V) hmap' lst Q >>
    << GUAR: a (INcmd: In a acts_cmd) (NIN: ¬ In a V)
                    (HC': hist_closed mt lab sb rf mo (a :: V)),
                hmap',
                 << HEQ : agrees lab sb rf V hmap hmap' >>
                 << VALID : e (IN: In e (a :: V)),
                              hmap_valid lab sb rf hmap' e >>
                 << SAFE : safe mt acts_cmd acts_ctx lab sb rf mo 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
    | Nonefun _True
    | Some xQQ x
  end.

Definition triple mt 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 mt)
     (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 mt lab sb rf mo V) hmap
     (VALID : e (IN: In e V), hmap_valid lab sb rf hmap e)
     (pDEF : hmap (hb_sb prev fst) Hundef) hp hFR
     (pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
     (pSAT : assn_sem P hp)
     (NOREL : with_mt mt (no_rlx_writes_global lab) True),
   safe mt acts_cmd acts_ctx lab sb rf mo n V hmap lst
     (with_opt res
       (fun res h hq, h Hundef h = hq +!+ hFR
                                 assn_sem (QQ res) hq)))
  with_mt mt (no_rlx_writes acts_cmd lab) True.


This page has been generated by coqdoc Imprint | Data protection