Commit 5eba6f8a authored by Ralf Jung's avatar Ralf Jung

Merge branch 'auto-lock' into 'master'

Add locking to value-scope notation for lambdas

This attempts to hide all our locking machinery so that users don't have to care. To this end, `locked` is added to the value-scope notation for lambdas and recursive functions, and the tactics wp_rec and wp_lam are enhanced to unlock properly.

The main open question is: How can we figure out automatically what to unfold? The heuristic I cam up with fails in barrier_client because there, we have a value parameterized by something on the Coq level.

Maybe a more viable alternative would be to add locking to the coercion that embeds values into expressions?

Cc @robbertkrebbers @jjourdan

See merge request !34
parents 6e00aa34 6a04e745
Pipeline #3247 passed with stage
in 10 minutes and 51 seconds
......@@ -17,15 +17,17 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E x ef e Φ :
is_Some (to_val e) Closed (x :b: []) ef
WP subst' x e ef @ E {{ Φ }} WP App (Lam x ef) e @ E {{ Φ }}.
Lemma wp_lam E x elam e1 e2 Φ :
e1 = Lam x elam
is_Some (to_val e2)
Closed (x :b: []) elam
WP subst' x e2 elam @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
Lemma wp_let E x e1 e2 Φ :
is_Some (to_val e1) Closed (x :b: []) e2
WP subst' x e1 e2 @ E {{ Φ }} WP Let x e1 e2 @ E {{ Φ }}.
Proof. apply wp_lam. Qed.
Proof. by apply wp_lam. Qed.
Lemma wp_seq E e1 e2 Φ :
is_Some (to_val e1) Closed [] e2
......
......@@ -4,13 +4,13 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Definition assert : val :=
locked (λ: "v", if: "v" #() then #() else #0 #0)%V. (* #0 #0 is unsafe *)
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert -lock. wp_let. wp_seq.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
From iris.heap_lang Require Export notation.
Definition newbarrier : val := locked (λ: <>, ref #false)%V.
Definition signal : val := locked (λ: "x", "x" <- #true)%V.
Definition newbarrier : val := λ: <>, ref #false.
Definition signal : val := λ: "x", "x" <- #true.
Definition wait : val :=
locked (rec: "wait" "x" := if: !"x" then #() else "wait" "x")%V.
rec: "wait" "x" := if: !"x" then #() else "wait" "x".
......@@ -95,7 +95,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
{{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P send l P }}}.
Proof.
iIntros (HN Φ) "#? HΦ".
rewrite -wp_fupd /newbarrier -lock /=. wp_seq. wp_alloc l as "Hl".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with ">[-]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
......@@ -119,7 +119,7 @@ Qed.
Lemma signal_spec l P :
{{{ send l P P }}} signal #l {{{ RET #(); True }}}.
Proof.
rewrite /signal /send /barrier_ctx -lock /=.
rewrite /signal /send /barrier_ctx /=.
iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
......
......@@ -4,12 +4,11 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth.
From iris.heap_lang Require Import proofmode notation.
Definition newcounter : val := locked (λ: <>, ref #0)%V.
Definition incr : val := locked (
rec: "incr" "l" :=
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l")%V.
Definition read : val := locked (λ: "l", !"l")%V.
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
......@@ -36,7 +35,7 @@ Section mono_proof.
heapN N
{{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl".
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
......@@ -72,7 +71,7 @@ Section mono_proof.
{{{ mcounter l j }}} read #l {{{ i, RET #i; j i%nat mcounter l i }}}.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
......@@ -113,7 +112,7 @@ Section contrib_spec.
{{{ heap_ctx }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl".
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (Some (1%Qp, O%nat)) (Some (1%Qp, 0%nat))))
as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
......@@ -147,7 +146,7 @@ Section contrib_spec.
{{{ c, RET #c; n c%nat ccounter γ q n }}}.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
......@@ -159,7 +158,7 @@ Section contrib_spec.
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2.
apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
......
......@@ -5,11 +5,11 @@ Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val :=
locked (λ: "fs",
λ: "fs",
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
("v1", "v2"))%V.
("v1", "v2").
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Section proof.
......@@ -26,7 +26,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par -lock. wp_value. wp_let. wp_proj.
rewrite /par. wp_value. wp_let. wp_proj.
wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
......@@ -44,5 +44,3 @@ Proof.
iSplitL "H1"; by wp_let.
Qed.
End proof.
Global Opaque par.
......@@ -5,15 +5,15 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Definition spawn : val :=
locked (λ: "f",
λ: "f",
let: "c" := ref NONE in
Fork ("c" <- SOME ("f" #())) ;; "c")%V.
Fork ("c" <- SOME ("f" #())) ;; "c".
Definition join : val :=
locked (rec: "join" "c" :=
rec: "join" "c" :=
match: !"c" with
SOME "x" => "x"
| NONE => "join" "c"
end)%V.
end.
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -50,7 +50,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
heapN N
{{{ heap_ctx WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn -lock /=.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
......
......@@ -5,11 +5,11 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Definition newlock : val := ssreflect.locked (λ: <>, ref #false)%V.
Definition try_acquire : val := ssreflect.locked (λ: "l", CAS "l" #false #true)%V.
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
ssreflect.locked (rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l")%V.
Definition release : val := ssreflect.locked (λ: "l", "l" <- #false)%V.
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -48,7 +48,7 @@ Section proof.
heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock. unlock.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
......@@ -83,7 +83,7 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
rewrite /release. unlock. wp_let. iInv N as (b) "[Hl _]" "Hclose".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
......
......@@ -7,24 +7,24 @@ From iris.heap_lang.lib Require Export lock.
Import uPred.
Definition wait_loop: val :=
ssreflect.locked (rec: "wait_loop" "x" "lk" :=
rec: "wait_loop" "x" "lk" :=
let: "o" := !(Fst "lk") in
if: "x" = "o"
then #() (* my turn *)
else "wait_loop" "x" "lk")%V.
else "wait_loop" "x" "lk".
Definition newlock : val :=
ssreflect.locked (λ: <>, ((* owner *) ref #0, (* next *) ref #0))%V.
λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition acquire : val :=
ssreflect.locked (rec: "acquire" "lk" :=
rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1)
then wait_loop "n" "lk"
else "acquire" "lk")%V.
else "acquire" "lk".
Definition release : val :=
ssreflect.locked (λ: "lk", (Fst "lk") <- !(Fst "lk") + #1)%V.
λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
(** The CMRAs we need. *)
Class tlockG Σ :=
......@@ -77,7 +77,7 @@ Section proof.
heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock. unlock.
iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
iMod (own_alloc ( (Excl' 0%nat, ) (Excl' 0%nat, ))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
......@@ -145,7 +145,7 @@ Section proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ".
iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
iDestruct "Hγ" as (o) "Hγo".
rewrite /release. unlock. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
......
......@@ -111,12 +111,6 @@ Proof.
intros; inv_head_step; eauto.
Qed.
Lemma wp_rec_locked E f x erec e1 e2 Φ `{!Closed (f :b: x :b: []) erec} :
e1 = of_val $ locked (RecV f x erec)
is_Some (to_val e2)
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof. unlock. auto using wp_rec. Qed.
Lemma wp_un_op E op e v v' Φ :
to_val e = Some v
un_op_eval op v = Some v'
......
......@@ -47,7 +47,7 @@ Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_sco
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
......@@ -58,20 +58,20 @@ defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation "'rec:' f x y := e" := (Rec f%bind x%bind (Lam y%bind e%E))
(at level 102, f, x, y at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%E))
Notation "'rec:' f x y := e" := (locked (RecV f%bind x%bind (Lam y%bind e%E)))
(at level 102, f, x, y at level 1, e at level 200) : val_scope.
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
(at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
Notation "λ: x , e" := (Lam x%bind e%E)
(at level 102, x at level 1, e at level 200) : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, x, y, z at level 1, e at level 200) : expr_scope.
Notation "λ: x , e" := (LamV x%bind e%E)
Notation "λ: x , e" := (locked (LamV x%bind e%E))
(at level 102, x at level 1, e at level 200) : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
(at level 102, x, y, z at level 1, e at level 200) : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
......
......@@ -44,13 +44,21 @@ Tactic Notation "wp_value" :=
| _ => fail "wp_value: not a wp"
end.
Lemma of_val_unlock v e : of_val v = e of_val (locked v) = e.
Proof. by unlock. Qed.
(* Applied to goals that are equalities of expressions. Will try to unlock the
LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
Tactic Notation "wp_rec" :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
wp_bind_core K; etrans; [|(eapply wp_rec; wp_done) || (eapply wp_rec_locked; wp_done)]; simpl_subst; wp_finish
wp_bind_core K; etrans;
[|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
| _ => fail "wp_rec: not a 'wp'"
end.
......@@ -60,7 +68,8 @@ Tactic Notation "wp_lam" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind_core K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
wp_bind_core K; etrans;
[|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e
| _ => fail "wp_lam: not a 'wp'"
end.
......
......@@ -54,8 +54,6 @@ Section client.
Qed.
End client.
Global Opaque worker client.
Section ClosedProofs.
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
......
......@@ -136,5 +136,3 @@ Proof.
iModIntro; rewrite /C; eauto 10 with omega.
Qed.
End proof.
Global Opaque newcounter incr read.
......@@ -37,7 +37,6 @@ Section LiftingTests.
Definition Pred : val :=
λ: "x",
if: "x" #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
Global Opaque FindPred Pred.
Lemma FindPred_spec n1 n2 E Φ :
n1 < n2
......
......@@ -97,5 +97,3 @@ Proof.
- iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
Qed.
End proof.
Global Opaque client.
......@@ -24,7 +24,6 @@ Definition rev : val :=
"l" <- ("tmp1", "acc");;
"rev" "tmp2" "hd"
end.
Global Opaque rev.
Lemma rev_acc_wp hd acc xs ys (Φ : val iProp Σ) :
heap_ctx is_list hd xs is_list acc ys
......
......@@ -96,5 +96,3 @@ Proof.
iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
Global Opaque one_shot_example.
......@@ -64,6 +64,3 @@ Proof.
rewrite Z.add_0_r.
iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
Qed.
Global Opaque sum_loop sum'.
Markdown is supported
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