barrier_client.v 5.91 KB
Newer Older
1
From iris_automation.heap_lang Require Import stepping_tacs.
2
3
From iris_automation.biabd Require Import biabd_local_updates.
From iris.algebra Require Import frac_auth numbers csum agree.
4
From iris.heap_lang Require Import proofmode.
5
From iris_automation.lib Require Import frac_token int_as_nat_diff.
6
7
From iris_automation.examples.comparison Require Import barrier.

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
Definition increment : val := 
  rec: "inc" "c" := 
    let: "v" := ! "c" in
    if: CAS "c" "v" ("v" + #1) then 
      #()
    else 
      "inc" "c".

Definition decrement : val := 
  rec: "dec" "c" := 
    let: "v" := ! "c" in
    if: CAS "c" "v" ("v" - #1) then 
      #()
    else 
      "dec" "c".

Definition check_rising : val := 
  λ: "c",
    let: "a" := ! "c" in
    let: "b" := ! "c" in
    if: "b" < "a" then 
      #() #() (* unsafe *)
    else 
      #().

Definition check_falling : val := 
  λ: "c",
    let: "a" := ! "c" in
    let: "b" := ! "c" in
    if: "a" < "b" then 
      #() #() (* unsafe *)
    else 
      #().

42
Definition client_thread p : val := 
43
  λ: "c" "b",
44
    increment "c";;
45
46
47
    check_rising "c" ;;
    sync_up p "b" ;; 
    decrement "c" ;;
48
    check_falling "c".
49
50
51

Definition client_run p : val := 
  rec: "spawn_clients" "c" "b" "n" :=
52
53
54
    if: "n" = #0 
    then 
      #()
55
    else 
56
      Fork (client_thread p "c" "b") ;;
57
58
      "spawn_clients" "c" "b" ("n" - #1).

59
60
61
62
63
Definition client p : val := 
  λ: <>, 
    let: "c" := ref #0 in
    let: "b" := make_barrier #() in
    client_run p "c" "b" #(Zpos p).
64
65
66
67
68
69
70
71
72
73

Definition barrier_clientUR := frac_authUR $ prodR (csumR max_natR max_natR) $ agreeR natO.
Class barrier_clientG Σ :=
  BarrierClientG { 
    barrier_client_clientG :> inG Σ barrier_clientUR;
    barrier_client_barrierG :> barrierG Σ
  }.
Definition barrier_clientΣ : gFunctors :=
  #[GFunctor barrier_clientUR; barrierΣ].

74
75
76
Local Obligation Tactic := program_smash_verify.

Program Instance subG_barrier_clientΣ {Σ} : subG barrier_clientΣ Σ  barrier_clientG Σ.
77
78
79

Section proof.
  Context `{!heapGS Σ, barrier_clientG Σ}.
80
  Let N := nroot.@"client".
81
82

  Definition counter_inv γ (l : loc) : iProp Σ :=
83
     (z : Z), l  #z   (n1 n2 : nat), int_as_nat_diff z n1 n2 
84
85
86
87
88
89
90
91
      (own γ (F (Cinl $ MaxNat n1, to_agree n2))  own γ (F (Cinr $ MaxNat n2, to_agree n1))).

  Definition P1 γ : Qp  iProp Σ := λ q,
    ( (n1 n2 : nat), own γ (F{q} (Cinl $ MaxNat n1, to_agree n2)))%I.

  Definition P2 γ : Qp  iProp Σ := λ q,
    ( (n1 n2 : nat), own γ (F{q} (Cinr $ MaxNat n1, to_agree n2)))%I.

92
93
  Hint Extern 4 (_  _)%nat => eapply Nat.le_refl : solve_pure_add.

94
  Lemma p1_fractional γ : Fractional (P1 γ).
95
  Proof. rewrite /Fractional => p q. apply (anti_symm _); iStepsS. Qed.
96
  Lemma p2_fractional γ : Fractional (P2 γ).
97
  Proof. rewrite /Fractional => p q. apply (anti_symm _); iStepsS. Qed.
98
  Existing Instance p1_fractional. Existing Instance p2_fractional.
99
100
101
102

  Definition is_counter_barrier threads γp1 γp2 γt γb (v : val) γc : iProp Σ :=
    is_barrier (P1 γc) (P2 γc) threads γp1 γp2 γt γb (v : val).

103
  Program Instance increment_spec γc (l : loc) :
104
    SPEC q, {{ P1 γc q  inv N (counter_inv γc l) }}
105
106
107
108
      increment #l
    {{ RET #(); P1 γc q }}.

  Instance check_rising_spec γc (l : loc) :
109
    SPEC q, {{ P1 γc q  inv N (counter_inv γc l) }}
110
111
112
113
114
      check_rising #l
    {{ RET #(); P1 γc q }}.
  Proof.
    iStepsS.
    assert (x8 = x8 `max` x1) by lia. rewrite {2}H1.
115
    iLeft. iStepS. rewrite -H1. iSmash.
116
117
  Qed.

118
  Program Instance decrement_spec γc (l : loc) :
119
    SPEC q, {{ P2 γc q  inv N (counter_inv γc l) }}
120
121
122
123
      decrement #l
    {{ RET #(); P2 γc q }}.

  Instance check_falling_spec γc (l : loc) :
124
    SPEC q, {{ P2 γc q  inv N (counter_inv γc l) }}
125
126
127
128
129
      check_falling #l
    {{ RET #(); P2 γc q }}.
  Proof.
    iStepsS.
    assert (x9 = x9 `max` x1) by lia. rewrite {3}H1.
130
    iRight. iStepS. rewrite -H1. iSmash.
131
132
  Qed.

133
  Opaque P1 P2.
134

135
  Program Instance client_thread_spec threads γp1 γp2 γt γb (v : val) γc (l : loc) :
136
    SPEC {{ is_counter_barrier threads γp1 γp2 γt γb v γc  token (P1 γc) γp1  inv N (counter_inv γc l) }}
137
138
      client_thread threads #l v
    {{ RET #(); token (P2 γc) γp2 }}.
139
140
141
142
143
144
145
146
147

  Instance client_run_spec threads γp1 γp2 γt γb (v : val) γc (l : loc) (z : Z) :
    SPEC {{ is_counter_barrier threads γp1 γp2 γt γb v γc  0  z%Z  
          token_iter (P1 γc) (Z.to_nat z) γp1  inv N (counter_inv γc l) }}
      client_run threads #l v #z
    {{ RET #(); True }}.
  Proof.
    iStepsS. rewrite -{2}(Z2Nat.id z) //.
    generalize (Z.to_nat z) => n.
148
    iInduction n as [|n] "IH"; wp_lam; first iStepsS.
149
150
151
152
153
154
    change (token_iter (P1 γc) (S n) γp1) with (token (P1 γc) γp1  token_iter (P1 γc) n γp1)%I.
    iStepsS.
    replace (NtoZ (S n) - 1)%Z with (NtoZ n) by lia.
    iStepsS.
  Qed.

155
156
157
  Transparent P1 P2. 
  (* currently needed because of bug in repeated applications of into_texist; notypeclasses refine works, simple eapply does not.
     problem occurs for biabd_exist lemma, and for TeleSummarize typeclass *)
158
159
160
161
162
163
164

  Instance client_spec threads :
    SPEC {{ True }}
      client threads #()
    {{ RET #(); True }}.
  Proof.
    iStepsS.
165
166
167
    iAssert (|={}=>  γc, inv N (counter_inv γc x0)  P1 γc 1)%I with "[H2]" as ">[%γc [#HI [%n1 [%n2 HPn]]]]".
    { iSmash. }
    assert (H' := newbarrier_spec (P1 γc) (P2 γc) threads).
168
169
170
    iStepS.
    iStepS.
    rewrite /SolveSep /=.
171
    iSplitR; [ | iSplitR; iIntros "!>"; [ | iStepsS]].
172
173
    - iIntros "!> !>". iStepS. 
      iInv N as "HN". iRevert "HN".
174
      iStepsS; case: H0 => /= H1 H2; simplify_eq.
175
176
      apply biabd_local_updates.agree_equiv in H2. fold_leibniz. subst.
      iRight. iStepsS.
177
    - iIntros "!> !>". iStepS. 
178
      iInv N as "HN". iRevert "HN".
179
      iStepsS; case: H0 => /= H1 H2; simplify_eq.
180
      apply biabd_local_updates.agree_equiv in H2. fold_leibniz. subst.
181
      iSmash.
182
    Unshelve. all: apply inhabitant.
183
184
185
186
187
  Qed.
End proof.