ex_04_parallel_add.v 5.85 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 exercises Require Import ex_03_spinlock.
Robbert Krebbers's avatar
Robbert Krebbers committed
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

(** 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 *)
      admit. }
    iIntros (l) "#Hl". wp_let.
Ralf Jung's avatar
Ralf Jung committed
42
    wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
    - 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 *)
      admit.
    - (* exercise *)
      admit.
  Admitted.
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:

61
  inG Σ (excl_authR ZO)
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65

*)

Section proof2.
66
  Context `{!heapG Σ, !spawnG Σ, !inG Σ (excl_authR ZO)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69

  Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ :=
    ( n1 n2 : Z, r  #(n1 + n2)
70
             own γ1 (E n1)  own γ2 (E n2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
74
75

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

  Lemma ghost_var_agree γ n m :
84
    own γ (E n) - own γ (E m) -  n = m .
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
  Proof.
    iIntros "Hγ● Hγ◯".
87
    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agreeL.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
  Qed.

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

  (** *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
140
    iMod (own_alloc (F 0  F 0)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
Hai Dang's avatar
Hai Dang committed
141
    { by apply auth_both_valid. }
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
145
    wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
    { (* exercise *)
      admit. }
    iIntros (l) "#Hl". wp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
    wp_apply (wp_par (λ _, own γ (F{1/2} 2)) (λ _, own γ (F{1/2} 2))
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
149
                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
150
      iMod (own_update_2 _ _ _ (F (n+2)  F{1/2}2) with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
Robbert Krebbers's avatar
Robbert Krebbers committed
151
      { rewrite (comm plus).
Robbert Krebbers's avatar
Robbert Krebbers committed
152
        by apply frac_auth_update, (op_local_update_discrete n 0 2). }
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
157
158
159
160
      wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto].
      iExists _. iFrame. by rewrite Nat2Z.inj_add.
    - (* exercise *)
      admit.
    - (* exercise *)
      admit.
  Admitted.
End proof3.