Verifying wait-notify patterns

Verifying a wait/notify concurrency pattern, in the context of two workers/threads that concurrently operate on a shared Queue. When working on the queue all other threads have to _wait_ for completion, and when the working threads has finished it _notifies_ all other waiting threads.

General information

ID160
Articlenone
Back-endSilicon
LanguagePVL
FeaturesFork/join concurrency, Locking, Loop invariants
Sources
Path to example filewaitnotify/Queue.pvl
Date2017-06-21

Statistical information

Lines of code25 lines (comments not included)
Lines of specification4 lines (16% of the total)
Computation time22453 milliseconds

Example code

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