From 21c976cef707ef9ccd33ec72f07a297b4cec057d Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Tue, 17 Jul 2012 22:03:01 -0700 Subject: [PATCH] model: add support for modification orders This update adds support for modification orders and kills the bogus executions seen before... [Updated, split by Brian Norris] --- main.cc | 2 ++ model.cc | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++++--- model.h | 6 +++++ 3 files changed, 86 insertions(+), 3 deletions(-) diff --git a/main.cc b/main.cc index 339b85e..cbf93b6 100644 --- a/main.cc +++ b/main.cc @@ -31,6 +31,8 @@ static int thread_system_next(void) { ASSERT(false); } next = model->scheduler->next_thread(); + if (!model->isfeasible()) + return 1; if (next) next->set_state(THREAD_RUNNING); DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); diff --git a/model.cc b/model.cc index e9d1f1d..3180991 100644 --- a/model.cc +++ b/model.cc @@ -7,6 +7,7 @@ #include "snapshot-interface.h" #include "common.h" #include "clockvector.h" +#include "cyclegraph.h" #define INITIAL_THREAD_ID 0 @@ -31,7 +32,8 @@ ModelChecker::ModelChecker() obj_thrd_map(new std::map >()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), - next_backtrack(NULL) + next_backtrack(NULL), + cyclegraph(new CycleGraph()) { } @@ -49,6 +51,7 @@ ModelChecker::~ModelChecker() delete thrd_last_action; delete node_stack; delete scheduler; + delete cyclegraph; } /** @@ -279,8 +282,6 @@ void ModelChecker::check_current_action(void) set_backtracking(curr); - add_action_to_lists(curr); - /* Assign reads_from values */ /* TODO: perform release/acquire synchronization here; include * reads_from as ModelAction member? */ @@ -291,8 +292,80 @@ void ModelChecker::check_current_action(void) value = reads_from->get_value(); /* Assign reads_from, perform release/acquire synchronization */ curr->read_from(reads_from); + r_modification_order(curr,reads_from); + } else if (curr->is_write()) { + w_modification_order(curr); } + th->set_return_value(value); + + /* Add action to list last. */ + add_action_to_lists(curr); +} + +bool ModelChecker::isfeasible() { + return !cyclegraph->checkForCycles(); +} + +void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) { + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + ASSERT(curr->is_read()); + + /* Iterate over all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + /* Iterate over actions in thread, starting from most recent */ + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + + /* Include at most one act per-thread that "happens before" curr */ + if (act->happens_before(curr)) { + if (act->is_read()) { + const ModelAction * prevreadfrom=act->get_reads_from(); + if (rf!=prevreadfrom) + cyclegraph->addEdge(rf, prevreadfrom); + } else if (rf!=act) { + cyclegraph->addEdge(rf, act); + } + break; + } + } + } +} + +void ModelChecker::w_modification_order(ModelAction * curr) { + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + ASSERT(curr->is_write()); + + if (curr->is_seqcst()) { + /* We have to at least see the last sequentially consistent write, + so we are initialized. */ + ModelAction * last_seq_cst=get_last_seq_cst(curr->get_location()); + if (last_seq_cst!=NULL) + cyclegraph->addEdge(curr, last_seq_cst); + } + + /* Iterate over all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + /* Iterate over actions in thread, starting from most recent */ + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + + /* Include at most one act per-thread that "happens before" curr */ + if (act->happens_before(curr)) { + if (act->is_read()) { + cyclegraph->addEdge(curr, act->get_reads_from()); + } else + cyclegraph->addEdge(curr, act); + break; + } + } + } } /** @@ -446,6 +519,8 @@ void ModelChecker::print_summary(void) printf("\n"); printf("Number of executions: %d\n", num_executions); printf("Total nodes created: %d\n", node_stack->get_total_nodes()); + if (!isfeasible()) + printf("INFEASIBLE EXECUTION!\n"); scheduler->print(); diff --git a/model.h b/model.h index 2093bf4..4c0af0a 100644 --- a/model.h +++ b/model.h @@ -21,6 +21,7 @@ /* Forward declaration */ class NodeStack; +class CycleGraph; /** @brief The central structure for model-checking */ class ModelChecker { @@ -55,6 +56,7 @@ public: int switch_to_master(ModelAction *act); ClockVector * get_cv(thread_id_t tid); bool next_execution(); + bool isfeasible(); MEMALLOC private: @@ -81,6 +83,9 @@ private: ModelAction * get_parent_action(thread_id_t tid); ModelAction * get_last_seq_cst(const void *location); void build_reads_from_past(ModelAction *curr); + void r_modification_order(ModelAction * curr, const ModelAction *rf); + void w_modification_order(ModelAction * curr); + ModelAction *current_action; ModelAction *diverge; @@ -98,6 +103,7 @@ private: std::vector *thrd_last_action; NodeStack *node_stack; ModelAction *next_backtrack; + CycleGraph * cyclegraph; }; extern ModelChecker *model; -- 2.34.1