Model-based reasoning: concurrent counting
An example verification program with concurrent counting: two threads that concurrently decrement a shared counter. The verification uses model-based abstraction/reasoning.
|Features||Futures, Statically-scoped locking, Statically-scoped parallelism|
|Path to example file||futures/counteradd_2.pvl|
|Lines of code||46 lines (comments not included)|
|Lines of specification||13 lines (28.26% of the total)|
|Computation time||27905 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.