From iris.algebra Require Import frac excl. From iris.base_logic Require Import base_logic. From iris.proofmode Require Import tactics. From iris.program_logic Require Export hoare. From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import lib.par lib.assert. Section demo1. Context {Σ : gFunctors}. Lemma sep_exist A (P R: iProp Σ) (Ψ: A → iProp Σ) : P ∗ (∃ a, Ψ a) ∗ R -∗ ∃ a, Ψ a ∗ P. Proof. iIntros "[HP [HΨ HR]]". iDestruct "HΨ" as (x) "HΨ". iExists x. iSplitL "HΨ". iAssumption. iAssumption. Qed. Lemma demo_1 (P Q: iProp Σ) (Ψ : Z → iProp Σ) : (∀ x, ▷ P ∗ (True -∗ True) -∗ ▷ Q -∗ Ψ x) -∗ ▷ (P ∗ Q) -∗ Ψ 0. Proof. iIntros "H [HP HQ]". iApply ("H" with "[$HP] HQ"). auto. Qed. End demo1. Section demo2. Context `{heapG Σ}. Definition swap : val := λ: "l1" "l2", let: "tmp" := !"l1" in "l1" <- !"l2";; "l2" <- "tmp". Lemma load_wp_bad (l : loc) v : l ↦ v -∗ WP ! #l {{ w, ⌜w = v⌝ ∗ l ↦ v }}. Proof. iIntros "Hl". wp_load. auto. Qed. Lemma swap_spec_better l1 l2 v1 v2 : l1 ↦ v1 ∗ l2 ↦ v2 -∗ WP swap #l1 #l2 {{ w, ⌜w = #()⌝ ∗ l1 ↦ v2 ∗ l2 ↦ v1 }}. Proof. iIntros "[Hl1 Hl2]". rewrite /swap /=. do 2 wp_lam. wp_bind (! _)%E. (* wp_load. wp_let. wp_load. wp_store. wp_store. iFrame. done. Qed. *) Admitted. Lemma swap_spec l1 l2 v1 v2 : {{{ l1 ↦ v1 ∗ l2 ↦ v2 }}} swap #l1 #l2 {{{ RET #(); l1 ↦ v2 ∗ l2 ↦ v1 }}}. Proof. iIntros (Φ) "[Hl1 Hl2] HΦ". do 2 wp_lam. wp_load. wp_let. wp_load. wp_store. wp_store. iApply "HΦ". iFrame. Qed. End demo2. Record lock Σ `{heapG Σ} := Lock { newlock : val; acquire : val; release : val; is_lock : gname → val → iProp Σ → iProp Σ; locked : gname → iProp Σ; is_lock_persistent γ v R : PersistentP (is_lock γ v R); newlock_spec R : {{{ R }}} newlock #() {{{ γ v, RET v; is_lock γ v R }}}; acquire_spec γ v R : {{{ is_lock γ v R }}} acquire v {{{ RET #(); locked γ ∗ R }}}; release_spec γ v R : {{{ is_lock γ v R ∗ locked γ ∗ R }}} release v {{{ RET #(); True }}}; }. Arguments newlock {_ _} _. Arguments acquire {_ _} _. Arguments release {_ _} _. Arguments is_lock {_ _ _} _ _ _. Arguments newlock_spec {_ _ _} _ _. Existing Instance is_lock_persistent. Section demo3. Context `{spawnG Σ, heapG Σ} (L : lock Σ). Definition foo : expr := let: "x" := ref #0 in let: "y" := ref #4 in let: "z" := newlock L #() in ( acquire L "z";; swap "x" "y";; release L "z" ) ||| ( acquire L "z";; assert: (!"x" + !"y" = #4);; release L "z" ). Lemma foo_spec : {{{ True }}} foo {{{ v, RET v; True }}}. Proof. iIntros (Φ) "HΦ /=". rewrite /foo. wp_alloc lx as "Hlx". wp_let. wp_alloc ly as "Hly". wp_let. wp_apply (newlock_spec (∃ n1 n2 : Z, lx ↦ #n1 ∗ ly ↦ #n2 ∗ ⌜(n1 + n2)%Z = 4⌝)%I with "[Hlx Hly]"); eauto with iFrame. iIntros (lk γ) "#Hlock". wp_let. wp_apply (wp_par (λ _, True)%I (λ _, True)%I with "[] []"). - (* Thread 1 *) wp_apply (acquire_spec with "Hlock"). iIntros "[Hlocked Hinv]". iDestruct "Hinv" as (n1 n2) "(Hlx & Hly & %)". wp_let. wp_apply (swap_spec with "[$Hlx $Hly]"). iIntros "[Hlx Hly]". wp_seq. wp_apply (release_spec with "[$Hlock $Hlocked Hlx Hly]"); eauto with omega iFrame. - (* Thread 2 *) wp_apply (acquire_spec with "Hlock"). iIntros "[Hlocked Hinv]". iDestruct "Hinv" as (n1 n2) "(Hlx & Hly & %)". wp_let. wp_apply wp_assert. wp_load. wp_load. wp_op. wp_op=> ?; last auto with congruence. iSplit; auto. wp_seq. wp_apply (release_spec with "[$Hlock $Hlocked Hlx Hly]"); eauto with omega iFrame. - (* Result *) iIntros (v1 v2) "_". iNext. by iApply "HΦ". Qed. End demo3. Definition new_spinlock : val := λ: <>, ref #false. Definition acquire_spinlock : val := rec: "acquire" "l" := if: CAS "l" #false #true then #() else "acquire" "l". Definition release_spinlock : val := λ: "l", "l" <- #false. Definition lockN := nroot .@ "lock". Section proof. Context `{!heapG Σ, !inG Σ (exclR unitC)}. (* { R * P } e { R * Q } e atomic ---------------------------------- inv R ⊢ { P } e { Q } *) Definition spinlock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ := (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I. Definition is_spinlock (γ : gname) (v : val) (R : iProp Σ) : iProp Σ := (∃ l : loc, ⌜v = #l⌝ ∗ inv lockN (spinlock_inv γ l R))%I. Definition spin_locked (γ : gname): iProp Σ := own γ (Excl ()). Instance is_spinlock_persistent γ l R : PersistentP (is_spinlock γ l R). Proof. apply _. Qed. Lemma new_spinlock_spec (R : iProp Σ): {{{ R }}} new_spinlock #() {{{ γ v, RET v; is_spinlock γ v R }}}. Proof. iIntros (Φ) "HR HΦ". rewrite /new_spinlock /=. wp_seq. iApply wp_fupd. wp_alloc l as "Hl". iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iMod (inv_alloc lockN _ (spinlock_inv γ l R) with "[-HΦ]") as "#?". { iIntros "!>". iExists false. by iFrame. } iModIntro. iApply "HΦ". iExists l. eauto. Qed. Lemma acquire_spinlock_spec γ v R : {{{ is_spinlock γ v R }}} acquire_spinlock v {{{ RET #(); spin_locked γ ∗ R }}}. Proof. iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec. iDestruct "Hl" as (l) "[% #?]"; subst. wp_bind (CAS _ _ _). iInv lockN as ([]) "[Hl HR]" "Hclose". - wp_cas_fail. iMod ("Hclose" with "[Hl]") as "_". { iNext; iExists true; eauto. } iModIntro. wp_if. iApply "IH". auto. - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iMod ("Hclose" with "[Hl]") as "_". { iNext; iExists true; eauto. } iModIntro. wp_if. iApply ("HΦ" with "[$Hγ $HR]"). Qed. Lemma release_spinlock_spec γ v R : {{{ is_spinlock γ v R ∗ spin_locked γ ∗ R }}} release_spinlock v {{{ RET #(); True }}}. Proof. iIntros (Φ) "(Hlock & Hlocked & HR) HΦ". iDestruct "Hlock" as (l) "[% #?]"; subst. rewrite /release /=. wp_let. iInv lockN as (b) "[Hl _]" "Hclose". wp_store. iApply "HΦ". iApply "Hclose". iExists false. by iFrame. Qed. Definition spinlock := {| newlock_spec := new_spinlock_spec; acquire_spec := acquire_spinlock_spec; release_spec := release_spinlock_spec |}. End proof.