Skip to content

Commit

Permalink
Merge pull request #652 from utwente-fmt/fork-examples
Browse files Browse the repository at this point in the history
Fork examples
  • Loading branch information
petravandenbos-utwente authored Jul 8, 2021
2 parents a7afff1 + fef6cc9 commit 5e0e69d
Show file tree
Hide file tree
Showing 3 changed files with 92 additions and 19 deletions.
28 changes: 28 additions & 0 deletions examples/forkjoin/forkfail.pvl
Original file line number Diff line number Diff line change
@@ -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;
}

}

60 changes: 60 additions & 0 deletions examples/forkjoin/forkjoininforloop.pvl
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
//:: 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() {

}
}
23 changes: 4 additions & 19 deletions examples/manual/fork.pvl → examples/forkjoin/forkpass.pvl
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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;
}

}



0 comments on commit 5e0e69d

Please sign in to comment.