ex_03_spinlock.v 5.13 KB
Newer Older
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 30 31 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 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
(**
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].
*)

(**
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.
    (** 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.
    - wp_cas_fail. iMod ("Hclose" with "[Hl]") as "_".
      { iNext. iExists true. iFrame. }
      iModIntro. iApply ("HΦ" $! false). done.
    - (* Exercise *) wp_cas_suc.
      iMod ("Hclose" with "[Hl]") as "_".
      { iNext. iExists true. iFrame. }
      iModIntro. by iApply ("HΦ" $! true with "HR").
  Qed.

  (** *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.
    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
    - iIntros "HR". wp_if. by iApply "HΦ".
    - iIntros "_". wp_if. iApply ("IH" with "HΦ").
  Qed.

  (** *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.
    iIntros (Φ) "(Hlock & HR) HΦ".
    iDestruct "Hlock" as (l ->) "#Hinv /=".
    wp_lam. iInv lockN as (b) "[Hl _]" "Hclose".
    wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. iFrame.
  Qed.
End proof.