Commit 4443b5c3 authored by Ralf Jung's avatar Ralf Jung

try another approach to taming simpl

parent 6c06af44
......@@ -4,12 +4,12 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth.
From iris.heap_lang Require Import proofmode notation.
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val :=
Definition newcounter : val := locked (λ: <>, ref #0)%V.
Definition incr : val := locked (
rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l")%V.
Definition read : val := locked (λ: "l", !"l")%V.
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
......@@ -36,7 +36,7 @@ Section mono_proof.
heapN N
{{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. 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 +72,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 /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read -lock /=. 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 +113,7 @@ Section contrib_spec.
{{{ heap_ctx }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. 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 +147,7 @@ Section contrib_spec.
{{{ c, RET #c; n c%nat ccounter γ q n }}}.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read -lock /=. 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,12 +159,10 @@ Section contrib_spec.
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read -lock /=. 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|].
by iApply "HΦ".
Qed.
End contrib_spec.
Global Opaque newcounter incr get.
......@@ -7,23 +7,24 @@ From iris.heap_lang.lib Require Export lock.
Import uPred.
Definition wait_loop: val :=
rec: "wait_loop" "x" "lk" :=
ssreflect.locked (rec: "wait_loop" "x" "lk" :=
let: "o" := !(Fst "lk") in
if: "x" = "o"
then #() (* my turn *)
else "wait_loop" "x" "lk".
else "wait_loop" "x" "lk")%V.
Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition newlock : val :=
ssreflect.locked (λ: <>, ((* owner *) ref #0, (* next *) ref #0))%V.
Definition acquire : val :=
rec: "acquire" "lk" :=
ssreflect.locked (rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1)
then wait_loop "n" "lk"
else "acquire" "lk".
else "acquire" "lk")%V.
Definition release : val := λ: "lk",
(Fst "lk") <- !(Fst "lk") + #1.
Definition release : val :=
ssreflect.locked (λ: "lk", (Fst "lk") <- !(Fst "lk") + #1)%V.
(** The CMRAs we need. *)
Class tlockG Σ :=
......@@ -76,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 /=.
iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock. unlock.
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. }
......@@ -144,7 +145,7 @@ Section proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ".
iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
iDestruct "Hγ" as (o) "Hγo".
rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
rewrite /release. unlock. 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
......@@ -168,7 +169,6 @@ Section proof.
End proof.
Typeclasses Opaque is_lock issued locked.
Global Opaque newlock acquire release wait_loop.
Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
......
......@@ -111,6 +111,16 @@ Proof.
intros; inv_head_step; eauto.
Qed.
Lemma wp_rec_locked E f x erec (e1 e2 : expr) Φ `{!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.
intros -> [v2 ?]. unlock. rewrite -(wp_lift_pure_det_head_step' (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_un_op E op e v v' Φ :
to_val e = Some v
un_op_eval op v = Some v'
......
......@@ -50,7 +50,7 @@ Tactic Notation "wp_rec" :=
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]; simpl_subst; wp_finish
wp_bind_core K; etrans; [|(eapply wp_rec; wp_done) || (eapply wp_rec_locked; wp_done)]; simpl_subst; wp_finish
(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
| _ => fail "wp_rec: not a 'wp'"
end.
......
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