Dafny: implemented compilation of parallel statements

Dafny: beefed up resolution of parallel statements

7 files changed, 384 insertions, 46 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 82de380d..e22d52ad 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -298,6 +298,12 @@ namespace Dafny
         return elmts;

       }

     }

+    public IEnumerable<T> UniqueElements {

+      get {

+        var st = Set<T>.FromElements(elmts);

+        return st.Elements;

+      }

+    }

     public T Select(BigInteger index) {

       return elmts[(int)index];

     }

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 47f5a98a..23477186 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -895,9 +895,184 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is ParallelStmt) {

         var s = (ParallelStmt)stmt;

-        Error("parallel statements are not yet supported by the Dafny compiler; stay tuned");

-        // TODO

-        

+        if (s.Kind != ParallelStmt.ParBodyKind.Assign) {

+          // Call and Proof have no side effects, so they can simply be optimized away.

+          return;

+        }

+        var s0 = (AssignStmt)s.S0;

+        if (s0.Rhs is HavocRhs) {

+          // The parallel statement says to havoc a bunch of things.  This can be efficiently compiled

+          // into doing nothing.

+          return;

+        }

+        var rhs = ((ExprRhs)s0.Rhs).Expr;

+

+        // Compile:

+        //   parallel (w,x,y,z | Range(w,x,y,z)) {

+        //     LHS(w,x,y,z) := RHS(w,x,y,z);

+        //   }

+        // where w,x,y,z have types seq<W>,set<X>,int,bool and LHS has L-1 top-level subexpressions

+        // (that is, L denotes the number of top-level subexpressions of LHS plus 1),

+        // into:

+        //   var ingredients = new List< L-Tuple >();

+        //   foreach (W w in sq.UniqueElements) {

+        //     foreach (X x in st.Elements) {

+        //       for (BigInteger y = Lo; j < Hi; j++) {

+        //         for (bool z in Helper.AllBooleans) {

+        //           if (Range(w,x,y,z)) {

+        //             ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

+        //           }

+        //         }

+        //       }

+        //     }

+        //   }

+        //   foreach (L-Tuple l in ingredients) {

+        //     LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);

+        //   }

+        //

+        // Note, because the .NET Tuple class only supports up to 8 components, the compiler implementation

+        // here supports arrays only up to 6 dimensions.  This does not seem like a serious practical limitation.

+        // However, it may be more noticeable if the parallel statement supported parallel assignments in its

+        // body.  To support cases where tuples would need more than 8 components, .NET Tuple's would have to

+        // be nested.

+

+        // Temporary names

+        string ingredients = "_ingredients" + tmpVarCount;

+        string tup = "_tup" + tmpVarCount;

+        tmpVarCount++;

+

+        // Compute L

+        int L;

+        string tupleTypeArgs;

+        if (s0.Lhs is FieldSelectExpr) {

+          var lhs = (FieldSelectExpr)s0.Lhs;

+          L = 2;

+          tupleTypeArgs = TypeName(lhs.Obj.Type);

+        } else if (s0.Lhs is SeqSelectExpr) {

+          var lhs = (SeqSelectExpr)s0.Lhs;

+          L = 3;

+          // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

+          tupleTypeArgs = TypeName(lhs.Seq.Type) + ",int";

+        } else {

+          var lhs = (MultiSelectExpr)s0.Lhs;

+          L = 2 + lhs.Indices.Count;

+          if (8 < L) {

+            Error("compiler currently does not support assignments to more-than-6-dimensional arrays in parallel statements");

+            return;

+          }

+          tupleTypeArgs = TypeName(lhs.Array.Type);

+          for (int i = 0; i < lhs.Indices.Count; i++) {

+            // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

+            tupleTypeArgs += ",int";

+          }

+        }

+        tupleTypeArgs += "," + TypeName(rhs.Type);

+

+        // declare and construct "ingredients"

+        Indent(indent);

+        wr.WriteLine("var {0} = new List<System.Tuple<{1}>>();", ingredients, tupleTypeArgs);

+

+        var n = s.BoundVars.Count;

+        Contract.Assert(s.Bounds.Count == n);

+        for (int i = 0; i < n; i++) {

+          Indent(indent + i * IndentAmount);

+          var bound = s.Bounds[i];

+          var bv = s.BoundVars[i];

+          if (bound is QuantifierExpr.BoolBoundedPool) {

+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.Name);

+          } else if (bound is QuantifierExpr.IntBoundedPool) {

+            var b = (QuantifierExpr.IntBoundedPool)bound;

+            wr.Write("for (var @{0} = ", bv.Name);

+            TrExpr(b.LowerBound);

+            wr.Write("; @{0} < ", bv.Name);

+            TrExpr(b.UpperBound);

+            wr.Write("; @{0}++) {{ ", bv.Name);

+          } else if (bound is QuantifierExpr.SetBoundedPool) {

+            var b = (QuantifierExpr.SetBoundedPool)bound;

+            wr.Write("foreach (var @{0} in (", bv.Name);

+            TrExpr(b.Set);

+            wr.Write(").Elements) { ");

+          } else if (bound is QuantifierExpr.SeqBoundedPool) {

+            var b = (QuantifierExpr.SeqBoundedPool)bound;

+            wr.Write("foreach (var @{0} in (", bv.Name);

+            TrExpr(b.Seq);

+            wr.Write(").UniqueElements) { ");

+          } else {

+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

+          }

+          wr.WriteLine();

+        }

