A THREAD_FINISH action may ensure that a Thread is no longer able to
break release sequences, so all pending release sequences should be
checked.
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
- bool synchronized = false;
switch (curr->get_type()) {
case THREAD_CREATE: {
switch (curr->get_type()) {
case THREAD_CREATE: {
Thread *blocking = (Thread *)curr->get_location();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
Thread *blocking = (Thread *)curr->get_location();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_FINISH: {
break;
}
case THREAD_FINISH: {
scheduler->wake(get_thread(act));
}
th->complete();
scheduler->wake(get_thread(act));
}
th->complete();
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
break;
}
case THREAD_START: {