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

• Backend: Silicon
• Language: PVL
• Features: Locking, Fork/join concurrency, Loop invariants
• Path to Example File: waitnotify/Queue.pvl
• Should Verify: Yes
• Date: 2017-06-21
• Lines of Code: 25 (comments not included)
• Lines of Specification: 4 (16.0% of total)
• Computation Time: 22.5 seconds