barrier.v 7.62 KB
Newer Older
1
From algebra Require Export upred_big_op.
2
From program_logic Require Export sts saved_prop.
3
From heap_lang Require Export derived heap wp_tactics notation.
Ralf Jung's avatar
Ralf Jung committed
4
Import uPred.
5
6
7

Definition newchan := (λ: "", ref '0)%L.
Definition signal := (λ: "x", "x" <- '1)%L.
8
Definition wait := (rec: "wait" "x" :=if: !"x" = '1 then '() else "wait" "x")%L.
9

10
11
12
(** The STS describing the main barrier protocol. Every state has an index-set
    associated with it. These indices are actually [gname], because we use them
    with saved propositions. *)
13
Module barrier_proto.
14
15
  Inductive phase := Low | High.
  Record stateT := State { state_phase : phase; state_I : gset gname }.
16
17
  Inductive token := Change (i : gname) | Send.

18
19
20
  Global Instance stateT_inhabited: Inhabited stateT.
  Proof. split. exact (State Low ). Qed.

21
  Definition change_tokens (I : gset gname) : set token :=
Ralf Jung's avatar
Ralf Jung committed
22
    mkSet (λ t, match t with Change i => i  I | Send => False end).
23

24
25
26
  Inductive trans : relation stateT :=
  | ChangeI p I2 I1 : trans (State p I1) (State p I2)
  | ChangePhase I : trans (State Low I) (State High I).
27

28
29
30
  Definition tok (s : stateT) : set token :=
      change_tokens (state_I s)
     match state_phase s with Low =>  | High => {[ Send ]} end.
31

Robbert Krebbers's avatar
Robbert Krebbers committed
32
  Canonical Structure sts := sts.STS trans tok.
33

34
  (* The set of states containing some particular i *)
35
36
37
38
  Definition i_states (i : gname) : set stateT :=
    mkSet (λ s, i  state_I s).

  Lemma i_states_closed i :
Robbert Krebbers's avatar
Robbert Krebbers committed
39
    sts.closed (i_states i) {[ Change i ]}.
40
41
  Proof.
    split.
42
    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
Ralf Jung's avatar
Ralf Jung committed
43
44
45
46
47
      apply lookup_singleton.
    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
      move=>s' /elem_of_intersection. rewrite !mkSet_elem_of /=.
      move=>[[Htok|Htok] ? ]; subst s'; first done.
      destruct p; done.
48
49
50
51
52
    - (* If we do the destruct of the states early, and then inversion
         on the proof of a transition, it doesn't work - we do not obtain
         the equalities we need. So we destruct the states late, because this
         means we can use "destruct" instead of "inversion". *)
      move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
Ralf Jung's avatar
Ralf Jung committed
53
54
      (* We probably want some helper lemmas for this... *)
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
55
56
      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
      destruct Htrans; last done; move:Hs1 Hdisj Htok.
Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
62
63
64
65
66
      rewrite /= /tok /=.
      intros. apply dec_stable. 
      assert (Change i  change_tokens I1) as HI1
        by (rewrite mkSet_not_elem_of; solve_elem_of +Hs1).
      assert (Change i  change_tokens I2) as HI2.
      { destruct p.
        - solve_elem_of +Htok Hdisj HI1.
        - solve_elem_of +Htok Hdisj HI1 / discriminate. }
      done.
  Qed.
67
68
69
70

  (* The set of low states *)
  Definition low_states : set stateT :=
    mkSet (λ s, if state_phase s is Low then True else False).
71
72

  Lemma low_states_closed : sts.closed low_states {[ Send ]}.
73
74
75
76
77
78
79
80
81
82
83
84
85
  Proof.
    split.
    - apply (non_empty_inhabited(State Low )). by rewrite !mkSet_elem_of /=.
    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
      destruct p; last done. solve_elem_of+ /discriminate.
    - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
      destruct Htrans; move:Hs1 Hdisj Htok =>/=;
                                first by destruct p.
      rewrite /= /tok /=. intros. solve_elem_of +Hdisj Htok.
  Qed.

86
End barrier_proto.
87
88
89
90
91
92
(* I am too lazy to type the full module name all the time. But then
   why did we even put this into a module? Because some of the names 
   are so general.
   What we'd really like here is to import *some* of the names from
   the module into our namespaces. But Coq doesn't seem to support that...?? *)
Import barrier_proto.
93

94
95
96
97
98
(** Now we come to the Iris part of the proof. *)
Section proof.
  Context {Σ : iFunctorG} (N : namespace).
  (* TODO: Bundle HeapI and HeapG and have notation so that we can just write
     "l ↦ '0". *)
99
100
101
  Context `{heapG Σ} (HeapN : namespace).
  Context `{stsG heap_lang Σ sts}.
  Context `{savedPropG heap_lang Σ}.
Ralf Jung's avatar
Ralf Jung committed
102
103
104
  (* TODO We could alternatively construct the namespaces to be disjoint.
     But that would take a lot of flexibility from the client, who probably
     wants to also use the heap_ctx elsewhere. *)
105
  Context (HeapN_disj : HeapN  N).
Ralf Jung's avatar
Ralf Jung committed
106

107
108
109
  Notation iProp := (iPropG heap_lang Σ).

  Definition waiting (P : iProp) (I : gset gname) : iProp :=
110
    ( R : gname  iProp, (P - Π★{set I} (λ i, R i)) 
111
                             Π★{set I} (λ i, saved_prop_own i (R i)))%I.
112
113

  Definition ress (I : gset gname) : iProp :=
114
    (Π★{set I} (λ i,  R, saved_prop_own i R  R))%I.
115

116
117
  Local Notation state_to_val s :=
    (match s with State Low _ => 0 | State High _ => 1 end).
118
  Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
119
    (l  '(state_to_val s) 
120
121
     match s with State Low I' => waiting P I' | State High I' => ress I' end
    )%I.
122
123

  Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
124
    (heap_ctx HeapN  sts_ctx γ N (barrier_inv l P))%I.
125
126

  Definition send (l : loc) (P : iProp) : iProp :=
127
    ( γ, barrier_ctx γ l P  sts_ownS γ low_states {[ Send ]})%I.
128
129

  Definition recv (l : loc) (R : iProp) : iProp :=
130
131
132
    ( γ (P Q : iProp) i, barrier_ctx γ l P  sts_ownS γ (i_states i) {[ Change i ]} 
        saved_prop_own i Q  (Q - R))%I.

Ralf Jung's avatar
Ralf Jung committed
133
  Lemma newchan_spec (P : iProp) (Q : val  iProp) :
134
    ( l, recv l P  send l P - Q (LocV l))  wp  (newchan '()) Q.
Ralf Jung's avatar
Ralf Jung committed
135
136
137
138
  Proof.
  Abort.

  Lemma signal_spec l P (Q : val  iProp) :
139
    (send l P  P  Q '())  wp  (signal (LocV l)) Q.
Ralf Jung's avatar
Ralf Jung committed
140
  Proof.
Ralf Jung's avatar
Ralf Jung committed
141
142
143
    rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
    apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
    (* I think some evars here are better than repeating *everything* *)
144
    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
145
    { solve_elem_of+. (* FIXME eauto should do this *) }
146
    rewrite [(_  sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
Ralf Jung's avatar
Ralf Jung committed
147
148
149
    apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
    apply const_elim_sep_l=>Hs. destruct p; last done.
    rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
Ralf Jung's avatar
Ralf Jung committed
150
151
152
153
154
155
156
157
    eapply wp_store; eauto with I.
    { (* FIXME can we make this more automatic? *)
      apply ndisj_disjoint in HeapN_disj. solve_elem_of. }
    rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
    { (* Is this really the best way to strip the later? *)
      erewrite later_sep. apply sep_mono_r. apply later_intro. }
    apply wand_intro_l. rewrite -(exist_intro (State High I)).
    rewrite -(exist_intro ). rewrite const_equiv /=; last first.
158
    { constructor; first constructor; rewrite /= /tok /=; solve_elem_of. }
Ralf Jung's avatar
Ralf Jung committed
159
160
161
162
163
164
165
166
    rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
    rewrite !assoc [(_  P)%I]comm !assoc -2!assoc.
    apply sep_mono; last first.
    { apply wand_intro_l. eauto with I. }
    (* Now we come to the core piece of the proof: Updating from waiting to ress. *)
    rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Q} Q.
    rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
    (* TODO: Now we need stuff about Π★{set I} *)
Ralf Jung's avatar
Ralf Jung committed
167
168
169
  Abort.

  Lemma wait_spec l P (Q : val  iProp) :
170
    (recv l P  (P - Q '()))  wp  (wait (LocV l)) Q.
Ralf Jung's avatar
Ralf Jung committed
171
172
173
174
  Proof.
  Abort.

  Lemma split_spec l P1 P2 Q :
175
    (recv l (P1  P2)  (recv l P1  recv l P2 - Q '()))  wp  Skip Q.
Ralf Jung's avatar
Ralf Jung committed
176
177
178
179
180
181
182
  Proof.
  Abort.

  Lemma recv_strengthen l P1 P2 :
    (P1 - P2)  (recv l P1 - recv l P2).
  Proof.
  Abort.
183
184

End proof.