tid = prevnode->get_next_backtrack();
/* Make sure the backtracked thread isn't sleeping. */
node_stack->pop_restofstack(1);
tid = prevnode->get_next_backtrack();
/* Make sure the backtracked thread isn't sleeping. */
node_stack->pop_restofstack(1);
-bool ModelChecker::process_mutex(ModelAction *curr) {
- std::mutex *mutex=NULL;
- struct std::mutex_state *state=NULL;
+bool ModelChecker::process_mutex(ModelAction *curr)
+{
+ std::mutex *mutex = NULL;
+ struct std::mutex_state *state = NULL;
if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
mutex = (std::mutex *)curr->get_location();
if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
mutex = (std::mutex *)curr->get_location();
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
scheduler->sleep(get_current_thread());
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
scheduler->sleep(get_current_thread());
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
action_list_t::iterator it = waiters->begin();
advance(it, wakeupthread);
scheduler->wake(get_thread(*it));
action_list_t::iterator it = waiters->begin();
advance(it, wakeupthread);
scheduler->wake(get_thread(*it));
ModelAction * ModelChecker::process_rmw(ModelAction *act) {
ModelAction *lastread = get_last_action(act->get_tid());
lastread->process_rmw(act);
ModelAction * ModelChecker::process_rmw(ModelAction *act) {
ModelAction *lastread = get_last_action(act->get_tid());
lastread->process_rmw(act);
mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
mo_graph->commitChanges();
}
mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
mo_graph->commitChanges();
}
//Case 1: The resolved read is a RMW, and we need to make sure
//that the write portion of the RMW mod order after rf
//Case 1: The resolved read is a RMW, and we need to make sure
//that the write portion of the RMW mod order after rf
mo_graph->addEdge(rf, postreadfrom);
} else {
//Case 3: The resolved read is a normal read and the next
//operation is a write, and we need to make sure that the
//write is mod ordered after rf
mo_graph->addEdge(rf, postreadfrom);
} else {
//Case 3: The resolved read is a normal read and the next
//operation is a write, and we need to make sure that the
//write is mod ordered after rf
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
//do we have a pwrite for the promise, if not, set it
if (promise->get_write() == NULL ) {
//do we have a pwrite for the promise, if not, set it
if (promise->get_write() == NULL ) {
}
model_print("HASH %u\n", hash);
model_print("---------------------------------------------------------------------\n");
}
model_print("HASH %u\n", hash);
model_print("---------------------------------------------------------------------\n");
void ModelChecker::dumpGraph(char *filename) {
char buffer[200];
sprintf(buffer, "%s.dot",filename);
void ModelChecker::dumpGraph(char *filename) {
char buffer[200];
sprintf(buffer, "%s.dot",filename);
fprintf(file, "digraph %s {\n",filename);
mo_graph->dumpNodes(file);
fprintf(file, "digraph %s {\n",filename);
mo_graph->dumpNodes(file);
if (action->is_read()) {
fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
if (action->is_read()) {
fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
}
if (thread_array[action->get_tid()] != NULL) {
fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
}
fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
}
if (thread_array[action->get_tid()] != NULL) {
fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
}