From b484ba1e3cc50c3daf6e994dd9628eedba5d786d Mon Sep 17 00:00:00 2001 From: Petra van den Bos Date: Thu, 8 Jul 2021 13:07:18 +0200 Subject: [PATCH 1/5] moved file fork.pvl from directory 'manual' to directory 'forkjoin' --- examples/{manual => forkjoin}/fork.pvl | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename examples/{manual => forkjoin}/fork.pvl (100%) diff --git a/examples/manual/fork.pvl b/examples/forkjoin/fork.pvl similarity index 100% rename from examples/manual/fork.pvl rename to examples/forkjoin/fork.pvl From e1cace1083113eab34a5fddda8226694e0febb02 Mon Sep 17 00:00:00 2001 From: Petra van den Bos Date: Thu, 8 Jul 2021 13:07:58 +0200 Subject: [PATCH 2/5] added example of using fork and join in a loop --- examples/forkjoin/forkjoininforloop.pvl | 57 +++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 examples/forkjoin/forkjoininforloop.pvl diff --git a/examples/forkjoin/forkjoininforloop.pvl b/examples/forkjoin/forkjoininforloop.pvl new file mode 100644 index 0000000000..afc078ec4c --- /dev/null +++ b/examples/forkjoin/forkjoininforloop.pvl @@ -0,0 +1,57 @@ +class MainFJ { + + + static void MainFJ(seq nodes){ + seq nodeThreads = seq {}; + + 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() { + + } +} From 531c18c720f4e3b98f761244fae69eb49c744e58 Mon Sep 17 00:00:00 2001 From: Petra van den Bos Date: Thu, 8 Jul 2021 13:25:52 +0200 Subject: [PATCH 3/5] added header to forkjoininforloop.pvl --- examples/forkjoin/forkjoininforloop.pvl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/examples/forkjoin/forkjoininforloop.pvl b/examples/forkjoin/forkjoininforloop.pvl index afc078ec4c..0792de9fc2 100644 --- a/examples/forkjoin/forkjoininforloop.pvl +++ b/examples/forkjoin/forkjoininforloop.pvl @@ -1,3 +1,7 @@ +//:: cases ForkJoinLoopPVL +//:: tools silicon +//:: verdict Pass + class MainFJ { From a73691d60260fd56bcce080a241d9170ac91ab64 Mon Sep 17 00:00:00 2001 From: Petra van den Bos Date: Thu, 8 Jul 2021 13:26:25 +0200 Subject: [PATCH 4/5] split fork.pvl in two files: one for failing methods and one for passing methods --- examples/forkjoin/forkfail.pvl | 28 ++++++++++++++++++++ examples/forkjoin/{fork.pvl => forkpass.pvl} | 23 +++------------- 2 files changed, 32 insertions(+), 19 deletions(-) create mode 100644 examples/forkjoin/forkfail.pvl rename examples/forkjoin/{fork.pvl => forkpass.pvl} (53%) diff --git a/examples/forkjoin/forkfail.pvl b/examples/forkjoin/forkfail.pvl new file mode 100644 index 0000000000..c174b2a7b4 --- /dev/null +++ b/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; + } + +} + diff --git a/examples/forkjoin/fork.pvl b/examples/forkjoin/forkpass.pvl similarity index 53% rename from examples/forkjoin/fork.pvl rename to examples/forkjoin/forkpass.pvl index 826e76dcd1..910d48b6ae 100644 --- a/examples/forkjoin/fork.pvl +++ b/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; - } - } - - From fef6cc90a01cadcdb2758b7457e80d2c4835edee Mon Sep 17 00:00:00 2001 From: Petra van den Bos Date: Thu, 8 Jul 2021 14:59:37 +0200 Subject: [PATCH 5/5] fix indentation --- examples/forkjoin/forkjoininforloop.pvl | 77 ++++++++++++------------- 1 file changed, 38 insertions(+), 39 deletions(-) diff --git a/examples/forkjoin/forkjoininforloop.pvl b/examples/forkjoin/forkjoininforloop.pvl index 0792de9fc2..ecd835d0f0 100644 --- a/examples/forkjoin/forkjoininforloop.pvl +++ b/examples/forkjoin/forkjoininforloop.pvl @@ -5,45 +5,44 @@ class MainFJ { - static void MainFJ(seq nodes){ - seq nodeThreads = seq {}; - - 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]); - } - } - + static void MainFJ(seq nodes) { + seq nodeThreads = seq {}; + + 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 {