From c832cb55af09e735821ae3463bc37c29d3fa27c8 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Thu, 4 Oct 2012 01:21:11 -0700 Subject: [PATCH] local commit... bug that prunes too many executions --- Makefile | 2 +- action.cc | 2 +- cyclegraph.cc | 29 +++++++++++++++++++++++++++++ cyclegraph.h | 3 ++- model.cc | 51 ++++++++++++++++++++++++++++++++++++++++++++------- model.h | 8 +++++--- promise.cc | 21 +++++++++++++++++++++ promise.h | 25 ++++++++++++++++++++----- threads.h | 8 ++++++++ 9 files changed, 131 insertions(+), 18 deletions(-) create mode 100644 promise.cc diff --git a/Makefile b/Makefile index 3a3d826..d530fee 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ include common.mk OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ datarace.o impatomic.o cmodelint.o \ - snapshot.o malloc.o mymemory.o common.o mutex.o + snapshot.o malloc.o mymemory.o common.o mutex.o promise.o CPPFLAGS += -Iinclude -I. -rdynamic LDFLAGS = -ldl -lrt diff --git a/action.cc b/action.cc index 20777f9..c6504cd 100644 --- a/action.cc +++ b/action.cc @@ -281,7 +281,7 @@ bool ModelAction::read_from(const ModelAction *act) bool ModelAction::synchronize_with(const ModelAction *act) { if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK) return false; - model->check_promises(cv, act->cv); + model->check_promises(act->get_tid(), cv, act->cv); cv->merge(act->cv); return true; } diff --git a/cyclegraph.cc b/cyclegraph.cc index f4d3b93..2280e76 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,6 +1,8 @@ #include "cyclegraph.h" #include "action.h" #include "common.h" +#include "promise.h" +#include "model.h" /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : @@ -195,6 +197,33 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { return false; } +bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) { + std::vector > queue; + HashTable discovered(64); + CycleNode *from = actionToNode.get(fromact); + + + queue.push_back(from); + discovered.put(from, from); + while(!queue.empty()) { + CycleNode * node=queue.back(); + queue.pop_back(); + + if (promise->increment_threads(node->getAction()->get_tid())) { + return true; + } + + for(unsigned int i=0;igetEdges()->size();i++) { + CycleNode *next=(*node->getEdges())[i]; + if (!discovered.contains(next)) { + discovered.put(next,next); + queue.push_back(next); + } + } + } + return false; +} + void CycleGraph::startChanges() { ASSERT(rollbackvector.size()==0); ASSERT(rmwrollbackvector.size()==0); diff --git a/cyclegraph.h b/cyclegraph.h index 42866a3..1cc0d06 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -11,6 +11,7 @@ #include "config.h" #include "mymemory.h" +class Promise; class CycleNode; class ModelAction; @@ -23,7 +24,7 @@ class CycleGraph { bool checkForCycles(); bool checkForRMWViolation(); void addRMWEdge(const ModelAction *from, const ModelAction *rmw); - + bool checkPromise(const ModelAction *from, Promise *p); bool checkReachable(const ModelAction *from, const ModelAction *to); void startChanges(); void commitChanges(); diff --git a/model.cc b/model.cc index e3d9203..824e1e4 100644 --- a/model.cc +++ b/model.cc @@ -52,7 +52,7 @@ ModelChecker::ModelChecker(struct model_params params) : /** @brief Destructor */ ModelChecker::~ModelChecker() { - for (int i = 0; i < get_num_threads(); i++) + for (unsigned int i = 0; i < get_num_threads(); i++) delete thread_map->get(i); delete thread_map; @@ -95,7 +95,7 @@ thread_id_t ModelChecker::get_next_id() } /** @return the number of user threads created during this execution */ -int ModelChecker::get_num_threads() +unsigned int ModelChecker::get_num_threads() { return priv->next_thread_id; } @@ -377,6 +377,8 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) curr->read_from(reads_from); mo_graph->commitChanges(); + mo_check_promises(curr->get_tid(), reads_from); + updated |= r_status; } else if (!second_part_of_rmw) { /* Read from future value */ @@ -474,6 +476,8 @@ bool ModelChecker::process_write(ModelAction *curr) } mo_graph->commitChanges(); + mo_check_promises(curr->get_tid(), curr); + get_thread(curr)->set_return_value(VALUE_NONE); return updated_mod_order || updated_promises; } @@ -526,7 +530,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } case THREAD_START: { - check_promises(NULL, curr->get_cv()); + check_promises(curr->get_tid(), NULL, curr->get_cv()); break; } default: @@ -1503,6 +1507,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) post_r_modification_order(read, write); //Make sure the promise's value matches the write's value ASSERT(promise->get_value() == write->get_value()); + mo_check_promises(read->get_tid(), write); delete(promise); promises->erase(promises->begin() + promise_index); @@ -1535,16 +1540,14 @@ void ModelChecker::compute_promises(ModelAction *curr) } /** Checks promises in response to change in ClockVector Threads. */ -void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) +void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv) { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; const ModelAction *act = promise->get_action(); if ((old_cv == NULL || !old_cv->synchronized_since(act)) && merge_cv->synchronized_since(act)) { - //This thread is no longer able to send values back to satisfy the promise - int num_synchronized_threads = promise->increment_threads(); - if (num_synchronized_threads == get_num_threads()) { + if (promise->increment_threads(tid)) { //Promise has failed failed_promise = true; return; @@ -1553,6 +1556,40 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) } } +/** Checks promises in response to change in ClockVector Threads. */ +void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) { + void * location = write->get_location(); + 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; + + if ( act->get_tid()==tid) { + if (promise->get_write() == NULL ) { + promise->set_write(write); + } + if (mo_graph->checkPromise(write, promise)) { + failed_promise = true; + return; + } + } + + //Don't do any lookups twice for the same thread + if (promise->has_sync_thread(tid)) + continue; + + if (mo_graph->checkReachable(promise->get_write(), write)) { + if (promise->increment_threads(tid)) { + failed_promise = true; + return; + } + } + } +} + /** * Build up an initial set of all past writes that this 'read' action may read * from. This set is determined by the clock vector's "happens before" diff --git a/model.h b/model.h index d8dce07..dfc8e36 100644 --- a/model.h +++ b/model.h @@ -49,7 +49,7 @@ struct PendingFutureValue { */ struct model_snapshot_members { ModelAction *current_action; - int next_thread_id; + unsigned int next_thread_id; modelclock_t used_sequence_numbers; Thread *nextThread; ModelAction *next_backtrack; @@ -76,7 +76,7 @@ public: Thread * get_thread(ModelAction *act) const; thread_id_t get_next_id(); - int get_num_threads(); + unsigned int get_num_threads(); Thread * get_current_thread(); int switch_to_master(ModelAction *act); @@ -86,7 +86,8 @@ public: bool isfeasible(); bool isfeasibleotherthanRMW(); bool isfinalfeasible(); - void check_promises(ClockVector *old_cv, ClockVector * merge_cv); + void mo_check_promises(thread_id_t tid, const ModelAction *write); + void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv); void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads); void finish_execution(); bool isfeasibleprefix(); @@ -97,6 +98,7 @@ public: void set_bad_synchronization() { bad_synchronization = true; } const model_params params; + Scheduler * get_scheduler() { return scheduler;} MEMALLOC private: diff --git a/promise.cc b/promise.cc new file mode 100644 index 0000000..259ba05 --- /dev/null +++ b/promise.cc @@ -0,0 +1,21 @@ +#include "promise.h" +#include "model.h" +#include "schedule.h" + +bool Promise::increment_threads(thread_id_t tid) { + unsigned int id=id_to_int(tid); + if (id>=synced_thread.size()) { + synced_thread.resize(id+1, false); + } + if (synced_thread[id]) + return false; + + synced_thread[id]=true; + bool * enabled=model->get_scheduler()->get_enabled(); + + for(unsigned int i=0;iget_num_threads();i++) { + if (!synced_thread[id] && enabled[id]) + return false; + } + return true; +} diff --git a/promise.h b/promise.h index 11719fc..2ce3e29 100644 --- a/promise.h +++ b/promise.h @@ -8,25 +8,40 @@ #define __PROMISE_H__ #include +#include "threads.h" -class ModelAction; +#include "model.h" class Promise { public: Promise(ModelAction *act, uint64_t value, modelclock_t expiration) : - value(value), expiration(expiration), read(act), numthreads(1) - { } + value(value), expiration(expiration), read(act), write(NULL) + { + increment_threads(act->get_tid()); + } modelclock_t get_expiration() const {return expiration;} ModelAction * get_action() const { return read; } - int increment_threads() { return ++numthreads; } + bool increment_threads(thread_id_t tid); + + bool has_sync_thread(thread_id_t tid) { + unsigned int id=id_to_int(tid); + if (id>=synced_thread.size()) { + return false; + } + return synced_thread[id]; + } + uint64_t get_value() const { return value; } + void set_write(const ModelAction *act) { write = act; } + const ModelAction * get_write() { return write; } SNAPSHOTALLOC private: + std::vector synced_thread; const uint64_t value; const modelclock_t expiration; ModelAction * const read; - unsigned int numthreads; + const ModelAction * write; }; #endif diff --git a/threads.h b/threads.h index b69f426..a379494 100644 --- a/threads.h +++ b/threads.h @@ -81,6 +81,14 @@ public: */ void push_wait_list(ModelAction *act) { wait_list.push_back(act); } + unsigned int num_wait_list() { + return wait_list.size(); + } + + ModelAction * get_waiter(unsigned int i) { + return wait_list[i]; + } + ModelAction * get_pending() { return pending; } void set_pending(ModelAction *act) { pending = act; } /** -- 2.34.1