Model-based reasoning: generalised concurrent counting

Verification example with `n` threads, each decrementing a shared variable. This verification problem shows that our model-based abstraction approach can be applied to applications that spawn a dynamic number of threads.

General information

ID65
Articlenone
Back-endSilicon
LanguagePVL
FeaturesFork/join concurrency, Futures, Statically-scoped locking
Sources
Path to example filefutures/counteradd_n.pvl
Date2017-06-19

Statistical information

Lines of code91 lines (comments not included)
Lines of specification26 lines (28.57% of the total)
Computation time27905 milliseconds

Example code

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