ex_03_spinlock.v 4.93 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
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's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
88
89
90
    (** We have to "focus on" the atomic [CmpXchg] operation before we can
    open the invariant. *)
    wp_bind (CmpXchg _ _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
102
    - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
103
      { iNext. iExists true. iFrame. }
104
      iModIntro. wp_proj.
105
106
      (* exercise *) admit.
    - (* exercise *) admit.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.