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.
|Features||Fork/join concurrency, Statically-scoped locking, Statically-scoped parallelism|
|Path to example file||futures/unequalcounting.pvl|
|Lines of code||52 lines (comments not included)|
|Lines of specification||19 lines (36.54% of the total)|
|Computation time||19881 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.