part4.v 5.35 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.
From iris.algebra Require Import frac_auth.
Local Definition N := nroot .@ "example".

(* PART 4: Parellel increment (from JH's talk) *)
Definition par_inc : val := λ: <>,
  let: "l" := ref #0 in
  (FAA "l" #2 ||| FAA "l" #2);;
  !"l".

Section proof1.
  Context `{heapG Σ, spawnG Σ}.

  Lemma Zeven_2 : Zeven 2.
  Proof. done. Qed.
17
  Hint Resolve Zeven_2 Zeven_plus_Zeven : core.
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

  Lemma par_inc_even_spec :
    {{{ True }}} par_inc #() {{{ n, RET #n;  Zeven n  }}}.
  Proof.
    iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
    iMod (inv_alloc N _ ( n : Z, l  #n   Zeven n )%I with "[Hl]") as "#?".
    { iExists 0. auto. }
    wp_bind (_ ||| _)%E.
    wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
    - iInv N as (n) ">[Hl %]" "Hclose".
      wp_faa. iMod ("Hclose" with "[Hl]"); first eauto 10.
      auto.
    - iInv N as (n) ">[Hl %]" "Hclose".
      wp_faa. iMod ("Hclose" with "[Hl]"); first eauto 10.
      auto.
    - iIntros (v1 v2) "_". iNext. wp_seq.
      iInv N as (n) ">[Hl %]" "Hclose".
      wp_load. iMod ("Hclose" with "[Hl]"); first eauto 10.
      iApply "Post"; auto.
  Qed.
End proof1.

(* PART 5: Better parellel increment *)
Definition par_incN_helper : val :=
  rec: "helper" "n" "l" :=
    if: "n" = #0 then #()
    else (FAA "l" #2 ||| "helper" ("n" - #1) "l").
Definition par_incN : val := λ: "n",
  let: "l" := ref #0 in
  par_incN_helper "n" "l";;
  !"l".

Section proof2.
  Context `{heapG Σ, spawnG Σ, inG Σ (frac_authR natR)}.
  Implicit Types n : nat.

  (* Rules for fractional ghost variables
     (proved from generic principles) *)
  Lemma frac_auth_alloc n :
Robbert Krebbers's avatar
Robbert Krebbers committed
57
     |==>  γ, own γ (F n)  own γ (F{1} n).
58
  Proof.
59
60
    iMod (own_alloc (F n  F n)) as (γ) "[??]"; eauto with iFrame.
    by apply frac_auth_valid.
61
62
63
  Qed.

  Lemma frac_auth_update n n1 n2 q γ :
64
65
    own γ (F n1) -
    own γ (F{q} n2) - |==>
Robbert Krebbers's avatar
Robbert Krebbers committed
66
    own γ (F (n1 + n))  own γ (F{q} (n2 + n)).
67
68
69
70
71
72
  Proof.
    iIntros "H H'". iMod (own_update_2 with "H H'") as "[$ $]"; last done.
    apply frac_auth_update, nat_local_update. lia.
  Qed.

  Lemma frac_auth_agree n n' γ :
73
    own γ (F n) - own γ (F{1} n') - n = n'.
74
75
76
77
78
79
80
  Proof.
    iIntros "H H'".
    by iDestruct (own_valid_2 with "H H'") as %->%frac_auth_agreeL.
  Qed.

  (* The invariant that we use *)
  Definition proof2_inv (γ : gname) (l : loc) : iProp Σ :=
81
    ( n : nat, own γ (F n)  l  #n)%I.
82
83
84

  (* Proof of the threads *)
  Lemma par_inc_FAA_spec n n' γ l q :
85
    {{{ inv N (proof2_inv γ l)  own γ (F{q} n) }}}
86
      FAA #l #n'
Robbert Krebbers's avatar
Robbert Krebbers committed
87
    {{{ m, RET #m; own γ (F{q} (n + n')) }}}.
88
89
90
91
92
  Proof.
    iIntros (Φ) "[#Hinv Hγ] Post". iInv N as (m) ">[Hauth Hl]" "Hclose".
    wp_faa.
    iMod (frac_auth_update n' with "Hauth Hγ") as "[Hauth Hγ]".
    iMod ("Hclose" with "[Hauth Hl]") as "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    { iNext; iExists (m + n'). rewrite Nat2Z.inj_add. iFrame. }
94
95
96
97
98
    by iApply "Post".
  Qed.

  (* Proof of the whole program *)
  Lemma par_inc_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
99
    {{{ True }}} par_inc #() {{{ RET #4; True }}}.
100
101
102
103
104
  Proof.
    iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
    iMod (frac_auth_alloc 0) as (γ) "[Hauth Hγ]".
    iDestruct "Hγ" as "[Hγ1 Hγ2]".
    iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
    { iNext. iExists 0. iFrame. }
    wp_apply (wp_par (λ _, own γ (F{1/2} 2))
                     (λ _, own γ (F{1/2} 2)) with "[Hγ1] [Hγ2]").
108
109
110
111
112
113
114
    - iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
    - iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
    - iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ". simpl.
      wp_seq. iInv N as (m) ">[Hauth Hx]" "Hclose".
      iDestruct (frac_auth_agree with "Hauth Hγ") as %->.
      wp_load.
      iMod ("Hclose" with "[Hauth Hx]") as "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
115
      { iNext. iExists 4. iFrame. }
116
117
118
119
      by iApply "Post".
  Qed.

  Lemma par_incN_helper_spec n γ l q :
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    {{{ inv N (proof2_inv γ l)  own γ (F{q} 0) }}}
121
      par_incN_helper #n #l
Robbert Krebbers's avatar
Robbert Krebbers committed
122
    {{{ v, RET v; own γ (F{q} (n * 2)) }}}.
123
124
125
  Proof.
    iIntros (Φ) "[#? Hγ] Post /=".
    iInduction n as [|n] "IH" forall (q Φ).
126
127
128
    { wp_lam. wp_pures. by iApply "Post". }
    rewrite Nat2Z.inj_succ. wp_lam. wp_pures.
    case_bool_decide; first (simplify_eq/=; lia). wp_if.
129
    iDestruct "Hγ" as "[Hγ1 Hγ2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
    wp_apply (wp_par (λ _, own γ (F{q/2} 2))
                     (λ _, own γ (F{q/2} (n * 2))) with "[Hγ1] [Hγ2]").
132
    - iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
133
    - wp_op. rewrite (_ : Z.succ n - 1 = n)%Z; last lia.
134
135
136
137
138
139
140
141
142
143
144
      iApply ("IH" with "Hγ2"); auto.
    - iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ".
      by iApply "Post".
  Qed.

  Lemma par_incN_spec n :
    {{{ True }}} par_incN #n {{{ RET #(n * 2)%nat; True }}}.
  Proof.
    iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
    iMod (frac_auth_alloc 0) as (γ) "[Hauth Hγ]".
    iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
145
    { iNext. iExists 0. iFrame. }
146
147
148
149
150
151
    wp_apply (par_incN_helper_spec with "[$]").
    iIntros (v) "Hγ". wp_seq.
    iInv N as (m) ">[Hauth Hx]" "Hclose".
    iDestruct (frac_auth_agree with "Hauth Hγ") as %->.
    wp_load.
    iMod ("Hclose" with "[Hauth Hx]") as "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    { iNext. iExists (n * 2). iFrame. }
153
154
155
    by iApply "Post".
  Qed.
End proof2.