From: Brian Demsky Date: Thu, 4 Oct 2012 00:28:26 +0000 (-0700) Subject: Merge branch 'master' of /home/git/model-checker X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=f4d77c40b4029cdc18f4aaa5a4e01dfbcfca5f7b;hp=85683f798e0955c43cf6cd8099713c45d9ce882b Merge branch 'master' of /home/git/model-checker --- diff --git a/action.cc b/action.cc index f80de7b3..20777f96 100644 --- a/action.cc +++ b/action.cc @@ -7,6 +7,7 @@ #include "action.h" #include "clockvector.h" #include "common.h" +#include "threads.h" #define ACTION_INITIAL_CLOCK 0 @@ -248,18 +249,27 @@ void ModelAction::set_try_lock(bool obtainedlock) { value=VALUE_TRYFAILED; } -/** Update the model action's read_from action */ -void ModelAction::read_from(const ModelAction *act) +/** + * Update the model action's read_from action + * @param act The action to read from; should be a write + * @return True if this read established synchronization + */ +bool ModelAction::read_from(const ModelAction *act) { ASSERT(cv); reads_from = act; if (act != NULL && this->is_acquire()) { rel_heads_list_t release_heads; model->get_release_seq_heads(this, &release_heads); + int num_heads = release_heads.size(); for (unsigned int i = 0; i < release_heads.size(); i++) - if (!synchronize_with(release_heads[i])) + if (!synchronize_with(release_heads[i])) { model->set_bad_synchronization(); + num_heads--; + } + return num_heads > 0; } + return false; } /** @@ -292,13 +302,8 @@ bool ModelAction::happens_before(const ModelAction *act) const return act->cv->synchronized_since(this); } -/** - * Print nicely-formatted info about this ModelAction - * - * @param print_cv True if we want to print clock vector data. Might be false, - * for instance, in situations where the clock vector might be invalid - */ -void ModelAction::print(bool print_cv) const +/** @brief Print nicely-formatted info about this ModelAction */ +void ModelAction::print() const { const char *type_str, *mo_str; switch (this->type) { @@ -382,7 +387,7 @@ void ModelAction::print(bool print_cv) const else printf(" Rf: ?"); } - if (cv && print_cv) { + if (cv) { printf("\t"); cv->print(); } else diff --git a/action.h b/action.h index f6fb0623..d178976a 100644 --- a/action.h +++ b/action.h @@ -7,11 +7,13 @@ #include #include +#include -#include "threads.h" #include "mymemory.h" -#include "clockvector.h" #include "memoryorder.h" +#include "modeltypes.h" + +class ClockVector; using std::memory_order; using std::memory_order_relaxed; @@ -64,7 +66,7 @@ class ModelAction { public: ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE); ~ModelAction(); - void print(bool print_cv = true) const; + void print() const; thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } @@ -103,7 +105,7 @@ public: void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } - void read_from(const ModelAction *act); + bool read_from(const ModelAction *act); bool synchronize_with(const ModelAction *act); bool has_synchronized_with(const ModelAction *act) const; diff --git a/clockvector.cc b/clockvector.cc index c5bf0770..2b6a4cc6 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -6,6 +6,7 @@ #include "action.h" #include "clockvector.h" #include "common.h" +#include "threads.h" /** * Constructs a new ClockVector, given a parent ClockVector and a first diff --git a/clockvector.h b/clockvector.h index 739a336e..6a902c52 100644 --- a/clockvector.h +++ b/clockvector.h @@ -5,10 +5,9 @@ #ifndef __CLOCKVECTOR_H__ #define __CLOCKVECTOR_H__ -#include "threads.h" #include "mymemory.h" +#include "modeltypes.h" -typedef unsigned int modelclock_t; /* Forward declaration */ class ModelAction; diff --git a/cmodelint.cc b/cmodelint.cc index 228c40f9..6b20c2cc 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -1,5 +1,6 @@ #include "model.h" #include "cmodelint.h" +#include "threads.h" /** Performs a read action.*/ uint64_t model_read_action(void * obj, memory_order ord) { diff --git a/datarace.cc b/datarace.cc index 29374305..f5501fe0 100644 --- a/datarace.cc +++ b/datarace.cc @@ -4,6 +4,7 @@ #include #include #include "mymemory.h" +#include "clockvector.h" struct ShadowTable *root; std::vector unrealizedraces; @@ -122,8 +123,8 @@ bool checkDataRaces() { void printRace(struct DataRace * race) { printf("Datarace detected\n"); printf("Location %p\n", race->address); - printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite); - printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite); + printf("Initial access: thread %u clock %u, iswrite %u\n", id_to_int(race->oldthread), race->oldclock, race->isoldwrite); + printf("Second access: thread %u clock %u, iswrite %u\n", id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number(), race->isnewwrite); } /** This function does race detection for a write on an expanded record. */ diff --git a/datarace.h b/datarace.h index 5bfcb8ad..627b8cc8 100644 --- a/datarace.h +++ b/datarace.h @@ -5,8 +5,12 @@ #ifndef DATARACE_H #include "config.h" #include -#include "clockvector.h" #include +#include "modeltypes.h" + +/* Forward declaration */ +class ClockVector; +class ModelAction; struct ShadowTable { void * array[65536]; diff --git a/impatomic.cc b/impatomic.cc index df11202d..0a35b4b6 100644 --- a/impatomic.cc +++ b/impatomic.cc @@ -1,6 +1,7 @@ #include "impatomic.h" #include "common.h" #include "model.h" +#include "threads.h" namespace std { diff --git a/librace.cc b/librace.cc index 38434de7..bdd6093a 100644 --- a/librace.cc +++ b/librace.cc @@ -5,6 +5,7 @@ #include "common.h" #include "datarace.h" #include "model.h" +#include "threads.h" void store_8(void *addr, uint8_t val) { diff --git a/libthreads.cc b/libthreads.cc index 4d6a0243..f973176b 100644 --- a/libthreads.cc +++ b/libthreads.cc @@ -23,7 +23,7 @@ int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg) int thrd_join(thrd_t t) { Thread *th = model->get_thread(thrd_to_id(t)); - model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, thrd_to_id(t))); + model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t)))); return 0; } diff --git a/model.cc b/model.cc index c9353db7..e3d9203e 100644 --- a/model.cc +++ b/model.cc @@ -12,6 +12,7 @@ #include "promise.h" #include "datarace.h" #include "mutex.h" +#include "threads.h" #define INITIAL_THREAD_ID 0 @@ -99,6 +100,12 @@ int ModelChecker::get_num_threads() return priv->next_thread_id; } +/** @return The currently executing Thread. */ +Thread * ModelChecker::get_current_thread() +{ + return scheduler->get_current_thread(); +} + /** @return a sequence number for a new ModelAction */ modelclock_t ModelChecker::get_next_seq_num() { @@ -171,7 +178,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) } else { tid = next->get_tid(); } - DEBUG("*** ModelChecker chose next thread = %d ***\n", tid); + DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid)); ASSERT(tid != THREAD_ID_T_NONE); return thread_map->get(id_to_int(tid)); } @@ -192,7 +199,7 @@ bool ModelChecker::next_execution() if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) - earliest_diverge->print(false); + earliest_diverge->print(); else printf("(Not set)\n"); @@ -317,7 +324,8 @@ void ModelChecker::set_backtracking(ModelAction *act) if (!node->set_backtrack(tid)) continue; DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", - prev->get_tid(), t->get_id()); + id_to_int(prev->get_tid()), + id_to_int(t->get_id())); if (DBG_ENABLED()) { prev->print(); act->print(); @@ -787,8 +795,7 @@ bool ModelChecker::isfinalfeasible() { /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ ModelAction * ModelChecker::process_rmw(ModelAction *act) { - int tid = id_to_int(act->get_tid()); - ModelAction *lastread = get_last_action(tid); + ModelAction *lastread = get_last_action(act->get_tid()); lastread->process_rmw(act); if (act->is_rmw() && lastread->get_reads_from()!=NULL) { mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); @@ -1169,7 +1176,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const +bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const { /* Only check for release sequences if there are no cycles */ if (mo_graph->checkForCycles()) @@ -1239,7 +1246,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel ModelAction *last = get_last_action(int_to_id(i)); if (last && (rf->happens_before(last) || - last->get_type() == THREAD_FINISH)) + get_thread(int_to_id(i))->is_complete())) future_ordered = true; for (rit = list->rbegin(); rit != list->rend(); rit++) { @@ -1291,13 +1298,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * @param act The 'acquire' action that may read from a release sequence * @param release_heads A pass-by-reference return parameter. Will be filled * with the head(s) of the release sequence(s), if they exists with certainty. - * @see ModelChecker::release_seq_head + * @see ModelChecker::release_seq_heads */ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); bool complete; - complete = release_seq_head(rf, release_heads); + complete = release_seq_heads(rf, release_heads); if (!complete) { /* add act to 'lazy checking' list */ pending_acq_rel_seq->push_back(act); @@ -1333,7 +1340,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; - complete = release_seq_head(rf, &release_heads); + complete = release_seq_heads(rf, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) { if (!act->has_synchronized_with(release_heads[i])) { if (act->synchronize_with(release_heads[i])) @@ -1701,12 +1708,35 @@ void ModelChecker::remove_thread(Thread *t) scheduler->remove_thread(t); } +/** + * @brief Get a Thread reference by its ID + * @param tid The Thread's ID + * @return A Thread reference + */ +Thread * ModelChecker::get_thread(thread_id_t tid) const +{ + return thread_map->get(id_to_int(tid)); +} + +/** + * @brief Get a reference to the Thread in which a ModelAction was executed + * @param act The ModelAction + * @return A Thread reference + */ +Thread * ModelChecker::get_thread(ModelAction *act) const +{ + return get_thread(act->get_tid()); +} + /** * Switch from a user-context to the "master thread" context (a.k.a. system * context). This switch is made with the intention of exploring a particular * model-checking action (described by a ModelAction object). Must be called * from a user-thread context. - * @param act The current action that will be explored. Must not be NULL. + * + * @param act The current action that will be explored. May be NULL only if + * trace is exiting via an assertion (see ModelChecker::set_assert and + * ModelChecker::has_asserted). * @return Return status from the 'swap' call (i.e., success/fail, 0/-1) */ int ModelChecker::switch_to_master(ModelAction *act) @@ -1726,7 +1756,7 @@ bool ModelChecker::take_step() { if (has_asserted()) return false; - Thread * curr = thread_current(); + Thread *curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); @@ -1740,22 +1770,23 @@ bool ModelChecker::take_step() { ASSERT(false); } } - Thread * next = scheduler->next_thread(priv->nextThread); + Thread *next = scheduler->next_thread(priv->nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) return false; - if (next) - next->set_state(THREAD_RUNNING); - DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); + DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, + next ? id_to_int(next->get_id()) : -1); /* next == NULL -> don't take any more steps */ if (!next) return false; - if ( next->get_pending() != NULL ) { - //restart a pending action + next->set_state(THREAD_RUNNING); + + if (next->get_pending() != NULL) { + /* restart a pending action */ set_current_action(next->get_pending()); next->set_pending(NULL); next->set_state(THREAD_READY); diff --git a/model.h b/model.h index 7241765d..d8dce07c 100644 --- a/model.h +++ b/model.h @@ -10,20 +10,19 @@ #include #include -#include "schedule.h" #include "mymemory.h" -#include "libthreads.h" -#include "threads.h" #include "action.h" -#include "clockvector.h" #include "hashtable.h" #include "workqueue.h" #include "config.h" +#include "modeltypes.h" /* Forward declaration */ class NodeStack; class CycleGraph; class Promise; +class Scheduler; +class Thread; /** @brief Shorthand for a list of release sequence heads */ typedef std::vector< const ModelAction *, ModelAlloc > rel_heads_list_t; @@ -73,14 +72,12 @@ public: void add_thread(Thread *t); void remove_thread(Thread *t); - Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); } - Thread * get_thread(ModelAction *act) { return get_thread(act->get_tid()); } + Thread * get_thread(thread_id_t tid) const; + Thread * get_thread(ModelAction *act) const; thread_id_t get_next_id(); int get_num_threads(); - - /** @return The currently executing Thread. */ - Thread * get_current_thread() { return scheduler->get_current_thread(); } + Thread * get_current_thread(); int switch_to_master(ModelAction *act); ClockVector * get_cv(thread_id_t tid); @@ -151,7 +148,7 @@ private: void post_r_modification_order(ModelAction *curr, const ModelAction *rf); bool r_modification_order(ModelAction *curr, const ModelAction *rf); bool w_modification_order(ModelAction *curr); - bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const; + bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const; bool resolve_release_sequences(void *location, work_queue_t *work_queue); void do_complete_join(ModelAction *join); diff --git a/modeltypes.h b/modeltypes.h new file mode 100644 index 00000000..22221cb5 --- /dev/null +++ b/modeltypes.h @@ -0,0 +1,10 @@ +#ifndef __MODELTYPES_H__ +#define __MODELTYPES_H__ + +typedef int thread_id_t; + +#define THREAD_ID_T_NONE -1 + +typedef unsigned int modelclock_t; + +#endif /* __MODELTYPES_H__ */ diff --git a/mutex.cc b/mutex.cc index 51315d94..6ef297a5 100644 --- a/mutex.cc +++ b/mutex.cc @@ -1,5 +1,7 @@ #include "mutex.h" #include "model.h" +#include "threads.h" +#include "clockvector.h" namespace std { mutex::mutex() { diff --git a/mutex.h b/mutex.h index 828aae53..53fccb2b 100644 --- a/mutex.h +++ b/mutex.h @@ -1,7 +1,7 @@ #ifndef MUTEX_H #define MUTEX_H -#include "threads.h" -#include "clockvector.h" + +#include "modeltypes.h" namespace std { struct mutex_state { diff --git a/nodestack.cc b/nodestack.cc index d5425e33..a7376532 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -4,6 +4,7 @@ #include "action.h" #include "common.h" #include "model.h" +#include "threads.h" /** * @brief Node constructor @@ -273,6 +274,11 @@ bool Node::is_enabled(thread_id_t tid) return thread_id < num_threads && enabled_array[thread_id]; } +bool Node::has_priority(thread_id_t tid) +{ + return fairness[id_to_int(tid)].priority; +} + /** * Add an action to the may_read_from set. * @param act is the action to add diff --git a/nodestack.h b/nodestack.h index 8df67838..fca063e7 100644 --- a/nodestack.h +++ b/nodestack.h @@ -8,11 +8,13 @@ #include #include #include -#include "threads.h" +#include + #include "mymemory.h" -#include "clockvector.h" +#include "modeltypes.h" class ModelAction; +class Thread; /** * A flag used for the promise counting/combination problem within a node, @@ -64,7 +66,7 @@ public: bool is_enabled(Thread *t); bool is_enabled(thread_id_t tid); ModelAction * get_action() { return action; } - bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;} + bool has_priority(thread_id_t tid); int get_num_threads() {return num_threads;} /** @return the parent Node to this Node; that is, the action that * occurred previously in the stack. */ diff --git a/schedule.cc b/schedule.cc index b1b41c3d..88200a81 100644 --- a/schedule.cc +++ b/schedule.cc @@ -36,7 +36,7 @@ void Scheduler::set_enabled(Thread *t, bool enabled_status) { */ void Scheduler::add_thread(Thread *t) { - DEBUG("thread %d\n", t->get_id()); + DEBUG("thread %d\n", id_to_int(t->get_id())); set_enabled(t, true); } @@ -119,7 +119,7 @@ Thread * Scheduler::get_current_thread() const void Scheduler::print() const { if (current) - DEBUG("Current thread: %d\n", current->get_id()); + DEBUG("Current thread: %d\n", id_to_int(current->get_id())); else DEBUG("No current thread\n"); } diff --git a/threads.cc b/threads.cc index 09efcae6..ca4b28b1 100644 --- a/threads.cc +++ b/threads.cc @@ -105,7 +105,7 @@ int Thread::swap(ucontext_t *ctxt, Thread *t) void Thread::complete() { if (!is_complete()) { - DEBUG("completed thread %d\n", get_id()); + DEBUG("completed thread %d\n", id_to_int(get_id())); state = THREAD_COMPLETED; if (stack) stack_free(stack); diff --git a/threads.h b/threads.h index 9456a22f..b69f4265 100644 --- a/threads.h +++ b/threads.h @@ -11,10 +11,7 @@ #include "mymemory.h" #include "libthreads.h" - -typedef int thread_id_t; - -#define THREAD_ID_T_NONE -1 +#include "modeltypes.h" /** @brief Represents the state of a user Thread */ typedef enum thread_state {