All synchronization updates should generate a re-check of release sequences.
This commit corrects this for mutexes.
*
* The unlock operation has to re-enable all of the threads that are
* waiting on the lock.
*
* 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()) {
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
state->islocked = true;
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
curr->synchronize_with(unlock);
curr->synchronize_with(unlock);
break;
}
case ATOMIC_UNLOCK: {
break;
}
case ATOMIC_UNLOCK: {
case WORK_CHECK_CURR_ACTION: {
ModelAction *act = work.action;
bool update = false; /* update this location's release seq's */
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);
process_thread_action(curr);
if (act->is_write() && process_write(act))
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_all)
+ work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+ else if (update)
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
break;
}
ModelAction * initialize_curr_action(ModelAction *curr);
bool process_read(ModelAction *curr, bool second_part_of_rmw);
bool process_write(ModelAction *curr);
ModelAction * initialize_curr_action(ModelAction *curr);
bool process_read(ModelAction *curr, bool second_part_of_rmw);
bool process_write(ModelAction *curr);
- void process_mutex(ModelAction *curr);
+ bool process_mutex(ModelAction *curr);
bool process_thread_action(ModelAction *curr);
bool check_action_enabled(ModelAction *curr);
bool process_thread_action(ModelAction *curr);
bool check_action_enabled(ModelAction *curr);