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