From 263410061cbcd077d4c7a2d5ec284c090ac66711 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 09:50:01 +0100
Subject: [PATCH] define the program we want to verify, and the STS we plan to
 use

---
 _CoqProject          |  1 +
 algebra/sts.v        |  1 +
 barrier/barrier.v    | 29 +++++++++++++++++++++++++++++
 heap_lang/notation.v |  1 +
 4 files changed, 32 insertions(+)
 create mode 100644 barrier/barrier.v

diff --git a/_CoqProject b/_CoqProject
index 4691c835f..9d0be2709 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 faf8ee3c9..ca2056e5a 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 000000000..6a13bce92
--- /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 c332abc5e..20bc92f40 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.
-- 
GitLab