Getting Started
Installation Guide
Tutorial
Issue Tracker
Tools
Verifier
Alpinist
VeSUV
VeyMont
Showcases
Publications
About
VerCors Team
News
Contact
Credits
License
Parallel Fibonacci (PVL)
Verifying parallel Fibonacci, with fork/join parallelism.
General Information
Backend
: Silicon
Language
: PVL
Features
: Fork/join concurrency
Path to Example File
: manual/fibonacci.pvl
Should Verify
: Yes
Date
: 2017-06-20
Lines of Code
: 24 (comments not included)
Lines of Specification
: 4 (16.7% of total)
Computation Time
: 20.7 seconds
// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases FibonacciPVL //:: suite puptol //:: tools silicon //:: verdict Pass /* * This example verifies the permission used for * a fork/join computation of a Fibonacci number. * * To verify this example, use: * * vct --silver=silicon fibonacci.pvl */ // begin(all) class Fib { static int fib(int n)=n<2?1:fib(n-1)+fib(n-2); int input, output; requires Perm(input,1\10) ** Perm(output,1); ensures Perm(input,1\10) ** Perm(output,1) ** output==fib(input); void run() { if (input<2) { output = 1; } else { Fib f1 = new Fib(input-1); Fib f2 = new Fib(input-2); fork f1; fork f2; join f1; join f2; output = f1.output + f2.output; } } ensures Perm(input,1) ** Perm(output,1) ** input==n; Fib(int n){ input = n; } } // end(all)
Language:
PVL
Java
Cuda
C / OpenMP / OpenCL
Viper