Block parallelism

Simple PVL program with parallel blocks (that is, code blocks with statically-scoped parallelism), incrementing two variables, `x` and `y`. We verify that, after the parallel blocks have executed, the result of the shared state is (observably) unchanged.

General information

ID116
Articlenone
Back-endSilicon
LanguagePVL
FeaturesIteration contracts, Loop parallelisations, Statically-scoped parallelism
Sources
Path to example fileparallel/block-par.pvl
Date2017-06-20

Statistical information

Lines of code21 lines (comments not included)
Lines of specification5 lines (23.81% of the total)
Computation time13157 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.