ex_04_parallel_add.v 7.6 KB
Newer Older
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.
*)
6
From iris.algebra Require Import excl_auth frac_auth.
7
8
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation.
Ralf Jung's avatar
Ralf Jung committed
9
From solutions Require Import ex_03_spinlock.
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's avatar
Ralf Jung committed
41
    wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
    - 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:

Robbert Krebbers's avatar
Robbert Krebbers committed
65
  inG Σ (authR (optionUR (exclR ZO)))
66
67
68
69

*)

Section proof2.
70
  Context `{!heapG Σ, !spawnG Σ, !inG Σ (excl_authR ZO)}.
71
72
73

  Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ :=
    ( n1 n2 : Z, r  #(n1 + n2)
74
             own γ1 (E n1)  own γ2 (E n2))%I.
75
76
77
78
79

  (** 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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
80
     |==>  γ, own γ (E n)  own γ (E n).
81
  Proof.
82
83
    iMod (own_alloc (E n  E n)) as (γ) "[??]".
    - by apply excl_auth_valid.
Hai Dang's avatar
Hai Dang committed
84
    - by eauto with iFrame.
85
86
87
  Qed.

  Lemma ghost_var_agree γ n m :
88
    own γ (E n) - own γ (E m) -  n = m .
89
90
  Proof.
    iIntros "Hγ● Hγ◯".
91
    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agreeL.
92
93
94
  Qed.

  Lemma ghost_var_update γ n' n m :
95
    own γ (E n) - own γ (E m) == own γ (E n')  own γ (E n').
96
97
  Proof.
    iIntros "Hγ● Hγ◯".
98
99
    iMod (own_update_2 _ _ _ (E n'  E n') with "Hγ● Hγ◯") as "[$$]".
    { by apply excl_auth_update. }
100
101
102
103
104
105
106
107
108
109
110
111
112
113
    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.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
    wp_apply (wp_par (λ _, own γ1 (E 2%Z)) (λ _, own γ2 (E 2%Z))
115
116
117
118
119
120
                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].
Robbert Krebbers's avatar
Robbert Krebbers committed
121
      iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2)%Z; [done|ring].
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
    - (* 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 Σ :=
145
    ( n : nat, r  #n  own γ (F n))%I.
146
147
148
149
150
151
152

  (** *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.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
    iMod (own_alloc (F 0  F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
Hai Dang's avatar
Hai Dang committed
154
    { by apply auth_both_valid. }
155
    wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
Robbert Krebbers's avatar
Robbert Krebbers committed
156
    { (* exercise *) iExists 0. iFrame. }
157
    iIntros (l) "#Hl". wp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
    wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2))
159
160
161
                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.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
      iMod (own_update_2 _ _ _ (F (n+2)  F{1/2}2) with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
163
      { rewrite (comm plus).
Robbert Krebbers's avatar
Robbert Krebbers committed
164
        by apply frac_auth_update, (op_local_update_discrete n 0 2). }
165
166
167
168
169
      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.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
      iMod (own_update_2 _ _ _ (F (n+2)  F{1/2}2) with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]".
171
      { rewrite (comm plus).
Robbert Krebbers's avatar
Robbert Krebbers committed
172
        by apply frac_auth_update, (op_local_update_discrete n 0 2). }
173
174
175
176
177
178
179
180
181
182
      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.