Parallel GCD

In this example a concurrent GCD algorithm is proven correct, meaning that after the algorithm terminates it has calculated the GCD of the two input values. The verification is done by using model-based abstraction. A process algebraic model of the GCD algorithm is defined and we prove that the program adheres to this abstraction. By analysing the process algebra term we finally verify that the program calculates the correct GCD.

General Information

• Backend: Silicon
• Language: PVL
• Features: Futures, Statically-scoped locking, Statically-scoped parallelism
• Path to Example File: futures/ParallelGCD.pvl
• Should Verify: Yes
• Date: 2017-06-16
• Lines of Code: 80 (comments not included)
• Lines of Specification: 37 (46.2% of total)
• Computation Time: 24.9 seconds