diff --git a/_CoqProject b/_CoqProject
index 4691c835f829637e4d035e0fdea08e447cc797e2..9d0be2709ce3b3fdccdca7ba3f733b35ce4e40ee 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -77,3 +77,4 @@ heap_lang/heap.v
 heap_lang/notation.v
 heap_lang/tests.v
 heap_lang/substitution.v
+barrier/barrier.v
diff --git a/algebra/sts.v b/algebra/sts.v
index faf8ee3c9cd0abe9b9b9b8c8ac4affe64d1f33c4..ca2056e5a1b856fe122fac0ecf85a6b735a0d1d7 100644
--- a/algebra/sts.v
+++ b/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. *)
diff --git a/barrier/barrier.v b/barrier/barrier.v
new file mode 100644
index 0000000000000000000000000000000000000000..6a13bce92b37304c1b3b79782fd741de7e6383f9
--- /dev/null
+++ b/barrier/barrier.v
@@ -0,0 +1,29 @@
+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.
+
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index c332abc5eb6aca0076bdefad0203d84b837946be..20bc92f4053433537eb086394fe136f6dfa1e88d 100644
--- a/heap_lang/notation.v
+++ b/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.