+

+        // if (range) {

+        //   ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

+        // }

+        Indent(indent + n * IndentAmount);

+        wr.Write("if (");

+        if (s.Range == null) {

+          wr.Write("true");

+        } else {

+          TrExpr(s.Range);

+        }

+        wr.WriteLine(") {");

+

+        Indent(indent + (n + 1) * IndentAmount);

+        wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);

+        if (s0.Lhs is FieldSelectExpr) {

+          var lhs = (FieldSelectExpr)s0.Lhs;

+          TrExpr(lhs.Obj);

+        } else if (s0.Lhs is SeqSelectExpr) {

+          var lhs = (SeqSelectExpr)s0.Lhs;

+          TrExpr(lhs.Seq);

+          wr.Write(", (int)(");

+          TrExpr(lhs.E0);

+          wr.Write(")");

+        } else {

+          var lhs = (MultiSelectExpr)s0.Lhs;

+          TrExpr(lhs.Array);

+          for (int i = 0; i < lhs.Indices.Count; i++) {

+            wr.Write(", (int)(");

+            TrExpr(lhs.Indices[i]);

+            wr.Write(")");

+          }

+          wr.WriteLine("] = {0}.Item{1};", tup, L);

+        }

+        wr.Write(", ");

+        TrExpr(rhs);

+        wr.WriteLine("));");

+

+        Indent(indent + n * IndentAmount);

+        wr.WriteLine("}");

+

+        for (int i = n; 0 <= --i; ) {

+          Indent(indent + i * IndentAmount);

+          wr.WriteLine("}");

+        }

+

+        //   foreach (L-Tuple l in ingredients) {

+        //     LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);

+        //   }

+        Indent(indent);

+        wr.WriteLine("foreach (var {0} in {1}) {{", tup, ingredients);

+        Indent(indent + IndentAmount);

+        if (s0.Lhs is FieldSelectExpr) {

+          var lhs = (FieldSelectExpr)s0.Lhs;

+          wr.WriteLine("{0}.Item1.@{1} = {0}.Item2;", tup, lhs.FieldName);

+        } else if (s0.Lhs is SeqSelectExpr) {

+          var lhs = (SeqSelectExpr)s0.Lhs;

+          wr.WriteLine("{0}.Item1[{0}.Item2] = {0}.Item3;", tup);

+        } else {

+          var lhs = (MultiSelectExpr)s0.Lhs;

+          wr.Write("{0}.Item1[");

+          string sep = "";

+          for (int i = 0; i < lhs.Indices.Count; i++) {

+            wr.Write("{0}{1}.Item{2}", sep, tup, i + 2);

+            sep = ", ";

+          }

+          wr.WriteLine("] = {0}.Item{1};", tup, L);

+        }

+        Indent(indent);

+        wr.WriteLine("}");

