Skip to content
Snippets Groups Projects
Commit 703718ed authored by Ralf Jung's avatar Ralf Jung
Browse files

make atomic_wp mask work more like wp mask

parent 3bd580ba
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/program_logic/atomic.v
+ 37
− 46
View file @ 703718ed
......@@ -10,22 +10,24 @@ From iris.prelude Require Import options.
example where we want it to be anything else. *)
Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
(e: expr Λ) (* expression *)
(Eo : coPset) (* (outer) mask *)
(E : coPset) (* *implementation* mask *)
(α: TA → iProp Σ) (* atomic pre-condition *)
(β: TA → TB → iProp Σ) (* atomic post-condition *)
(f: TA → TB → val Λ) (* Turn the return data into the return value *)
: iProp Σ :=
∀ (Φ : val Λ → iProp Σ),
atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
(* The (outer) user mask is what is left after the implementation
opened its things. *)
atomic_update (⊤∖E) ∅ α β (λ.. x y, Φ (f x y)) -∗
WP e {{ Φ }}.
(* Note: To add a private postcondition, use
atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
e%E
Eo
E
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
λ x1, .. (λ xn, α%I) ..)
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
......@@ -39,15 +41,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v
(λ 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 @ Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
(at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ E '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
: bi_scope.
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
(TB:=TeleO)
e%E
Eo
E
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
λ x1, .. (λ xn, α%I) ..)
(tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
......@@ -59,15 +61,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
tele_app (TT:=TeleO) v%V
) .. )
)
(at level 20, Eo, α, β, v at level 200, x1 binder, xn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
(at level 20, E, α, β, v at level 200, x1 binder, xn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ E '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
: bi_scope.
Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleO)
(TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
e%E
Eo
E
(tele_app (TT:=TeleO) α%I)
(tele_app (TT:=TeleO) $
tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
......@@ -76,21 +78,21 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
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 @ Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
(at level 20, E, α, β, v at level 200, y1 binder, yn binder,
format "'[hv' '<<<' α '>>>' '/ ' e @ E '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
: bi_scope.
Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleO)
(TB:=TeleO)
e%E
Eo
E
(tele_app (TT:=TeleO) α%I)
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
(tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
)
(at level 20, Eo, α, β, v at level 200,
format "'[hv' '<<<' α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
(at level 20, E, α, β, v at level 200,
format "'[hv' '<<<' α '>>>' '/ ' e @ E '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
: bi_scope.
(** Theory *)
......@@ -99,16 +101,9 @@ Section lemmas.
Notation iProp := (iProp Σ).
Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
Lemma atomic_wp_mask_weaken e Eo1 Eo2 α β f :
Eo2 ⊆ Eo1 → atomic_wp e Eo1 α β f -∗ atomic_wp e Eo2 α β f.
Proof.
iIntros (HEo) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
iApply atomic_update_mask_weaken; last done. done.
Qed.
(* Atomic triples imply sequential triples if the precondition is laterable. *)
Lemma atomic_wp_seq e Eo α β f {HL : ∀.. x, Laterable (α x)} :
atomic_wp e Eo α β f -∗
Lemma atomic_wp_seq e E α β f {HL : ∀.. x, Laterable (α x)} :
atomic_wp e E α β f -∗
∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
Proof.
rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
......@@ -120,9 +115,9 @@ 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 Eo α β f {HL : ∀.. x, Laterable (α x)} :
Lemma atomic_wp_seq_step e E α β f {HL : ∀.. x, Laterable (α x)} :
TCEq (to_val e) None →
atomic_wp e Eo α β f -∗
atomic_wp e E α β f -∗
∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
Proof.
iIntros (?) "H"; iIntros (Φ x) "Hα HΦ".
......@@ -133,9 +128,9 @@ Section lemmas.
Qed.
(* Sequential triples with the empty mask for a physically atomic [e] are atomic. *)
Lemma atomic_seq_wp_atomic e Eo α β f `{!Atomic WeaklyAtomic e} :
Lemma atomic_seq_wp_atomic e E α β f `{!Atomic WeaklyAtomic e} :
(∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e @ ∅ {{ Φ }}) -∗
atomic_wp e Eo α β f.
atomic_wp e E α β f.
Proof.
iIntros "Hwp" (Φ) "AU". iMod "AU" as (x) "[Hα [_ Hclose]]".
iApply ("Hwp" with "Hα"). iIntros (y) "Hβ".
......@@ -145,10 +140,10 @@ Section lemmas.
(** Sequential triples with a persistent precondition and no initial quantifier
are atomic. *)
Lemma persistent_seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
Lemma persistent_seq_wp_atomic e E (α : [tele] → iProp) (β : [tele] → TB → iProp)
(f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
(∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ Φ (f [tele_arg] y)) -∗ WP e {{ Φ }}) -∗
atomic_wp e Eo α β f.
atomic_wp e E α β f.
Proof.
simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
......@@ -158,26 +153,22 @@ Section lemmas.
rewrite ->!tele_app_bind. done.
Qed.
(** The polarity of [Eo] is the opposite of what one might expect: if you have
an atomic triple with some mask, you can always *shrink* that mask. *)
Lemma wp_atomic_mask e Eo1 Eo2 α β f :
Eo2 ⊆ Eo1 →
atomic_wp e Eo1 α β f -∗
atomic_wp e Eo2 α β f.
Lemma atomic_wp_mask_weaken e E1 E2 α β f :
E1 ⊆ E2 → atomic_wp e E1 α β f -∗ atomic_wp e E2 α β f.
Proof.
intros ?. iIntros "Hwp" (Φ) "AU". iApply "Hwp".
iApply atomic_update_mask_weaken; done.
iIntros (HE) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
iApply atomic_update_mask_weaken; last done. set_solver.
Qed.
(** We can open invariants around atomic triples.
(Just for demonstration purposes; we always use [iInv] in proofs.) *)
Lemma wp_atomic_inv e Eo α β f N I :
↑N ⊆ Eo →
atomic_wp e Eo (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
inv N I -∗ atomic_wp e (Eo ∖ ↑N) α β f.
Lemma atomic_wp_inv e E α β f N I :
↑N ⊆ E →
atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
inv N I -∗ atomic_wp e E α β 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.
......
iris_heap_lang/lib/atomic_heap.v
+ 7
− 7
View file @ 703718ed
......@@ -29,9 +29,9 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
free_spec (l : loc) (v : val) :
{{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
load_spec (l : loc) :
⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ∅ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (w : val) :
⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ⊤
⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ∅
<<< mapsto l (DfracOwn 1) w, RET #() >>>;
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
......@@ -41,7 +41,7 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
[destruct (decide (a = b))] and it will simplify in both places. *)
cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ⊤
⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
<<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
RET (v, #if decide (v = w1) then true else false) >>>;
}.
......@@ -75,7 +75,7 @@ Section derived.
Lemma cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ⊤
⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ∅
<<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
RET #if decide (v = w1) then true else false >>>.
Proof.
......@@ -114,7 +114,7 @@ Section proof.
Qed.
Lemma primitive_load_spec (l : loc) :
⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
<<< l ↦{q} v, RET v >>>.
Proof.
iIntros (Φ) "AU". wp_lam.
......@@ -123,7 +123,7 @@ Section proof.
Qed.
Lemma primitive_store_spec (l : loc) (w : val) :
⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ∅
<<< l ↦ w, RET #() >>>.
Proof.
iIntros (Φ) "AU". wp_lam. wp_let.
......@@ -134,7 +134,7 @@ Section proof.
Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
⊢ <<< ∀ (v : val), l ↦ v >>>
primitive_cmpxchg #l w1 w2 @ ⊤
primitive_cmpxchg #l w1 w2 @ ∅
<<< if decide (v = w1) then l ↦ w2 else l ↦ v,
RET (v, #if decide (v = w1) then true else false) >>>.
Proof.
......
iris_heap_lang/lib/increment.v
+ 4
− 4
View file @ 703718ed
......@@ -21,7 +21,7 @@ Section increment_physical.
else "incr" "l".
Lemma incr_phy_spec (l: loc) :
⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
......@@ -52,7 +52,7 @@ Section increment.
(** A proof of the incr specification that unfolds the definition of atomic
accessors. This is the style that most logically atomic proofs take. *)
Lemma incr_spec_direct (l: loc) :
⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
awp_apply load_spec.
......@@ -91,7 +91,7 @@ Section increment.
prove are in 1:1 correspondence; most logically atomic proofs will not be
able to use them. *)
Lemma incr_spec (l: loc) :
⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
awp_apply load_spec.
......@@ -126,7 +126,7 @@ Section increment.
Lemma weak_incr_spec (l: loc) (v : Z) :
l ↦{#1/2} #v -∗
<<< ∀ (v' : Z), l ↦{#1/2} #v' >>>
weak_incr #l @ ⊤
weak_incr #l @ ∅
<<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros "Hl" (Φ) "AU". wp_lam.
......
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