projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
main: change default future value sloppiness
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 1e730d794baca5dc99387053bb98125b3756193a..b29df05cafe86fadefa27b85c535e30eb94fd43e 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-208,7
+208,7
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
return thread_map->get(id_to_int(tid));
}
return thread_map->get(id_to_int(tid));
}
-/**
+/**
* We need to know what the next actions of all threads in the sleep
* set will be. This method computes them and stores the actions at
* the corresponding thread object's pending action.
* We need to know what the next actions of all threads in the sleep
* set will be. This method computes them and stores the actions at
* the corresponding thread object's pending action.
@@
-241,7
+241,7
@@
void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
scheduler->remove_sleep(thr);
}
}
scheduler->remove_sleep(thr);
}
}
- }
+ }
}
/**
}
/**
@@
-393,7
+393,7
@@
void ModelChecker::set_backtracking(ModelAction *act)
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid)!=THREAD_ENABLED)
continue;
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid)!=THREAD_ENABLED)
continue;
-
+
/* Check if this has been explored already */
if (node->has_been_explored(tid))
continue;
/* Check if this has been explored already */
if (node->has_been_explored(tid))
continue;
@@
-1066,7
+1066,7
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
ModelAction *act = *rit;
if (!act->is_read())
return;
ModelAction *act = *rit;
if (!act->is_read())
return;
-
+
if (act->get_reads_from() != rf)
return;
if (act->get_node()->get_read_from_size() <= 1)
if (act->get_reads_from() != rf)
return;
if (act->get_node()->get_read_from_size() <= 1)
@@
-1291,7
+1291,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
* 1) If RMW and it actually read from something, then we
* already have all relevant edges, so just skip to next
* thread.
* 1) If RMW and it actually read from something, then we
* already have all relevant edges, so just skip to next
* thread.
- *
+ *
* 2) If RMW and it didn't read from anything, we should
* whatever edge we can get to speed up convergence.
*
* 2) If RMW and it didn't read from anything, we should
* whatever edge we can get to speed up convergence.
*
@@
-1301,7
+1301,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
if (curr->is_rmw()) {
if (curr->get_reads_from()!=NULL)
break;
if (curr->is_rmw()) {
if (curr->get_reads_from()!=NULL)
break;
- else
+ else
continue;
} else
continue;
continue;
} else
continue;
@@
-1320,7
+1320,7
@@
bool ModelChecker::w_modification_order(ModelAction *curr)
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
- else if (act->is_read()) {
+ else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
@@
-1388,7
+1388,6
@@
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
unsigned int i;
{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
unsigned int i;
-
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
const ModelAction *write_after_read = NULL;
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
const ModelAction *write_after_read = NULL;
@@
-1403,15
+1402,14
@@
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
break;
else if (act->is_write())
write_after_read = act;
break;
else if (act->is_write())
write_after_read = act;
- else if (act->is_read()
&&act->get_reads_from()!=NULL
) {
+ else if (act->is_read()
&& act->get_reads_from() != NULL && act != reader
) {
write_after_read = act->get_reads_from();
}
}
write_after_read = act->get_reads_from();
}
}
-
+
if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
return false;
}
if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
return false;
}
-
return true;
}
return true;
}
@@
-1692,7
+1690,7
@@
void ModelChecker::add_action_to_lists(ModelAction *act)
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
obj_map->get_safe_ptr(mutex_loc)->push_back(act);
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
obj_map->get_safe_ptr(mutex_loc)->push_back(act);
-
+
std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
@@
-1804,7
+1802,7
@@
bool ModelChecker::resolve_promises(ModelAction *write)
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
delete(promise);
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
delete(promise);
-
+
promises->erase(promises->begin() + promise_index);
threads_to_check.push_back(read->get_tid());
promises->erase(promises->begin() + promise_index);
threads_to_check.push_back(read->get_tid());
@@
-1874,7
+1872,7
@@
void ModelChecker::check_promises_thread_disabled() {
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
- *
+ *
* pread is the read that created the promise
*
* pwrite is either the first write to same location as pread by
* pread is the read that created the promise
*
* pwrite is either the first write to same location as pread by
@@
-1903,7
+1901,7
@@
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *act = promise->get_action();
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *act = promise->get_action();
-
+
//Is this promise on the same location?
if ( act->get_location() != location )
continue;
//Is this promise on the same location?
if ( act->get_location() != location )
continue;
@@
-1925,11
+1923,11
@@
void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
return;
}
}
return;
}
}
-
+
//Don't do any lookups twice for the same thread
if (promise->has_sync_thread(tid))
continue;
//Don't do any lookups twice for the same thread
if (promise->has_sync_thread(tid))
continue;
-
+
if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
@@
-2002,17
+2000,14
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
- DEBUG("Adding action to may_read_from:\n");
- if (DBG_ENABLED()) {
- act->print();
- curr->print();
- }
-
- if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
- if (sleep_can_read_from(curr, act))
- curr->get_node()->add_read_from(act);
- } else
+ if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
+ DEBUG("Adding action to may_read_from:\n");
+ if (DBG_ENABLED()) {
+ act->print();
+ curr->print();
+ }
curr->get_node()->add_read_from(act);
curr->get_node()->add_read_from(act);
+ }
}
/* Include at most one act per-thread that "happens before" curr */
}
/* Include at most one act per-thread that "happens before" curr */
@@
-2041,7
+2036,7
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
while(true) {
Node *prevnode=write->get_node()->get_parent();
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
while(true) {
Node *prevnode=write->get_node()->get_parent();
-
+
bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
if (write->is_release()&&thread_sleep)
return true;
bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
if (write->is_release()&&thread_sleep)
return true;
@@
-2061,7
+2056,7
@@
static void print_list(action_list_t *list)
printf("---------------------------------------------------------------------\n");
printf("Trace:\n");
unsigned int hash=0;
printf("---------------------------------------------------------------------\n");
printf("Trace:\n");
unsigned int hash=0;
-
+
for (it = list->begin(); it != list->end(); it++) {
(*it)->print();
hash=hash^(hash<<3)^((*it)->hash());
for (it = list->begin(); it != list->end(); it++) {
(*it)->print();
hash=hash^(hash<<3)^((*it)->hash());
@@
-2073,12
+2068,12
@@
static void print_list(action_list_t *list)
#if SUPPORT_MOD_ORDER_DUMP
void ModelChecker::dumpGraph(char *filename) {
char buffer[200];
#if SUPPORT_MOD_ORDER_DUMP
void ModelChecker::dumpGraph(char *filename) {
char buffer[200];
- sprintf(buffer, "%s.dot",filename);
- FILE *file=fopen(buffer, "w");
- fprintf(file, "digraph %s {\n",filename);
+
sprintf(buffer, "%s.dot",filename);
+
FILE *file=fopen(buffer, "w");
+
fprintf(file, "digraph %s {\n",filename);
mo_graph->dumpNodes(file);
ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
mo_graph->dumpNodes(file);
ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
-
+
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
ModelAction *action=*it;
if (action->is_read()) {
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
ModelAction *action=*it;
if (action->is_read()) {
@@
-2089,12
+2084,12
@@
void ModelChecker::dumpGraph(char *filename) {
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());
}
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());
}
-
+
thread_array[action->get_tid()]=action;
}
thread_array[action->get_tid()]=action;
}
- fprintf(file,"}\n");
+
fprintf(file,"}\n");
model_free(thread_array);
model_free(thread_array);
- fclose(file);
+ fclose(file);
}
#endif
}
#endif
@@
-2111,7
+2106,7
@@
void ModelChecker::print_summary()
sprintf(buffername, "exec%04u", num_executions);
mo_graph->dumpGraphToFile(buffername);
sprintf(buffername, "graph%04u", num_executions);
sprintf(buffername, "exec%04u", num_executions);
mo_graph->dumpGraphToFile(buffername);
sprintf(buffername, "graph%04u", num_executions);
- dumpGraph(buffername);
+
dumpGraph(buffername);
#endif
if (!isfinalfeasible())
#endif
if (!isfinalfeasible())
@@
-2132,7
+2127,7
@@
void ModelChecker::add_thread(Thread *t)
}
/**
}
/**
- * Removes a thread from the scheduler.
+ * Removes a thread from the scheduler.
* @param the thread to remove.
*/
void ModelChecker::remove_thread(Thread *t)
* @param the thread to remove.
*/
void ModelChecker::remove_thread(Thread *t)