Fork examples

examples/forkjoin/forkfail.pvl

@@ -0,0 +1,28 @@
+//:: cases ForkPVLFail
+//:: tools silicon
+//:: verdict Fail
+
+class Test {
+
+  Test() {}
+
+  requires true;
+  ensures  true;
+  void run(){
+
+  }
+
+  void test2(){
+    Test t1=new Test();
+    fork t1;
+    fork t1;
+
+  }
+
+  void test3(){
+    Test t1=new Test();
+    join t1;    
+  }
+
+}
+

examples/forkjoin/forkjoininforloop.pvl

@@ -0,0 +1,61 @@
+//:: cases ForkJoinLoopPVL
+//:: tools silicon
+//:: verdict Pass
+
+class MainFJ {
+
+
+  static void MainFJ(seq<int> nodes){
+    seq<NodesThread> nodeThreads = seq<NodesThread> {};
+
+    loop_invariant 0 <= i && i <= |nodes|;
+	loop_invariant |nodeThreads| == i;
+	loop_invariant (\forall* int j=0..|nodeThreads|; idle(nodeThreads[j]));
+	loop_invariant (\forall* int j=0..|nodeThreads|; Perm(nodeThreads[j].val,1));
+    for(int i = 0; i < |nodes|; i++) {
+		NodesThread node = new NodesThread(nodes[i]);
+		nodeThreads = nodeThreads ++ node;
+		assert idle(nodeThreads[i]);
+    }
+
+    assert (\forall* int j=0..|nodeThreads|; Perm(nodeThreads[j].val,1));
+    assert (\forall* int j=0..|nodeThreads|; idle(nodeThreads[j]));
+
+    loop_invariant 0 <= i && i <= |nodes|;
+	loop_invariant (\forall* int j=i..|nodeThreads|; idle(nodeThreads[j]));
+	loop_invariant (\forall* int j=0..i; running(nodeThreads[j]));
+	loop_invariant (\forall* int j=0..|nodeThreads|; Perm(nodeThreads[j].val,1));
+	for(int i = 0; i < |nodes|; i++) {
+		assert idle(nodeThreads[i]);
+		fork nodeThreads[i];
+		assert running(nodeThreads[i]);
+    }
+
+    assert (\forall* int j=0..|nodeThreads|; running(nodeThreads[j]));
+
+    loop_invariant 0 <= i && i <= |nodes|;
+    loop_invariant |nodeThreads| == |nodes|;
+    loop_invariant (\forall* int j=i..|nodeThreads|; running(nodeThreads[j]));
+	loop_invariant (\forall* int j=0..i; idle(nodeThreads[j]));
+    for(int i = 0; i < |nodes|; i++) {
+		assert running(nodeThreads[i]);
+		join nodeThreads[i];
+		assert idle(nodeThreads[i]);
+    }
+  }
+
+}
+
+class NodesThread {
+
+	int val;
+
+	ensures Perm(val,1);
+	NodesThread(int v) {
+		val = v;
+	}
+
+	void run() {
+
+	}
+}

examples/manual/fork.pvl → examples/forkjoin/forkpass.pvl

@@ -1,10 +1,10 @@
-// -*- tab-width:2 ; indent-tabs-mode:nil -*-
-//:: cases ForkPVL
+//:: cases ForkPVLPass
 //:: tools silicon
-//:: verdict Pass Test.run Test.test1
-//:: verdict Fail Test.test2 Test.test3
+//:: verdict Pass 
 
 class Test {
+
+  Test() {}
 
 
   requires true;
@@ -27,20 +27,5 @@ class Test {
     join t1;
     assert idle(t1);    
   }
-
-  void test2(){
-    Test t1=new Test();
-    fork t1;
-    fork t1;
-
-  }
-
-  void test3(){
-    Test t1=new Test();
-    join t1;    
-  }
-
 }
 
-
-