DESCRIPTION
Requirement: The system does not deadlock.
Note: This property is actually violated. A
deadlock can occur in the system in the following kind of situation:
suppose artist a2 has registered for e1, and
now has accepted the call to its terminate_artist entry.
Task a2 then proceeds to call the dispatcher's
unregister_event entry. Suppose at the same time that
the dispatcher task has accepted a call to its
notify_artists entry and is at the point of calling the
notify_client_event entry in a2. Then the
dispatcher is blocked until a2 can proceed, and
a2 is blocked until the dispatcher can proceed, and
deadlock has occured.
Each of the four tools below discovers this deadlock.
SPECIFICATION
Up to Chiron Decomposed Dispatcher (2 artists, 2 events)
Forward to Property 1