barrier.v 5.05 KB
Newer Older
1
From program_logic Require Export sts saved_prop.
2
3
4
5
From heap_lang Require Export derived heap wp_tactics notation.

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

8
9
10
(** 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. *)
11
Module barrier_proto.
12
13
  Inductive phase := Low | High.
  Record stateT := State { state_phase : phase; state_I : gset gname }.
14
15
  Inductive token := Change (i : gname) | Send.

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

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

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

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

  Definition sts := sts.STS trans tok.
31

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

  Lemma i_states_closed i :
    sts.closed sts (i_states i) {[ Change i ]}.
  Proof.
    split.
40
    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
Ralf Jung's avatar
Ralf Jung committed
41
42
43
44
45
      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.
46
47
48
49
50
    - (* 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
51
52
      (* We probably want some helper lemmas for this... *)
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
53
54
      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
      destruct Htrans; last done; move:Hs1 Hdisj Htok.
Ralf Jung's avatar
Ralf Jung committed
55
56
57
58
59
60
61
62
63
64
      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.
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

  (* The set of low states *)
  Definition low_states : set stateT :=
    mkSet (λ s, if state_phase s is Low then True else False).
  
  Lemma low_states_closed :
    sts.closed sts low_states {[ Send ]}.
  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.

85
End barrier_proto.
86
87
88
89
90
91
(* 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.
92

93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
(** 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". *)
  Context (HeapI : gid) `{!HeapInG Σ HeapI} (HeapG : gname).
  Context (StsI : gid) `{!sts.InG heap_lang Σ StsI sts}.
  Context (SpI : gid) `{!SavedPropInG heap_lang Σ SpI}.

  Notation iProp := (iPropG heap_lang Σ).

  Definition waiting (P : iProp) (I : gset gname) : iProp :=
    ( Q : gmap gname iProp, True)%I.

  Definition ress (I : gset gname) : iProp :=
    (True)%I.

  Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
    match s with
    | State Low I' => (heap_mapsto HeapI HeapG l ('0)  waiting P I')%I
    | State High I' => (heap_mapsto HeapI HeapG l ('1)  ress I')%I
    end.

  Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
    (heap_ctx HeapI HeapG N  sts.ctx StsI sts γ N (barrier_inv l P))%I.

  Definition send (l : loc) (P : iProp) : iProp :=
    ( γ, barrier_ctx γ l P  sts.in_states StsI sts γ low_states {[ Send ]})%I.

  Definition recv (l : loc) (R : iProp) : iProp :=
    ( γ (P Q : iProp) i, barrier_ctx γ l P  sts.in_states StsI sts γ (i_states i) {[ Change i ]} 
        saved_prop_own SpI i Q  (Q - R))%I.
    

End proof.