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

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

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

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

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

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

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

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

33
  (* The set of states containing some particular i *)
34 35 36 37
  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
38
    sts.closed (i_states i) {[ Change i ]}.
39 40
  Proof.
    split.
41
    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
Ralf Jung's avatar
Ralf Jung committed
42 43 44 45 46
      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.
47 48 49 50 51
    - (* 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
52 53
      (* We probably want some helper lemmas for this... *)
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
54 55
      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
      destruct Htrans; last done; move:Hs1 Hdisj Htok.
Ralf Jung's avatar
Ralf Jung committed
56 57 58 59 60 61 62 63 64 65
      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.
66 67 68 69 70 71

  (* 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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
72
    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 99
(** 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).
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  Context (StsI : gid) `{!STSInG heap_lang Σ StsI sts}.
101 102 103 104 105
  Context (SpI : gid) `{!SavedPropInG heap_lang Σ SpI}.

  Notation iProp := (iPropG heap_lang Σ).

  Definition waiting (P : iProp) (I : gset gname) : iProp :=
106 107
    ( Q : gmap gname iProp, (P - Π★{map Q} (λ _ Q, Q)) 
                             Π★{map Q} (λ i Q, saved_prop_own SpI i Q))%I.
108 109

  Definition ress (I : gset gname) : iProp :=
110
    (Π★{set I} (λ i,  Q, saved_prop_own SpI i Q  Q))%I.
111 112 113 114 115 116 117 118

  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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
119
    (heap_ctx HeapI HeapG N  sts_ctx StsI sts γ N (barrier_inv l P))%I.
120 121

  Definition send (l : loc) (P : iProp) : iProp :=
Robbert Krebbers's avatar
Robbert Krebbers committed
122
    ( γ, barrier_ctx γ l P  sts_ownS StsI sts γ low_states {[ Send ]})%I.
123 124

  Definition recv (l : loc) (R : iProp) : iProp :=
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    ( γ (P Q : iProp) i, barrier_ctx γ l P  sts_ownS StsI sts γ (i_states i) {[ Change i ]} 
126 127
        saved_prop_own SpI i Q  (Q - R))%I.
    
Ralf Jung's avatar
Ralf Jung committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
  Lemma newchan_spec (P : iProp) (Q : val  iProp) :
    ( l, recv l P  send l P - Q (LocV l))  wp coPset_all (newchan '()) Q.
  Proof.
  Abort.

  Lemma signal_spec l P (Q : val  iProp) :
    (send l P  P  Q '())  wp coPset_all (signal (LocV l)) Q.
  Proof.
  Abort.

  Lemma wait_spec l P (Q : val  iProp) :
    (recv l P  (P - Q '()))  wp coPset_all (wait (LocV l)) Q.
  Proof.
  Abort.

  Lemma split_spec l P1 P2 Q :
    (recv l (P1  P2)  (recv l P1  recv l P2 - Q '()))  wp coPset_all Skip Q.
  Proof.
  Abort.

  Lemma recv_strengthen l P1 P2 :
    (P1 - P2)  (recv l P1 - recv l P2).
  Proof.
  Abort.
152 153

End proof.