+

       } else if (stmt is ForeachStmt) {

         ForeachStmt s = (ForeachStmt)stmt;

         // List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2fa86d5e..43c72000 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -12,7 +12,7 @@ using Microsoft.Boogie;
 namespace Microsoft.Dafny {

   public class Resolver {

     public int ErrorCount = 0;

-    protected virtual void Error(IToken tok, string msg, params object[] args) {

+    void Error(IToken tok, string msg, params object[] args) {

       Contract.Requires(tok != null);

       Contract.Requires(msg != null);

       ConsoleColor col = Console.ForegroundColor;

@@ -43,6 +43,16 @@ namespace Microsoft.Dafny {
       Contract.Requires(msg != null);

       Error(e.tok, msg, args);

     }

+    void Warning(IToken tok, string msg, params object[] args) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

+      ConsoleColor col = Console.ForegroundColor;

+      Console.ForegroundColor = ConsoleColor.Yellow;

+      Console.WriteLine("{0}({1},{2}): Warning: {3}",

+          tok.filename, tok.line, tok.col - 1,

+          string.Format(msg, args));

+      Console.ForegroundColor = col;

+    }

 

     readonly BuiltIns builtIns;

     readonly Dictionary<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes = new Dictionary<string/*!*/,TopLevelDecl/*!*/>();

@@ -1570,40 +1580,27 @@ namespace Microsoft.Dafny {
         scope.PopMarker();

 

         if (prevErrorCount == ErrorCount) {

-          // check for supported kinds

-          if (s.Ens.Count == 0) {

-            // The supported kinds are Assign and Call.  See if it's one of them.

+          // determine the Kind and run some additional checks on the body

+          if (s.Ens.Count != 0) {

+            // The only supported kind with ensures clauses is Proof.

+            s.Kind = ParallelStmt.ParBodyKind.Proof;

+          } else {

+            // There are two special cases:

+            // * Assign, which is the only kind of the parallel statement that allows a heap update.

+            // * Call, which is a single call statement with no side effects or output parameters.

+            // The effect of Assign and the postcondition of Call will be seen outside the parallel

+            // statement.

             Statement s0 = s.S0;

             if (s0 is AssignStmt) {

-              var lhs = ((AssignStmt)s0).Lhs.Resolved;

-              if (lhs is IdentifierExpr) {

-                Error(s0, "a parallel statement must not update local variables declared outside the parallel body");

-              } else if (lhs is FieldSelectExpr) {

-                // cool

-              } else if (lhs is SeqSelectExpr && ((SeqSelectExpr)lhs).SelectOne) {

-                // cool

-              } else if (lhs is MultiSelectExpr) {

-                // cool

-              } else {

-                Contract.Assert(false);  // unexpected assignment LHS

-              }

-              var rhs = ((AssignStmt)s0).Rhs;  // ExprRhs and HavocRhs are fine, but TypeRhs is not

-              // TODO: Occurrences of Choose in RHS must also be handled or disallowed (this happen when Choose is treated like a method member of the set type)

-              if (rhs is TypeRhs) {

-                Error(rhs.Tok, "new allocation not supported in parallel statements");

-              }

               s.Kind = ParallelStmt.ParBodyKind.Assign;

             } else if (s0 is CallStmt) {

-              CheckNoForeignUpdates(s0);

               s.Kind = ParallelStmt.ParBodyKind.Call;

             } else {

-              Error(s, "the body of an ensures-less parallel statement must be one assignment statement or one call statement");

+              s.Kind = ParallelStmt.ParBodyKind.Proof;

+              Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");

             }

-          } else {

-            // The only supported kind with ensures clauses is Proof.  See if that's what the body really is.

-            CheckNoForeignUpdates(s.Body);

-            s.Kind = ParallelStmt.ParBodyKind.Proof;

           }

+          CheckParallelBodyRestrictions(s.Body, s.Kind == ParallelStmt.ParBodyKind.Assign);

         }

 

       } else if (stmt is MatchStmt) {

@@ -2064,30 +2061,42 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public void CheckNoForeignUpdates(Statement stmt) {

+    /// <summary>

+    /// This method performs some additional checks on the body "stmt" of a parallel statement

+    /// </summary>

+    public void CheckParallelBodyRestrictions(Statement stmt, bool allowHeapUpdates) {

       Contract.Requires(stmt != null);

       if (stmt is PredicateStmt) {

         // cool

       } else if (stmt is PrintStmt) {

         Error(stmt, "print statement is not allowed inside a parallel statement");

       } else if (stmt is BreakStmt) {

-        // TODO: this case can be checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack

+        // this case can be checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack

       } else if (stmt is ReturnStmt) {

         Error(stmt, "return statement is not allowed inside a parallel statement");

       } else if (stmt is ConcreteSyntaxStatement) {

         var s = (ConcreteSyntaxStatement)stmt;

         foreach (var ss in s.ResolvedStatements) {

-          CheckNoForeignUpdates(ss);

+          CheckParallelBodyRestrictions(ss, allowHeapUpdates);

         }

       } else if (stmt is AssignStmt) {

         var s = (AssignStmt)stmt;

-        var idExpr = s.Lhs as IdentifierExpr;

+        var idExpr = s.Lhs.Resolved as IdentifierExpr;

         if (idExpr != null) {

           if (scope.ContainsDecl(idExpr.Var)) {

             Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");

           }

-        } else {

-          Error(stmt, "the body of the enclosing parallel statement may not updated heap locations");

+        } else if (!allowHeapUpdates) {

+          Error(stmt, "the body of the enclosing parallel statement may not update heap locations");

+        }

+        var rhs = s.Rhs;  // ExprRhs and HavocRhs are fine, but TypeRhs is not

+        if (rhs is TypeRhs) {

+          Error(rhs.Tok, "new allocation not supported in parallel statements");

+        } else if (rhs is ExprRhs) {

+          var r = ((ExprRhs)rhs).Expr.Resolved;

+          if (r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {

+            Error(r, "set choose operator not supported inside parallel statement");

+          }

         }

       } else if (stmt is VarDecl) {

         // cool

@@ -2100,7 +2109,7 @@ namespace Microsoft.Dafny {
               Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");

             }

           } else {

-            Error(stmt, "the body of the enclosing parallel statement may not updated heap locations");

+            Error(stmt, "the body of the enclosing parallel statement may not update heap locations");

           }

         }

         if (s.Method.Mod.Count != 0) {

@@ -2111,34 +2120,34 @@ namespace Microsoft.Dafny {
         var s = (BlockStmt)stmt;

         scope.PushMarker();

         foreach (var ss in s.Body) {

-          CheckNoForeignUpdates(ss);

+          CheckParallelBodyRestrictions(ss, allowHeapUpdates);

         }

         scope.PopMarker();

 

       } else if (stmt is IfStmt) {

         var s = (IfStmt)stmt;

-        CheckNoForeignUpdates(s.Thn);

+        CheckParallelBodyRestrictions(s.Thn, allowHeapUpdates);

         if (s.Els != null) {

-          CheckNoForeignUpdates(s.Els);

+          CheckParallelBodyRestrictions(s.Els, allowHeapUpdates);

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

         foreach (var alt in s.Alternatives) {

           foreach (var ss in alt.Body) {

-            CheckNoForeignUpdates(ss);

+            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

           }

         }

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

-        CheckNoForeignUpdates(s.Body);

+        CheckParallelBodyRestrictions(s.Body, allowHeapUpdates);

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

         foreach (var alt in s.Alternatives) {

           foreach (var ss in alt.Body) {

-            CheckNoForeignUpdates(ss);

+            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

           }

         }

 

@@ -2164,7 +2173,7 @@ namespace Microsoft.Dafny {
         var s = (MatchStmt)stmt;

         foreach (var kase in s.Cases) {

           foreach (var ss in kase.Body) {

-            CheckNoForeignUpdates(ss);

+            CheckParallelBodyRestrictions(ss, allowHeapUpdates);

           }

         }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4e79e92f..4745ae48 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -947,6 +947,22 @@ Execution trace:
 

 Dafny program verifier finished with 27 verified, 6 errors

 

+-------------------- ParallelResolveErrors.dfy --------------------

+ParallelResolveErrors.dfy(8,6): Error: LHS of assignment must denote a mutable variable or field

+ParallelResolveErrors.dfy(13,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

+ParallelResolveErrors.dfy(31,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ParallelResolveErrors.dfy(43,13): Error: set choose operator not supported inside parallel statement

+ParallelResolveErrors.dfy(48,13): Error: new allocation not supported in parallel statements

+ParallelResolveErrors.dfy(53,13): Error: new allocation not supported in parallel statements

+ParallelResolveErrors.dfy(60,19): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(64,18): Error: return statement is not allowed inside a parallel statement

+ParallelResolveErrors.dfy(71,21): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(72,20): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(73,20): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(82,24): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(83,24): Error: break label is undefined or not in scope: OutsideLoop

+13 resolution/type errors detected in ParallelResolveErrors.dfy

+

 -------------------- Parallel.dfy --------------------

 Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.

 Parallel.dfy(57,14): Related location: This is the precondition that might not hold.

@@ -1019,8 +1035,14 @@ Execution trace:
     (0,0): anon6_Then

     (0,0): anon7_Then

     (0,0): anon3

+Parallel.dfy(182,12): Error: left-hand sides for different parallel-statement bound variables may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon19_Then

+    (0,0): anon20_Then

+    (0,0): anon5

 

-Dafny program verifier finished with 17 verified, 7 errors

+Dafny program verifier finished with 20 verified, 8 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(44,22): Error: assertion violation

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index e3ba0d67..817120ce 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -148,3 +148,42 @@ method M5()
     assert Pred(34, 34);

   }

 }

+

+method Main()

+{

+  var a := new int[180];

+  parallel (i | 0 <= i < 180) {

+    a[i] := 2*i + 100;

+  }

+  var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];

+  parallel (i | 0 <= i < |sq|) {

+    a[20+i] := sq[i];

+  }

+  parallel (t | t in sq) {

+    a[t] := 1000;

+  }

+  parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {

+    a[u] := 6000 + t;

+  }

+  var k := 0;

+  while (k < 180) {

+    if (k != 0) { print ", "; }

+    print a[k];

+    k := k + 1;

+  }

+  print "\n";

+}

+

+method DuplicateUpdate() {

+  var a := new int[180];

+  var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];

+  if (*) {

+    parallel (t,u | t in sq && 10 <= u < 10+t) {

+      a[u] := 6000 + t;  // error: a[10] (and a[11]) are assigned more than once

+    }

+  } else {

+    parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {

+      a[u] := 6000 + t;  // with the 't < 4' conjunct in the line above, this is fine

+    }

+  }

+}

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
new file mode 100644
index 00000000..4e0be32e
--- /dev/null
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -0,0 +1,87 @@
+class C {

+  var data: int;

+}

+

+method M0(IS: set<int>)

+{

+  parallel (i | 0 <= i < 20) {

+    i := i + 1;  // error: not allowed to assign to bound variable

+  }

+

+  var k := 0;

+  parallel (i | 0 <= i < 20) {

+    k := k + i;  // error: not allowed to assign to local k, since k is not declared inside parallel block

+  }

+

+  parallel (i | 0 <= i < 20)

+    ensures true;

+  {

+    var x := i;

+    x := x + 1;

+  }

+

+  ghost var y;

+  var z;

+  parallel (i | 0 <= i)

+    ensures true;

+  {

+    var x := i;

+    x := x + 1;

+    y := 18;  // (this statement is not allowed, since y is declared outside the parallel, but that check happens only if the first resolution pass of the parallel statement passes, which it doesn't in this case because of the next line)

+    z := 20;  // error: assigning to a non-ghost variable inside a ghost parallel block

+  }

+

+  parallel (i | 0 <= i)

+    ensures true;

+  {

+    ghost var x := i;

+    x := x + 1;  // cool

+  }

+

+  var ia := new int[20];

+  parallel (i | 0 <= i < 20) {

+    ia[i] := choose IS;  // error: set choose not allowed

+  }

+

+  var ca := new C[20];

+  parallel (i | 0 <= i < 20) {

+    ca[i] := new C;  // error: new allocation not allowed

+  }

+  parallel (i | 0 <= i < 20)

+    ensures true;

+  {

+    var c := new C;  // error: new allocation not allowed

+  }

+}

+

+method M1() {

+  parallel (i | 0 <= i < 20) {

+    assert i < 100;

+    if (i == 17) { break; }  // error: nothing to break out of

+  }

+

+  parallel (i | 0 <= i < 20) ensures true; {

+    if (i == 8) { return; }  // error: return not allowed inside parallel block

+  }

+

+  var m := 0;

+  label OutsideLoop:

+  while (m < 20) {

+    parallel (i | 0 <= i < 20) {

+      if (i == 17) { break; }  // error: not allowed to break out of loop that sits outside parallel

+      if (i == 8) { break break; }  // error: ditto (also: attempt to break too far)

+      if (i == 9) { break OutsideLoop; }  // error: ditto

+    }

+    m := m + 1;

+  }

+

+  parallel (i | 0 <= i < 20) {

+    var j := 0;

+    while (j < i) {

+      if (j == 6) { break; }  // fine

+      if (j % 7 == 4) { break break; }  // error: attempt to break out too far

+      if (j % 7 == 4) { break OutsideLoop; }  // error: attempt to break to place not in enclosing scope

+      j := j + 1;

+    }

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index a670ced5..c30ec3a5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

-            Termination.dfy DTypes.dfy Parallel.dfy

+            Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy