Dafny: implemented compilation of parallel statements

Dafny: beefed up resolution of parallel statements

4 files changed, 150 insertions, 2 deletions

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