Robbert Krebbers committed Jan 08, 2018 1 2 3 4 5 ``````(** In this exercise we use the spin-lock from the previous exercise to implement the running example during the lecture of the tutorial: proving that when two threads increase a reference that's initially zero by two, the result is four. *) `````` Hai Dang committed May 24, 2019 6 ``````From iris.algebra Require Import auth frac_auth excl. `````` Robbert Krebbers committed Jan 08, 2018 7 8 ``````From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import lib.par proofmode notation. `````` Ralf Jung committed Feb 01, 2019 9 ``````From solutions Require Import ex_03_spinlock. `````` Robbert Krebbers committed Jan 08, 2018 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 `````` (** The program as a heap-lang expression. We use the heap-lang [par] module for parallel composition. *) Definition parallel_add : expr := let: "r" := ref #0 in let: "l" := newlock #() in ( (acquire "l";; "r" <- !"r" + #2;; release "l") ||| (acquire "l";; "r" <- !"r" + #2;; release "l") );; acquire "l";; !"r". (** 1st proof : we only prove that the return value is even. No ghost state is involved in this proof. *) Section proof1. Context `{!heapG Σ, !spawnG Σ}. Definition parallel_add_inv_1 (r : loc) : iProp Σ := (∃ n : Z, r ↦ #n ∗ ⌜ Zeven n ⌝)%I. (** *Exercise*: finish the missing cases of this proof. *) Lemma parallel_add_spec_1 : {{{ True }}} parallel_add {{{ n, RET #n; ⌜Zeven n⌝ }}}. Proof. iIntros (Φ) "_ Post". unfold parallel_add. wp_alloc r as "Hr". wp_let. wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]"). { (* exercise *) iExists 0. iFrame. } iIntros (l) "#Hl". wp_let. `````` Ralf Jung committed Feb 18, 2019 41 `````` wp_apply (wp_par (λ _, True%I) (λ _, True%I)). `````` Robbert Krebbers committed Jan 08, 2018 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". wp_seq. wp_load. wp_op. wp_store. wp_apply (release_spec with "[Hr \$Hl]"); [|done]. iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven. - (* exercise *) wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". wp_seq. wp_load. wp_op. wp_store. wp_apply (release_spec with "[Hr \$Hl]"); [|done]. iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven. - (* exercise *) iIntros (v1 v2) "_ !>". wp_seq. wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]". wp_seq. wp_load. by iApply "Post". Qed. End proof1. (** 2nd proof : we prove that the program returns 4 exactly. We need a piece of ghost state: integer ghost variables. Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the proofs, we now need to make sure that we can use integer ghost variables. For this, we add the type class constraint: inG Σ (authR (optionUR (exclR ZC))) *) Section proof2. Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZC)))}. Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ := (∃ n1 n2 : Z, r ↦ #(n1 + n2) ∗ own γ1 (● (Excl' n1)) ∗ own γ2 (● (Excl' n2)))%I. (** Some helping lemmas for ghost state that we need in the proof. In actual proofs we tend to inline simple lemmas like these, but they are here to make things easier to understand. *) Lemma ghost_var_alloc n : (|==> ∃ γ, own γ (● (Excl' n)) ∗ own γ (◯ (Excl' n)))%I. Proof. `````` Hai Dang committed May 24, 2019 82 83 84 `````` iMod (own_alloc (● (Excl' n) ⋅ ◯ (Excl' n))) as (γ) "[??]". - by apply auth_both_valid. - by eauto with iFrame. `````` Robbert Krebbers committed Jan 08, 2018 85 86 87 88 89 90 91 `````` Qed. Lemma ghost_var_agree γ n m : own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜ n = m ⌝. Proof. iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯") `````` Hai Dang committed May 24, 2019 92 `````` as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. `````` Robbert Krebbers committed Jan 08, 2018 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 `````` Qed. Lemma ghost_var_update γ n' n m : own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) ==∗ own γ (● (Excl' n')) ∗ own γ (◯ (Excl' n')). Proof. iIntros "Hγ● Hγ◯". iMod (own_update_2 _ _ _ (● Excl' n' ⋅ ◯ Excl' n') with "Hγ● Hγ◯") as "[\$\$]". { by apply auth_update, option_local_update, exclusive_local_update. } done. Qed. (** *Exercise*: finish the missing cases of the proof. *) Lemma parallel_add_spec_2 : {{{ True }}} parallel_add {{{ RET #4; True }}}. Proof. iIntros (Φ) "_ Post". unfold parallel_add. wp_alloc r as "Hr". wp_let. iMod (ghost_var_alloc 0) as (γ1) "[Hγ1● Hγ1◯]". iMod (ghost_var_alloc 0) as (γ2) "[Hγ2● Hγ2◯]". wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]"). { (* exercise *) iExists 0, 0. iFrame. } iIntros (l) "#Hl". wp_let. `````` Ralf Jung committed Feb 18, 2019 116 `````` wp_apply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2)) `````` Robbert Krebbers committed Jan 08, 2018 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 `````` with "[Hγ1◯] [Hγ2◯]"). - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)". wp_seq. wp_load. wp_op. wp_store. iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->. iMod (ghost_var_update γ1 2 with "Hγ1● Hγ1◯") as "[Hγ1● Hγ1◯]". wp_apply (release_spec with "[- \$Hl Hγ1◯]"); [|by auto]. iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2); [done|ring]. - (* exercise *) wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)". wp_seq. wp_load. wp_op. wp_store. iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->. iMod (ghost_var_update γ2 2 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]". wp_apply (release_spec with "[- \$Hl Hγ2◯]"); [|by auto]. iExists _, _. iFrame "Hγ1● Hγ2●". by rewrite -Z.add_assoc. - (* exercise *) iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq. wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)". wp_seq. wp_load. iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->. iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->. by iApply "Post". Qed. End proof2. (** 3rd proof : we prove that the program returns 4 exactly, but using a fractional authoritative ghost state. We need another piece of ghost state. *) Section proof3. Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}. Definition parallel_add_inv_3 (r : loc) (γ : gname) : iProp Σ := `````` Ralf Jung committed Jun 11, 2019 147 `````` (∃ n : nat, r ↦ #n ∗ own γ (●F n))%I. `````` Robbert Krebbers committed Jan 08, 2018 148 149 150 151 152 153 154 `````` (** *Exercise*: finish the missing cases of the proof. *) Lemma parallel_add_spec_3 : {{{ True }}} parallel_add {{{ RET #4; True }}}. Proof. iIntros (Φ) "_ Post". unfold parallel_add. wp_alloc r as "Hr". wp_let. `````` Ralf Jung committed Jun 11, 2019 155 `````` iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]". `````` Hai Dang committed May 24, 2019 156 `````` { by apply auth_both_valid. } `````` Robbert Krebbers committed Jan 08, 2018 157 158 159 `````` wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]"). { (* exercise *) iExists 0%nat. iFrame. } iIntros (l) "#Hl". wp_let. `````` Ralf Jung committed Jun 11, 2019 160 `````` wp_apply (wp_par (λ _, own γ (◯F{1/2} 2%nat)) (λ _, own γ (◯F{1/2} 2%nat)) `````` Robbert Krebbers committed Jan 08, 2018 161 162 163 `````` with "[Hγ1◯] [Hγ2◯]"). - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]". wp_seq. wp_load. wp_op. wp_store. `````` Ralf Jung committed Jun 11, 2019 164 `````` iMod (own_update_2 _ _ _ (●F (n+2) ⋅ ◯F{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]". `````` Robbert Krebbers committed Jan 08, 2018 165 166 167 168 169 170 171 `````` { rewrite (comm plus). by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. } wp_apply (release_spec with "[\$Hl Hr Hγ●]"); [|by auto]. iExists _. iFrame. by rewrite Nat2Z.inj_add. - (* exercise *) wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]". wp_seq. wp_load. wp_op. wp_store. `````` Ralf Jung committed Jun 11, 2019 172 `````` iMod (own_update_2 _ _ _ (●F (n+2) ⋅ ◯F{1/2}2)%nat with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]". `````` Robbert Krebbers committed Jan 08, 2018 173 174 175 176 177 178 179 180 181 182 183 184 `````` { rewrite (comm plus). by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. } wp_apply (release_spec with "[- \$Hl Hγ2◯]"); [|by auto]. iExists _. iFrame. by rewrite Nat2Z.inj_add. - (* exercise *) iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq. wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "(Hr & Hγ●)". wp_seq. wp_load. iCombine "Hγ1◯ Hγ2◯" as "Hγ◯". iDestruct (own_valid_2 with "Hγ● Hγ◯") as %->%frac_auth_agreeL. by iApply "Post". Qed. End proof3.``````