1 files changed, 59 insertions, 0 deletions
diff --git a/Chalice/tests/examples/UnboundedThreads.chalice b/Chalice/tests/examples/UnboundedThreads.chalice
new file mode 100644
index 00000000..c52bb10a
--- /dev/null
+++ b/Chalice/tests/examples/UnboundedThreads.chalice
@@ -0,0 +1,59 @@
+class C {
+  
+  var f: int;
+  
+  method main(n: int)
+    requires n > 0 && acc(this.f)
+    ensures acc(this.f)
+  {
+    // fork all threads, and join them afterwards
+    call work(n);
+    
+    this.f := 100; // we want a full permission in the end
+  }
+
+  method work(n: int)
+    requires rd(this.f,n)
+    ensures rd(this.f,n)
+  {
+    var tks:seq<token<C.m>> := nil<token<C.m>>;
+    
+    // first loop; fork all threads
+    var i := 0;
+    while (i < n)
+      invariant i <= n && |tks| == i;
+      invariant i < n ==> rd(this.f,n-i);
+      invariant acc(tks[*].joinable);
+      invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
+      invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
+      invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
+    {
+      fork tk := m();
+      tks := tks ++ [tk];
+      i := i+1;
+    }
+    
+    // second loop; join all threads
+    i := n;
+    while (i > 0)
+      invariant i >= 0 && |tks| == i;
+      invariant i < n ==> rd(this.f,n-i); // BUG: the eval construct inside the quantification does not give us the information needed to proof this invariant, see http://boogie.codeplex.com/workitem/10187
+      invariant acc(tks[*].joinable);
+      invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
+      invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
+      invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
+    {
+      var tk: token<C.m>;
+      tk := tks[i-1];
+      join tk;
+      i := i-1;
+      tks := tks[0..i];
+    }
+  }
+  
+  method m()
+    requires rd(this.f,1);
+    ensures rd(this.f,1);
+  { /* do some computation */ }
+
+}