*
* The unlock operation has to re-enable all of the threads that are
* waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
*/
-void ModelChecker::process_mutex(ModelAction *curr) {
+bool ModelChecker::process_mutex(ModelAction *curr) {
std::mutex *mutex = (std::mutex *)curr->get_location();
struct std::mutex_state *state = mutex->get_state();
switch (curr->get_type()) {
state->islocked = true;
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
- if (unlock != NULL)
+ if (unlock != NULL) {
curr->synchronize_with(unlock);
+ return true;
+ }
break;
}
case ATOMIC_UNLOCK: {
default:
ASSERT(0);
}
+ return false;
}
/**
build_reads_from_past(curr);
curr = newcurr;
+ /* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
while (!work_queue.empty()) {
case WORK_CHECK_CURR_ACTION: {
ModelAction *act = work.action;
bool update = false; /* update this location's release seq's */
+ bool update_all = false; /* update all release seq's */
- process_thread_action(curr);
+ if (process_thread_action(curr))
+ update_all = true;
if (act->is_read() && process_read(act, second_part_of_rmw))
update = true;
if (act->is_write() && process_write(act))
update = true;
- if (act->is_mutex_op())
- process_mutex(act);
+ if (act->is_mutex_op() && process_mutex(act))
+ update_all = true;
- if (update)
+ if (update_all)
+ work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+ else if (update)
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
work_queue->push_back(MOEdgeWorkEntry(act));
/* propagate synchronization to later actions */
- action_list_t::reverse_iterator it = action_trace->rbegin();
- for (; (*it) != act; it++) {
- ModelAction *propagate = *it;
+ action_list_t::reverse_iterator rit = action_trace->rbegin();
+ for (; (*rit) != act; rit++) {
+ ModelAction *propagate = *rit;
if (act->happens_before(propagate)) {
propagate->synchronize_with(act);
/* Re-check 'propagate' for mo_graph edges */