Commit 08039edc authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of all the timeless stuff.

parent 30503baf
......@@ -89,16 +89,16 @@ Section a_wp_rules.
iIntros (v) "H". by iApply ("H" with "[$]").
Qed.
Lemma awp_atomic e (ev : val) R Φ `{Timeless _ R} :
Lemma awp_atomic e (ev : val) R Φ :
IntoVal e ev
(R - R', Timeless R' R' awp (ev #()) R' (λ w, R' - R Φ w)) -
(R - R', R' awp (ev #()) R' (λ w, R' - R Φ w)) -
awp (a_atomic e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic. wp_lam.
iIntros (γ π env l) "#Hlock1 Hunfl1". do 2 wp_let.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[Hflkd [Henv HR]] /=". wp_seq.
iDestruct ("Hwp" with "HR") as (R') "(% & HR' & Hwp)".
iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]".
wp_apply (newlock_cancel_spec amonadN (env_inv env R')%I with "[$Henv $HR']").
iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
......@@ -110,7 +110,7 @@ Section a_wp_rules.
iIntros "Hunfl1". wp_seq. iFrame.
Qed.
Lemma awp_atomic_env e (ev : val) R Φ `{Timeless _ R} :
Lemma awp_atomic_env e (ev : val) R Φ :
IntoVal e ev
( env, env_inv env - R -
WP ev env {{ w, env_inv env R Φ w }}) -
......@@ -153,8 +153,8 @@ End a_wp_rules.
Section a_wp_run.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.
Lemma awp_run (v : val) R Φ `{Timeless _ R} :
R - ( `{locking_heapG Σ}, awp v R (λ w, R - Φ w)) -
Lemma awp_run (v : val) R Φ :
R - ( `{locking_heapG Σ}, awp v R (λ w, R ={}= Φ w)) -
WP a_run v {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /a_run /=. wp_let.
......@@ -166,8 +166,8 @@ Section a_wp_run.
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp".
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
iIntros (w) "[HΦ Hunfl]". iApply "HΦ".
by iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]".
iIntros (w) "[HΦ Hunfl]".
iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]". by iApply "HΦ".
Qed.
End a_wp_run.
......
......@@ -56,7 +56,7 @@ Definition a_while: val := λ: "cond" "body",
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma a_seq_spec R `{Timeless _ R} Φ :
Lemma a_seq_spec R Φ :
U (Φ #()) -
awp (a_seq #()) R Φ.
Proof.
......@@ -88,7 +88,7 @@ Section proofs.
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_load_spec R `{Timeless _ R} (l : loc) (v : val) Φ :
Lemma a_load_spec R (l : loc) (v : val) Φ :
l U v -
(l U v - Φ v) -
awp (a_load (a_ret #l)) R Φ.
......@@ -120,7 +120,7 @@ Section proofs.
- by iApply "HΦ".
Qed.
Lemma a_alloc_spec R `{Timeless _ R} (v : val) Φ :
Lemma a_alloc_spec R (v : val) Φ :
( l, l U v - Φ #l) -
awp (a_alloc (a_ret v)) R Φ.
Proof.
......@@ -149,7 +149,7 @@ Section proofs.
- by iApply "HΦ".
Qed.
Lemma a_store_spec `{Timeless _ R} (l : loc) (v : val) (we : expr) (w : val) Φ :
Lemma a_store_spec R (l : loc) (v : val) (we : expr) (w : val) Φ :
IntoVal we w
l U v -
(l L w - Φ w) -
......@@ -201,7 +201,7 @@ Section proofs.
- iApply "HΦ". iFrame.
Qed.
Lemma a_if_true_spec `{Timeless _ R} (e1 e2 : val) Φ :
Lemma a_if_true_spec R (e1 e2 : val) Φ :
awp e1 R Φ - awp (a_if (a_ret #true) e1 e2) R Φ.
Proof.
unfold a_if. iIntros "HΦ".
......@@ -211,7 +211,7 @@ Section proofs.
awp_lam. by awp_if_true.
Qed.
Lemma a_if_false_spec `{Timeless _ R} (e1 e2 : val) Φ :
Lemma a_if_false_spec R (e1 e2 : val) Φ :
awp e2 R Φ - awp (a_if (a_ret #false) e1 e2) R Φ.
Proof.
unfold a_if. iIntros "HΦ".
......@@ -220,5 +220,4 @@ Section proofs.
iApply awp_value.
awp_lam. by awp_if_false.
Qed.
End proofs.
......@@ -10,6 +10,8 @@ Inductive lockstate :=
| Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.
Instance lockstate_inhabited : Inhabited lockstate := populate Unlocked.
Record flock_name := {
flock_lock_name : gname;
flock_cinv_name : gname;
......@@ -23,7 +25,6 @@ Class flockG Σ :=
flock_lockG :> lockG Σ
}.
Section cinv_lemmas.
Context `{invG Σ, cinvG Σ}.
......@@ -70,13 +71,6 @@ Section flock.
| Unlocked => R
end)%I.
Local Instance flock_inv_timeless γ R `{Timeless _ R} : Timeless (flock_inv γ R).
Proof.
rewrite /flock_inv.
apply uPred.exist_timeless => s.
destruct s; apply _.
Qed.
Definition is_flock (γ : flock_name) (lk : val) (R : iProp Σ) : iProp Σ :=
(cinv (N .@ "inv") (flock_cinv_name γ) (flock_inv γ R)
is_lock (N .@ "lock") (flock_lock_name γ) lk
......@@ -93,12 +87,10 @@ Section flock.
cinv_own (flock_cinv_name γ) (q/2))%I.
Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
unflocked γ (π1+π2)
unflocked γ π1 unflocked γ π2.
unflocked γ (π1+π2) unflocked γ π1 unflocked γ π2.
Proof. by rewrite /unflocked fractional. Qed.
Global Instance unflocked_fractional γ :
Fractional (unflocked γ).
Global Instance unflocked_fractional γ : Fractional (unflocked γ).
Proof. intros p q. apply unflocked_op. Qed.
Global Instance unflocked_as_fractional γ π :
AsFractional (unflocked γ π) (unflocked γ) π.
......@@ -121,10 +113,10 @@ Section flock.
rewrite /is_flock. by iFrame "Hlock".
Qed.
Lemma acquire_cancel_spec γ π lk (R : iProp Σ) `{Timeless _ R} :
Lemma acquire_cancel_spec γ π lk (R : iProp Σ) :
{{{ is_flock γ lk R unflocked γ π }}}
acquire lk
{{{ RET #(); flocked γ π R }}}.
{{{ RET #(); flocked γ π R }}}.
Proof.
iIntros (Φ) "[Hl Hunfl] HΦ". rewrite -wp_fupd.
rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
......@@ -132,14 +124,10 @@ Section flock.
iIntros "[Hlocked Hunlk]".
iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
rewrite {2}/flock_inv.
(* TODO: why doesn't this work?
iDestruct "Hstate" as (s) "Hstate". *)
iDestruct "Hstate" as ">Hstate".
iDestruct "Hstate" as (s) "Hstate".
destruct s as [q|].
- iDestruct "Hstate" as "(Hstate & Hcown & Hlocked2)".
iDestruct "Hstate" as ([q|]) "Hstate".
- iDestruct "Hstate" as ">(Hstate & Hcown & Hlocked2)".
iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
- iDestruct "Hstate" as "[Hstate HR]".
- iDestruct "Hstate" as "[>Hstate HR]".
iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
{ apply (auth_update _ _ (Excl' (Locked π)) (Excl' (Locked π))).
apply option_local_update.
......@@ -151,8 +139,8 @@ Section flock.
iApply "HΦ". by iFrame.
Qed.
Lemma release_cancel_spec γ π lk R `{Timeless _ R} :
{{{ is_flock γ lk R flocked γ π R }}}
Lemma release_cancel_spec γ π lk R :
{{{ is_flock γ lk R flocked γ π R }}}
release lk
{{{ RET #(); unflocked γ π }}}.
Proof.
......@@ -160,19 +148,15 @@ Section flock.
rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
rewrite {2}/flock_inv.
(* TODO: why doesn't this work?
iDestruct "Hstate" as (s) "Hstate". *)
iDestruct "Hstate" as ">Hstate".
iDestruct "Hstate" as (s) "Hstate".
destruct s as [q|]; last first.
- iDestruct "Hstate" as "[Hstate HR']".
iDestruct "Hstate" as ([q|]) "Hstate"; last first.
- iDestruct "Hstate" as "[>Hstate HR']".
iExFalso. iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
iPureIntro. revert Hfoo.
rewrite auth_valid_discrete /= left_id.
intros [Hexcl _].
apply Some_included_exclusive in Hexcl; try (done || apply _).
simplify_eq.
- iDestruct "Hstate" as "(Hstate & Hcown & Hlocked)".
- iDestruct "Hstate" as ">(Hstate & Hcown & Hlocked)".
iAssert (q = π⌝)%I with "[Hstate Hstate']" as %->.
{ iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
iPureIntro. revert Hfoo.
......@@ -192,19 +176,16 @@ Section flock.
by iSplitL "Hcown".
Qed.
Lemma cancel_lock γ lk R `{Timeless _ R} :
is_flock γ lk R - unflocked γ 1 ={}= R.
Lemma cancel_lock γ lk R :
is_flock γ lk R - unflocked γ 1 ={}= R.
Proof.
rewrite /is_flock /unflocked.
iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "Hcown".
iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as ">$"; eauto.
iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
iIntros "[Hcown Hstate]".
iDestruct "Hstate" as ">Hstate".
iDestruct "Hstate" as (s) "(Hstate & HR)".
destruct s as [q|].
- iDestruct "HR" as "(Hcown2 & Hlocked)".
iDestruct "Hstate" as ([q|]) "(Hstate & HR)".
- iDestruct "HR" as ">(Hcown2 & Hlocked)".
iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
- by iFrame.
Qed.
End flock.
......@@ -20,9 +20,9 @@ Section test.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
Lemma test2 (l r : loc) R `{Timeless _ R}:
Lemma test2 (l r : loc) R :
l U #3 - r L #0 -
awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l))%E R (fun v => v = #1).
awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (fun v => v = #1).
Proof.
iIntros "Hl Hr".
iApply awp_bind.
......@@ -34,5 +34,4 @@ Section test.
awp_lam.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
End test.
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