Model-based reasoning: unequal counting

A variant on the verification example of concurrent counting: two threads that concurrently decrement a shared value, but with unequal amounts.

General information

ID67
Articlenone
Back-endSilicon
LanguagePVL
FeaturesFork/join concurrency, Statically-scoped locking, Statically-scoped parallelism
Sources
Path to example filefutures/unequalcounting.pvl
Date2017-06-19

Statistical information

Lines of code52 lines (comments not included)
Lines of specification19 lines (36.54% of the total)
Computation time19881 milliseconds

Example code

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