barrier.v 2.21 KB
Newer Older
1
2
3
4
5
6
7
8
9
From program_logic Require Export sts.
From heap_lang Require Export derived heap wp_tactics notation.

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

(** The STS describing the main barrier protocol. *)
Module barrier_proto.
10
11
  Inductive phase := Low | High.
  Record stateT := State { state_phase : phase; state_I : gset gname }.
12
13
  Inductive token := Change (i : gname) | Send.

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

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

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

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

  Definition sts := sts.STS trans tok.
29
30
31
32
33
34
35
36

  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.
Ralf Jung's avatar
Ralf Jung committed
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
    - apply (non_empty_inhabited (State Low {[ i ]})). rewrite !mkSet_elem_of /=.
      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.
    - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
      (* We probably want some helper lemmas for this... *)
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
      inversion_clear Hstep' as [? ? ? ? Htrans Htok1 Htok2 Htok].
      destruct Htrans; last done; move:Hs1 Hdisj Htok1 Htok2 Htok.
      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.
58
    
59
60
End barrier_proto.