define the program we want to verify, and the STS we plan to use

_CoqProject

@@ -77,3 +77,4 @@ heap_lang/heap.v
 heap_lang/notation.v
 heap_lang/tests.v
 heap_lang/substitution.v
+barrier/barrier.v

algebra/sts.v

@@ -13,6 +13,7 @@ Record stsT := STS {
   trans : relation state;
   tok   : state → set token;
 }.
+Arguments STS {_ _} _ _.
 
 (* The type of bounds we can give to the state of an STS. This is the type
    that we equip with an RA structure. *)

barrier/barrier.v

+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.
+  Inductive state := Low (I : gset gname) | High (I : gset gname).
+  Inductive token := Change (i : gname) | Send.
+
+  Definition change_tokens (I : gset gname) : set token :=
+    mkSet (λ t, match t with Change i => i ∈ I | Send => False end).
+
+  Inductive trans : relation state :=
+  | LowChange I1 I2 : trans (Low I1) (Low I2)
+  | HighChange I2 I1 : trans (High I1) (High I2)
+  | LowHigh I : trans (Low I) (High I).
+
+  Definition tok (s : state) : set token :=
+    match s with
+    | Low I' => change_tokens I'
+    | High I' => change_tokens I' ∪ {[ Send ]}
+    end.
+
+  Definition sts := sts.STS trans tok.
+End barrier_proto.
+

heap_lang/notation.v

@@ -20,6 +20,7 @@ Coercion of_val : val >-> expr.
    pretty printing. *)
 Notation "' l" := (Lit l%Z) (at level 8, format "' l").
 Notation "' l" := (LitV l%Z) (at level 8, format "' l").
+Notation "()"  := LitUnit  (at level 0) : lang_scope.
 Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope.
 Notation "'ref' e" := (Alloc e%L)
   (at level 30, right associativity) : lang_scope.