barrier_client.v 5.57 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
Local Obligation Tactic := program_smash_verify.

76
Global 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
      check_rising #l
    {{ RET #(); P1 γc q }}.
  Proof.
    iStepsS.
Ike Mulder's avatar
Ike Mulder committed
114
    assert (x5 = x5 `max` x0) as Hx8 by lia. rewrite {2}Hx8.
115
    iLeft. iStepS. rewrite -Hx8. 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
      check_falling #l
    {{ RET #(); P2 γc q }}.
  Proof.
    iStepsS.
Ike Mulder's avatar
Ike Mulder committed
129
    assert (x6 = x6 `max` x0) as Hx9 by lia. rewrite {3}Hx9.
130
    iRight. iStepS. rewrite -Hx9. iSmash.
131
132
  Qed.

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

  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.
146
    iInduction n as [|n] "IH"; wp_lam; first iStepsS.
147
148
149
150
151
152
    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.

153
  Global Instance client_spec threads :
154
155
156
157
158
    SPEC {{ True }}
      client threads #()
    {{ RET #(); True }}.
  Proof.
    iStepsS.
Ike Mulder's avatar
Ike Mulder committed
159
    iAssert (|={}=>  γc, inv N (counter_inv γc x)  P1 γc 1)%I with "[H1]" as ">[%γc [#HI [%n1 [%n2 HPn]]]]".
160
161
    { iSmash. }
    assert (H' := newbarrier_spec (P1 γc) (P2 γc) threads).
162
163
    iStepS.
    iStepS.
164
    unseal_diaframe => /=.
165
    iSplitR; [ | iSplitR; iIntros "!>"; [ | iStepsS]].
Ike Mulder's avatar
Ike Mulder committed
166
    - iStepS. iStepS. 
167
      iInv N as "HN". iRevert "HN".
168
      iStepsS; case: H0 => /= H1 /to_agree_equiv H2; simplify_eq.
169
      iRight. iStepsS.
Ike Mulder's avatar
Ike Mulder committed
170
    - iStepS. iStepS.
171
      iInv N as "HN". iRevert "HN".
172
      iStepsS; case: H0 => /= H1 /to_agree_equiv H2; simplify_eq.
173
      iSmash.
174
    Unshelve. all: apply inhabitant.
175
176
177
178
179
  Qed.
End proof.