Commit 2749e5ef authored by Hai Dang's avatar Hai Dang
Browse files

Fix logically atomic triples to expose implementation masks

parent c728bfdf
......@@ -70,7 +70,7 @@ Lemma AtomicSeen_CON_XCHG_aux_int
l sn{γ} ζ' -
(if decide (AcqRel ow) then True else {tid} Vrel) -
<<< Vb ζ, {Vb} l at{γ} ζ int_only_hist ζ >>>
XCHG_aux or ow f [ #l ; #v] @ tid;
XCHG_aux or ow f [ #l ; #v] @ tid;
<<< (tr : time) (vr vw : Z) Vr Vw V'' ζ'' ζn,
@{V''} l sn{γ} ζ'' {Vb} l at{γ} ζn
V''
......@@ -162,7 +162,7 @@ Lemma AtomicSeen_CON_XCHG_int
l sn{γ} ζ' -
(if decide (AcqRel ow) then True else {tid} Vrel) -
<<< Vb ζ, {Vb} l at{γ} ζ int_only_hist ζ >>>
XCHG or ow [ #l ; #v] @ tid;
XCHG or ow [ #l ; #v] @ tid;
<<< (tr : time) (vr : Z) Vr Vw V'' ζ'' ζn,
@{V''} l sn{γ} ζ'' {Vb} l at{γ} ζn
V''
......@@ -208,7 +208,7 @@ Lemma AtomicSeen_CON_FAA
l sn{γ} ζ' -
(if decide (AcqRel ow) then True else {tid} Vrel) -
<<< Vb ζ, {Vb} l at{γ} ζ int_only_hist ζ >>>
FAA or ow [ #l ; #v] @ tid;
FAA or ow [ #l ; #v] @ tid;
<<< (tr : time) (vr : Z) Vr Vw V'' ζ'' ζn,
@{V''} l sn{γ} ζ'' {Vb} l at{γ} ζn
V''
......
......@@ -10,7 +10,7 @@ Require Import gpfsl.logic.invariants.
Definition atomic_wp `{!noprolG Σ} {TA TB : tele}
(e: expr) (* expression *)
(tid : thread_id)
(Eo : coPset) (* outer masks *)
(E : coPset) (* implementation masks *)
(α: TA vProp Σ) (* atomic pre-condition *)
(β: TA TB vProp Σ) (* atomic post-condition *)
(POST: TA TB vProp Σ) (* private post condition *) (* TODO: seems to be unnecessary *)
......@@ -18,15 +18,15 @@ Definition atomic_wp `{!noprolG Σ} {TA TB : tele}
: vProp Σ :=
(Φ : val vProp Σ),
(* Fix the inner mask to the shared global namespace histN *)
atomic_update Eo (histN) α β (λ.. x y, POST x y - Φ (f x y)) -
atomic_update (E) (histN) α β (λ.. x y, POST x y - Φ (f x y)) -
WP e @ tid ; top {{ Φ }}.
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; Eo '<<<' ∃ y1 .. yn , β , 'RET' v , POST '>>>'" :=
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; E '<<<' ∃ y1 .. yn , β , 'RET' v , POST '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
e%E
tid
Eo
E
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
λ x1, .. (λ xn, α%I) ..)
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
......@@ -45,16 +45,16 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; Eo '<<<' ∃ y1 .. yn , β , '
(λ y1, .. (λ yn, v%V) .. )
) .. )
)
(at level 20, Eo, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ tid ; Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v , POST '>>>' ']' ']'")
(at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ tid ; E '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v , POST '>>>' ']' ']'")
: bi_scope.
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; Eo '<<<' β , 'RET' v , POST '>>>'" :=
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; E '<<<' β , 'RET' v , POST '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleO)
e%E
tid
Eo
E
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
λ x1, .. (λ xn, α%I) ..)
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
......@@ -71,15 +71,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ tid ; Eo '<<<' β , 'RET' v , POST '
) .. )
)
(at level 20, α, β, v at level 200, x1 binder, xn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ tid ; Eo '/' '[ ' '<<<' β , '/' 'RET' v , POST '>>>' ']' ']'")
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ tid ; E '/' '[ ' '<<<' β , '/' 'RET' v , POST '>>>' ']' ']'")
: bi_scope.
Notation "'<<<' α '>>>' e @ tid ; Eo '<<<' ∃ y1 .. yn , β , 'RET' v , POST '>>>'" :=
Notation "'<<<' α '>>>' e @ tid ; E '<<<' ∃ y1 .. yn , β , 'RET' v , POST '>>>'" :=
(atomic_wp (TA:=TeleO)
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
e%E
tid
Eo
E
(tele_app (TT:=TeleO) α%I)
(tele_app (TT:=TeleO) $
tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
......@@ -91,23 +91,23 @@ Notation "'<<<' α '>>>' e @ tid ; Eo '<<<' ∃ y1 .. yn , β , 'RET' v , POST '
tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
(λ y1, .. (λ yn, v%V) .. ))
)
(at level 20, Eo, α, β , v at level 200, y1 binder, yn binder,
format "'[hv' '<<<' α '>>>' '/ ' e @ tid ; Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v , POST '>>>' ']' ']'")
(at level 20, E, α, β , v at level 200, y1 binder, yn binder,
format "'[hv' '<<<' α '>>>' '/ ' e @ tid ; E '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v , POST '>>>' ']' ']'")
: bi_scope.
Notation "'<<<' α '>>>' e @ tid ; Eo '<<<' β , 'RET' v , POST '>>>'" :=
Notation "'<<<' α '>>>' e @ tid ; E '<<<' β , 'RET' v , POST '>>>'" :=
(atomic_wp (TA:=TeleO)
(TB:=TeleO)
e%E
tid
Eo
E
(tele_app (TT:=TeleO) α%I)
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) POST%I)
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
)
(at level 20, Eo, α, β, v at level 200,
format "'[hv' '<<<' α '>>>' '/ ' e @ tid ; Eo '/' '[ ' '<<<' β , '/' 'RET' v , POST '>>>' ']' ']'")
(at level 20, E, α, β, v at level 200,
format "'[hv' '<<<' α '>>>' '/ ' e @ tid ; E '/' '[ ' '<<<' β , '/' 'RET' v , POST '>>>' ']' ']'")
: bi_scope.
(** Theory *)
......@@ -116,17 +116,17 @@ Section lemmas.
Notation vProp := (vProp Σ).
Implicit Types (α : TA vProp) (β : TA TB vProp) (f : TA TB val).
Lemma atomic_wp_mask_weaken e tid Eo1 Eo2 α β POST f :
Eo2 Eo1 atomic_wp e tid Eo1 α β POST f - atomic_wp e tid Eo2 α β POST f.
Lemma atomic_wp_mask_weaken e tid E1 E2 α β POST f :
E1 E2 atomic_wp e tid E1 α β POST f - atomic_wp e tid E2 α β POST f.
Proof.
iIntros (HEo) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
iApply atomic_update_mask_weaken; last done. done.
iIntros (HE) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
iApply atomic_update_mask_weaken; last done. set_solver.
Qed.
(* Atomic triples imply sequential triples if the precondition is laterable. *)
Lemma atomic_wp_seq e tid Eo α β POST f {HL : .. x, Laterable (α x)}
(Sub: histN Eo) :
atomic_wp e tid Eo α β POST f -
Lemma atomic_wp_seq e tid E α β POST f {HL : .. x, Laterable (α x)}
(Sub: histN E) :
atomic_wp e tid E α β POST f -
Φ, .. x, α x - (.. y, β x y - POST x y - Φ (f x y)) - WP e @ tid; {{ Φ }}.
Proof.
rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
......@@ -137,10 +137,10 @@ Section lemmas.
(** This version matches the Texan triple, i.e., with a later in front of the
[(∀.. y, β x y -∗ Φ (f x y))]. *)
Lemma atomic_wp_seq_step e tid Eo α β POST f {HL : .. x, Laterable (α x)}
(Sub: histN Eo) :
Lemma atomic_wp_seq_step e tid E α β POST f {HL : .. x, Laterable (α x)}
(Sub: histN E) :
TCEq (to_val e) None
atomic_wp e tid Eo α β POST f -
atomic_wp e tid E α β POST f -
Φ, .. x, α x - (.. y, β x y - POST x y - Φ (f x y)) - WP e @ tid; {{ Φ }}.
Proof.
iIntros (TCE) "H"; iIntros (Φ x) "Hα HΦ".
......@@ -151,10 +151,10 @@ Section lemmas.
Qed.
(* Sequential triples with the inner mask for a physically atomic [e] are atomic. *)
Lemma atomic_seq_wp_atomic e tid Eo α β POST f `{!Atomic e} :
Lemma atomic_seq_wp_atomic e tid E α β POST f `{!Atomic e} :
( Φ, .. x, α x - (.. y, β x y - POST x y - Φ (f x y)) -
WP e @ tid; histN {{ Φ }}) -
atomic_wp e tid Eo α β POST f.
atomic_wp e tid E α β POST f.
Proof.
iIntros "Hwp" (Φ) "AU". iMod "AU" as (x) "[Hα [_ Hclose]]".
iApply ("Hwp" with "Hα"). iIntros (y) "Hβ HP".
......@@ -164,12 +164,12 @@ Section lemmas.
(* Sequential triples with a persistent precondition and no initial quantifier
are atomic. *)
Lemma persistent_seq_wp_atomic e tid Eo
Lemma persistent_seq_wp_atomic e tid E
(α : [tele] vProp) (β POST : [tele] TB vProp)
(f : [tele] TB val) {HP : Persistent (α [tele_arg])} :
( Φ, α [tele_arg] - (.. y, β [tele_arg] y - POST [tele_arg] y - Φ (f [tele_arg] y)) -
WP e @ tid; {{ Φ }}) -
atomic_wp e tid Eo α β POST f.
atomic_wp e tid E α β POST f.
Proof.
simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
......@@ -180,13 +180,13 @@ Section lemmas.
(* We can open invariants around atomic triples.
(Just for demonstration purposes; we always use [iInv] in proofs.) *)
Lemma wp_atomic_inv e tid Eo α β POST f N I `{!Objective I} :
N Eo
atomic_wp e tid Eo (λ.. x, I α x) (λ.. x y, I β x y) POST f -
inv N I - atomic_wp e tid (Eo N) α β POST f.
Lemma wp_atomic_inv e tid E α β POST f N I `{!Objective I} :
N E
atomic_wp e tid (E N) (λ.. x, I α x) (λ.. x y, I β x y) POST f -
inv N I - atomic_wp e tid E α β POST f.
Proof.
intros ?. iIntros "Hwp #Hinv" (Φ) "AU". iApply "Hwp". iAuIntro.
iInv N as "HI". iApply (aacc_aupd with "AU"); first done.
iInv N as "HI". iApply (aacc_aupd with "AU"); first solve_ndisj.
iIntros (x) "Hα". iAaccIntro with "[HI Hα]"; rewrite ->!tele_app_bind; first by iFrame.
- (* abort *)
iIntros "[HI $]". by eauto with iFrame.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment