X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=afb72b0aae490bda4a0464bb04837b380d81f4ca;hp=5941cf27f5f0d89523fe8a27a6581eb3184d7203;hb=07b041c2dd6958bb3a52ffcba07e8e642130548c;hpb=4fa31aac91303266f4c87a6cd5d60cbab34135db diff --git a/model.cc b/model.cc index 5941cf2..afb72b0 100644 --- a/model.cc +++ b/model.cc @@ -16,25 +16,13 @@ #include "datarace.h" #include "threads-model.h" #include "output.h" +#include "traceanalysis.h" +#include "bugmessage.h" #define INITIAL_THREAD_ID 0 ModelChecker *model; -struct bug_message { - bug_message(const char *str) { - const char *fmt = " [BUG] %s\n"; - msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str)); - sprintf(msg, fmt, str); - } - ~bug_message() { if (msg) snapshot_free(msg); } - - char *msg; - void print() { model_print("%s", msg); } - - SNAPSHOTALLOC -}; - /** * Structure for holding small ModelChecker members that should be snapshotted */ @@ -92,6 +80,7 @@ ModelChecker::ModelChecker(struct model_params params) : thrd_last_action(new SnapVector(1)), thrd_last_fence_release(new SnapVector()), node_stack(new NodeStack()), + trace_analyses(new ModelVector()), priv(new struct model_snapshot_members()), mo_graph(new CycleGraph()) { @@ -121,6 +110,9 @@ ModelChecker::~ModelChecker() delete thrd_last_action; delete thrd_last_fence_release; delete node_stack; + for (unsigned int i = 0; i < trace_analyses->size(); i++) + delete (*trace_analyses)[i]; + delete trace_analyses; delete scheduler; delete mo_graph; delete priv; @@ -146,6 +138,18 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *wrv=obj_thrd_map->get(obj); + if (wrv==NULL) + return NULL; + unsigned int thread=id_to_int(tid); + if (thread < wrv->size()) + return &(*wrv)[thread]; + else + return NULL; +} + + /** * Restores user program to initial state and resets all model-checker data * structures. @@ -553,6 +557,7 @@ bool ModelChecker::next_execution() assert_bug("Deadlock detected"); checkDataRaces(); + run_trace_analyses(); } record_stats(); @@ -578,6 +583,12 @@ bool ModelChecker::next_execution() return true; } +/** @brief Run trace analyses on complete trace */ +void ModelChecker::run_trace_analyses() { + for (unsigned int i = 0; i < trace_analyses->size(); i++) + (*trace_analyses)[i]->analyze(action_trace); +} + /** * @brief Find the last fence-related backtracking conflict for a ModelAction * @@ -968,7 +979,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement if (unlock != NULL) { - curr->synchronize_with(unlock); + synchronize(unlock, curr); return true; } break; @@ -1178,8 +1189,7 @@ bool ModelChecker::process_fence(ModelAction *curr) rel_heads_list_t release_heads; get_release_seq_heads(curr, act, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) - if (!curr->synchronize_with(release_heads[i])) - set_bad_synchronization(); + synchronize(release_heads[i], curr); if (release_heads.size() != 0) updated = true; } @@ -1220,7 +1230,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) case THREAD_JOIN: { Thread *blocking = curr->get_thread_operand(); ModelAction *act = get_last_action(blocking->get_id()); - curr->synchronize_with(act); + synchronize(act, curr); updated = true; /* trigger rel-seq checks */ break; } @@ -1294,10 +1304,8 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu */ /* Must synchronize */ - if (!acquire->synchronize_with(release)) { - set_bad_synchronization(); + if (!synchronize(release, acquire)) return; - } /* Re-check all pending release sequences */ work_queue->push_back(CheckRelSeqWorkEntry(NULL)); /* Re-check act for mo_graph edges */ @@ -1308,7 +1316,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; if (acquire->happens_before(propagate)) { - propagate->synchronize_with(acquire); + synchronize(acquire, propagate); /* Re-check 'propagate' for mo_graph edges */ work_queue->push_back(MOEdgeWorkEntry(propagate)); } @@ -1417,15 +1425,35 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf) get_release_seq_heads(act, act, &release_heads); int num_heads = release_heads.size(); for (unsigned int i = 0; i < release_heads.size(); i++) - if (!act->synchronize_with(release_heads[i])) { - set_bad_synchronization(); + if (!synchronize(release_heads[i], act)) num_heads--; - } return num_heads > 0; } return false; } +/** + * @brief Synchronizes two actions + * + * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector. + * This function performs the synchronization as well as providing other hooks + * for other checks along with synchronization. + * + * @param first The left-hand side of the synchronizes-with relation + * @param second The right-hand side of the synchronizes-with relation + * @return True if the synchronization was successful (i.e., was consistent + * with the execution order); false otherwise + */ +bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second) +{ + if (*second < *first) { + set_bad_synchronization(); + return false; + } + check_promises(first->get_tid(), second->get_cv(), first->get_cv()); + return second->synchronize_with(first); +} + /** * Check promises and eliminate potentially-satisfying threads when a thread is * blocked (e.g., join, lock). A thread which is waiting on another thread can @@ -2344,14 +2372,10 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ rel_heads_list_t release_heads; bool complete; complete = release_seq_heads(rf, &release_heads, pending); - for (unsigned int i = 0; i < release_heads.size(); i++) { - if (!acquire->has_synchronized_with(release_heads[i])) { - if (acquire->synchronize_with(release_heads[i])) + for (unsigned int i = 0; i < release_heads.size(); i++) + if (!acquire->has_synchronized_with(release_heads[i])) + if (synchronize(release_heads[i], acquire)) updated = true; - else - set_bad_synchronization(); - } - } if (updated) { /* Re-check all pending release sequences */ @@ -2365,7 +2389,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; if (acquire->happens_before(propagate)) { - propagate->synchronize_with(acquire); + synchronize(acquire, propagate); /* Re-check 'propagate' for mo_graph edges */ work_queue->push_back(MOEdgeWorkEntry(propagate)); } @@ -3089,6 +3113,12 @@ void user_main_wrapper(void *) user_main(model->params.argc, model->params.argv); } +/** @return True if the execution has taken too many steps */ +bool ModelChecker::too_many_steps() const +{ + return params.bound != 0 && priv->used_sequence_numbers > params.bound; +} + bool ModelChecker::should_terminate_execution() { /* Infeasible -> don't take any more steps */ @@ -3099,7 +3129,7 @@ bool ModelChecker::should_terminate_execution() return true; } - if (params.bound != 0 && priv->used_sequence_numbers > params.bound) + if (too_many_steps()) return true; return false; }