Property 0: The system does not deadlock


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.


Up to Chiron Decomposed Dispatcher (2 artists, 2 events)

Forward to Property 1