Commit 05a588df authored by Ralf Jung's avatar Ralf Jung

use texan triples for some more subtle cases

parent d2b71e0a
Pipeline #2927 passed with stage
in 9 minutes and 53 seconds
......@@ -57,26 +57,26 @@ Section proof.
iModIntro. iApply "HΦ". iExists l. eauto.
Qed.
Lemma try_acquire_spec γ lk R (Φ: val iProp Σ) :
is_lock γ lk R ((locked γ - R - Φ #true) Φ #false)
WP try_acquire lk {{ Φ }}.
Lemma try_acquire_spec γ lk R :
{{{ is_lock γ lk R }}} try_acquire lk
{{{b; #b, if b is true then locked γ R else True }}}.
Proof.
iIntros "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
iIntros (Φ) "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iDestruct "HΦ" as "[_ HΦ]". iApply "HΦ".
iModIntro. iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iDestruct "HΦ" as "[HΦ _]". rewrite /locked. by iApply ("HΦ" with "Hγ HR").
iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed.
Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ R }}}.
Proof.
iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "[- $Hl]"). iSplit.
- iIntros "Hlked HR". wp_if. iModIntro. iApply "HΦ"; iFrame.
- wp_if. iApply ("IH" with "[HΦ]"). auto.
wp_apply (try_acquire_spec with "[- $Hl]"). iIntros ([]).
- iIntros "[Hlked HR]". wp_if. iModIntro. iApply "HΦ"; iFrame.
- iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
Lemma release_spec γ lk R :
......
......@@ -88,10 +88,10 @@ Section proof.
iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
Qed.
Lemma wait_loop_spec γ lk x R (Φ : val iProp Σ) :
issued γ lk x R (locked γ R - Φ #()) WP wait_loop #x lk {{ Φ }}.
Lemma wait_loop_spec γ lk x R :
{{{ issued γ lk x R }}} wait_loop #x lk {{{; #(), locked γ R }}}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
iIntros (Φ) "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
......@@ -106,7 +106,7 @@ Section proof.
- iMod ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
iModIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
Qed.
Lemma acquire_spec γ lk R :
......
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