ex_03_spinlock.v 4.93 KB
 Robbert Krebbers committed Jan 08, 2018 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 ``````(** In this exercise, we prove the correctness of a spin lock module. *) From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import proofmode notation. Definition newlock : val := λ: <>, ref #false. Definition try_acquire : val := λ: "l", CAS "l" #false #true. Definition acquire : val := rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l". Definition release : val := λ: "l", "l" <- #false. (** As shown, the spin lock is implemented as a reference to a Boolean. If the Boolean is [true], it means some thread has acquired the lock/entered the critical section. We initiate the lock with the value [false], which means that the lock is initially in the unlocked state. The most interesting function of the spin lock is [acquire], which checks if the lock is in the unlocked state, and if not, changes the lock into [true]. Since multiple threads could try to acquire the lock at the same time, we use the [CAS l v w] (compare-and-set) instruction. This instruction atomically checks if the value of the reference [l] is equal to [v], and if so, changes it into [w] and returns [true]. If the value of [l] is unequal to [v], it leaves the value of [l] as if, and returns [false]. `````` Ralf Jung committed Jun 24, 2019 30 31 ``````[CAS l v w] is actually a short-hand for [Snd (CmpXchg l v w)], where [CmpXchg] also returns the old value in [l] before the operation took place. `````` Robbert Krebbers committed Jan 08, 2018 32 33 34 35 36 37 38 39 40 41 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 82 83 84 85 86 87 ``````*) (** We will prove the following lock specification in Iris: {{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}. {{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}} {{{ is_lock lk R ∗ R }}} release lk {{{ RET #(); True }}}. Here, [is_lock lk R] is a representation predicate which says that a lock at location [lk] guards the payload [R] described as an Iris proposition. *) Section proof. Context `{!heapG Σ}. (** The invariant of the lock: - It owns the memory location [l ↦ #b], which contain a Boolean [b], - If the Boolean [b] is [false] (the lock is in the unlocked state), then the payload [R] of the lock holds. *) Definition lock_inv (l : loc) (R : iProp Σ) : iProp Σ := (∃ b : bool, l ↦ #b ∗ if b then True else R)%I. (** Invariants in Iris are named by a *namespace* so that several invariants can be opened at the same time, while guaranteeing that no invariant is opened twice at the same time (which would be unsound). Here, this is irrelevant, since acquiring and releasing a lock only requires to open one invariant. The namespace [lockN] of the lock invariant: *) Definition lockN : namespace := nroot .@ "lock". Definition is_lock (lk : val) (R : iProp Σ) : iProp Σ := (∃ l: loc, ⌜ lk = #l ⌝ ∧ inv lockN (lock_inv l R))%I. (** The main proofs. *) Lemma newlock_spec (R : iProp Σ): {{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}. Proof. iIntros (Φ) "HR HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl". (** Use the Iris rule [inv_alloc] for allocating a lock. We put both the resources [HR : R] and the points-to [l ↦ #false] into the lock. *) iMod (inv_alloc lockN _ (lock_inv l R) with "[HR Hl]") as "#Hinv". { iNext. iExists false. iFrame. } iModIntro. iApply "HΦ". iExists l. eauto. Qed. (** *Exercise*: finish the proof below. *) Lemma try_acquire_spec lk R : {{{ is_lock lk R }}} try_acquire lk {{{ b, RET #b; if b is true then R else True }}}. Proof. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv". wp_rec. `````` Ralf Jung committed Jun 24, 2019 88 89 90 `````` (** We have to "focus on" the atomic [CmpXchg] operation before we can open the invariant. *) wp_bind (CmpXchg _ _ _). `````` Robbert Krebbers committed Jan 08, 2018 91 92 93 94 95 96 97 98 99 100 101 `````` (** Using the tactic [iInv] we open the invariant. *) iInv lockN as (b) "[Hl HR]" "Hclose". (** The post-condition of the WP is augmented with an *update* modality [ |={⊤ ∖ ↑lockN,⊤}=> ... ], which keeps track of the fact that we opened the invariant named [lockN]. We can introduce this update modality by closing the lock using the hypothesis: "Hclose" : ▷ lock_inv l R ={⊤ ∖ ↑lockN,⊤}=∗ True *) destruct b. `````` Ralf Jung committed Jun 24, 2019 102 `````` - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_". `````` Robbert Krebbers committed Jan 08, 2018 103 `````` { iNext. iExists true. iFrame. } `````` Ralf Jung committed Aug 06, 2020 104 `````` iModIntro. wp_proj. `````` Ralf Jung committed Aug 28, 2020 105 106 `````` (* exercise *) admit. - (* exercise *) admit. `````` Robbert Krebbers committed Jan 08, 2018 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 `````` Admitted. (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive function, you should use the tactic [iLöb] for Löb induction. Use the tactic [wp_apply] to use [try_acquire_spec] when appropriate. *) Lemma acquire_spec lk R : {{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}. Proof. (* exercise *) Admitted. (** *Exercise*: prove the spec of [release]. At a certain point in this proof, you need to open the invariant. For this you can use: iInv lockN as (b) "[Hl HR]" "Hclose". In the same way as in the proof of [try_acquire]. You also need to close the invariant. *) Lemma release_spec lk R : {{{ is_lock lk R ∗ R }}} release lk {{{ RET #(); True }}}. Proof. (* exercise *) Admitted. End proof.``````