From 07a0b575fabd521fb3f4a3f1f2483d46349c35dd Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 1 Jul 2019 23:02:15 -0700 Subject: [PATCH] memoize hb in writes --- action.cc | 8 +- action.h | 9 ++- clockvector.cc | 6 +- common.h | 24 +++--- execution.cc | 181 ++++++++++++++------------------------------ execution.h | 32 ++------ fuzzer.cc | 2 +- fuzzer.h | 2 +- include/impatomic.h | 26 +++---- include/wildcard.h | 4 +- model.cc | 18 ++--- nodestack.cc | 3 +- nodestack.h | 2 +- printf.c | 3 + printf.h | 6 +- 15 files changed, 123 insertions(+), 203 deletions(-) diff --git a/action.cc b/action.cc index 3059e0d9..8dcc9d51 100644 --- a/action.cc +++ b/action.cc @@ -39,6 +39,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, last_fence_release(NULL), node(NULL), cv(NULL), + rf_cv(NULL), value(value), type(type), order(order), @@ -73,6 +74,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, last_fence_release(NULL), node(NULL), cv(NULL), + rf_cv(NULL), value(value), type(type), order(order), @@ -107,6 +109,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order last_fence_release(NULL), node(NULL), cv(NULL), + rf_cv(NULL), value(value), type(type), order(order), @@ -142,6 +145,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order last_fence_release(NULL), node(NULL), cv(NULL), + rf_cv(NULL), value(value), type(type), order(order), @@ -591,7 +595,7 @@ Node * ModelAction::get_node() const * Update the model action's read_from action * @param act The action to read from; should be a write */ -void ModelAction::set_read_from(const ModelAction *act) +void ModelAction::set_read_from(ModelAction *act) { ASSERT(act); @@ -601,7 +605,7 @@ void ModelAction::set_read_from(const ModelAction *act) uint64_t val = *((uint64_t *) location); ModelAction * act_initialized = (ModelAction *)act; act_initialized->set_value(val); - reads_from = (const ModelAction *)act_initialized; + reads_from = act_initialized; // disabled by WL, because LLVM IR is unable to detect atomic init /* model->assert_bug("May read from uninitialized atomic:\n" diff --git a/action.h b/action.h index c7703094..5e8b1b1c 100644 --- a/action.h +++ b/action.h @@ -103,13 +103,13 @@ public: uint64_t get_reads_from_value() const; uint64_t get_write_value() const; uint64_t get_return_value() const; - const ModelAction * get_reads_from() const { return reads_from; } + ModelAction * get_reads_from() const { return reads_from; } cdsc::mutex * get_mutex() const; Node * get_node() const; void set_node(Node *n) { node = n; } - void set_read_from(const ModelAction *act); + void set_read_from(ModelAction *act); /** Store the most recent fence-release from the same thread * @param fence The fence-release that occured prior to this */ @@ -156,6 +156,8 @@ public: Thread * get_thread_operand() const; void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } + ClockVector * get_rfcv() const { return rf_cv; } + void set_rfcv(ClockVector * rfcv) { rf_cv = rfcv; } bool synchronize_with(const ModelAction *act); bool has_synchronized_with(const ModelAction *act) const; @@ -194,7 +196,7 @@ private: * * Only valid for reads */ - const ModelAction *reads_from; + ModelAction *reads_from; int size; }; @@ -217,6 +219,7 @@ private: * vectors for all operations. */ ClockVector *cv; + ClockVector *rf_cv; /** @brief The value written (for write or RMW; undefined for read) */ uint64_t value; diff --git a/clockvector.cc b/clockvector.cc index c86995bc..2336df2f 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -18,8 +18,7 @@ */ ClockVector::ClockVector(ClockVector *parent, const ModelAction *act) { - ASSERT(act); - num_threads = int_to_id(act->get_tid()) + 1; + num_threads = act != NULL ? int_to_id(act->get_tid()) + 1 : 0; if (parent && parent->num_threads > num_threads) num_threads = parent->num_threads; @@ -27,7 +26,8 @@ ClockVector::ClockVector(ClockVector *parent, const ModelAction *act) if (parent) std::memcpy(clock, parent->clock, parent->num_threads * sizeof(modelclock_t)); - clock[id_to_int(act->get_tid())] = act->get_seq_number(); + if (act != NULL) + clock[id_to_int(act->get_tid())] = act->get_seq_number(); } /** @brief Destructor */ diff --git a/common.h b/common.h index 67ef7863..0f0ad64f 100644 --- a/common.h +++ b/common.h @@ -14,18 +14,18 @@ extern int model_out; extern int switch_alloc; #define model_print(fmt, ...) do { \ - switch_alloc = 1; \ - char mprintbuf[256]; \ - int printbuflen=snprintf_(mprintbuf, 256, fmt, ## __VA_ARGS__); \ - int lenleft = printbuflen < 256 ?printbuflen:256; \ - int totalwritten = 0;\ - while(lenleft) { \ - int byteswritten=write(model_out, &mprintbuf[totalwritten], lenleft);\ - lenleft-=byteswritten; \ - totalwritten+=byteswritten; \ - } \ - switch_alloc = 0; \ - } while (0) + switch_alloc = 1; \ + char mprintbuf[256]; \ + int printbuflen=snprintf_(mprintbuf, 256, fmt, ## __VA_ARGS__); \ + int lenleft = printbuflen < 256 ? printbuflen : 256; \ + int totalwritten = 0; \ + while(lenleft) { \ + int byteswritten=write(model_out, &mprintbuf[totalwritten], lenleft); \ + lenleft-=byteswritten; \ + totalwritten+=byteswritten; \ + } \ + switch_alloc = 0; \ +} while (0) #ifdef CONFIG_DEBUG #define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ## __VA_ARGS__); } while (0) diff --git a/execution.cc b/execution.cc index 4b765206..40b83e05 100644 --- a/execution.cc +++ b/execution.cc @@ -64,7 +64,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack thrd_last_fence_release(), node_stack(node_stack), priv(new struct model_snapshot_members ()), - mo_graph(new CycleGraph()), + mo_graph(new CycleGraph()), fuzzer(new Fuzzer()) { /* Initialize a model-checker thread, for special ModelActions */ @@ -260,13 +260,13 @@ bool ModelExecution::is_complete_execution() const * @param rf_set is the set of model actions we can possibly read from * @return True if processing this read updates the mo_graph. */ -void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) +void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { SnapVector * priorset = new SnapVector(); while(true) { int index = fuzzer->selectWrite(curr, rf_set); - const ModelAction *rf = (*rf_set)[index]; + ModelAction *rf = (*rf_set)[index]; ASSERT(rf); @@ -434,11 +434,8 @@ bool ModelExecution::process_fence(ModelAction *curr) continue; /* Establish hypothetical release sequences */ - rel_heads_list_t release_heads; - get_release_seq_heads(curr, act, &release_heads); - for (unsigned int i = 0;i < release_heads.size();i++) - synchronize(release_heads[i], curr); - if (release_heads.size() != 0) + ClockVector *cv = get_hb_from_write(act); + if (curr->get_cv()->merge(cv)) updated = true; } } @@ -536,38 +533,17 @@ bool ModelExecution::process_thread_action(ModelAction *curr) */ bool ModelExecution::initialize_curr_action(ModelAction **curr) { - ModelAction *newcurr; - if ((*curr)->is_rmwc() || (*curr)->is_rmw()) { - newcurr = process_rmw(*curr); + ModelAction *newcurr = process_rmw(*curr); delete *curr; *curr = newcurr; return false; - } - - (*curr)->set_seq_number(get_next_seq_num()); - - newcurr = node_stack->explore_action(*curr); - if (newcurr) { - /* First restore type and order in case of RMW operation */ - if ((*curr)->is_rmwr()) - newcurr->copy_typeandorder(*curr); - - ASSERT((*curr)->get_location() == newcurr->get_location()); - newcurr->copy_from_new(*curr); - - /* Discard duplicate ModelAction; use action from NodeStack */ - delete *curr; - - /* Always compute new clock vector */ - newcurr->create_cv(get_parent_action(newcurr->get_tid())); - - *curr = newcurr; - return false; /* Action was explored previously */ } else { - newcurr = *curr; + ModelAction *newcurr = *curr; + newcurr->set_seq_number(get_next_seq_num()); + node_stack->add_action(newcurr); /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); @@ -590,22 +566,18 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * @return True if this read established synchronization */ -bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf) +void ModelExecution::read_from(ModelAction *act, ModelAction *rf) { ASSERT(rf); ASSERT(rf->is_write()); act->set_read_from(rf); if (act->is_acquire()) { - rel_heads_list_t release_heads; - 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 (!synchronize(release_heads[i], act)) - num_heads--; - return num_heads > 0; + ClockVector *cv = get_hb_from_write(rf); + if (cv == NULL) + return; + act->get_cv()->merge(cv); } - return false; } /** @@ -681,7 +653,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (!second_part_of_rmw && curr->get_type() != NOOP) add_action_to_lists(curr); - SnapVector * rf_set = NULL; + SnapVector * rf_set = NULL; /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) rf_set = build_may_read_from(curr); @@ -1039,91 +1011,52 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * } /** - * Finds the head(s) of the release sequence(s) containing a given ModelAction. - * The ModelAction under consideration is expected to be taking part in - * release/acquire synchronization as an object of the "reads from" relation. - * Note that this can only provide release sequence support for RMW chains - * which do not read from the future, as those actions cannot be traced until - * their "promise" is fulfilled. Similarly, we may not even establish the - * presence of a release sequence with certainty, as some modification order - * constraints may be decided further in the future. Thus, this function - * "returns" two pieces of data: a pass-by-reference vector of @a release_heads - * and a boolean representing certainty. + * Computes the clock vector that happens before propagates from this write. * * @param rf The action that might be part of a release sequence. Must be a * write. - * @param release_heads A pass-by-reference style return parameter. After - * execution of this function, release_heads will contain the heads of all the - * relevant release sequences, if any exists with certainty - * @return true, if the ModelExecution is certain that release_heads is complete; - * false otherwise + * @return ClockVector of happens before relation. */ -bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const -{ +ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { + SnapVector * processset = NULL; for ( ;rf != NULL;rf = rf->get_reads_from()) { ASSERT(rf->is_write()); + if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL) + break; + if (processset == NULL) + processset = new SnapVector(); + processset->push_back(rf); + } - if (rf->is_release()) - release_heads->push_back(rf); - else if (rf->get_last_fence_release()) - release_heads->push_back(rf->get_last_fence_release()); - if (!rf->is_rmw()) - break;/* End of RMW chain */ - - /** @todo Need to be smarter here... In the linux lock - * example, this will run to the beginning of the program for - * every acquire. */ - /** @todo The way to be smarter here is to keep going until 1 - * thread has a release preceded by an acquire and you've seen - * both. */ - - /* acq_rel RMW is a sufficient stopping condition */ - if (rf->is_acquire() && rf->is_release()) - return true;/* complete */ - }; - ASSERT(rf); // Needs to be real write - - if (rf->is_release()) - return true;/* complete */ - - /* else relaxed write - * - check for fence-release in the same thread (29.8, stmt. 3) - * - check modification order for contiguous subsequence - * -> rf must be same thread as release */ - - const ModelAction *fence_release = rf->get_last_fence_release(); - /* Synchronize with a fence-release unconditionally; we don't need to - * find any more "contiguous subsequence..." for it */ - if (fence_release) - release_heads->push_back(fence_release); - - return true; /* complete */ -} - -/** - * An interface for getting the release sequence head(s) with which a - * given ModelAction must synchronize. This function only returns a non-empty - * result when it can locate a release sequence head with certainty. Otherwise, - * it may mark the internal state of the ModelExecution so that it will handle - * the release sequence at a later time, causing @a acquire to update its - * synchronization at some later point in execution. - * - * @param acquire The 'acquire' action that may synchronize with a release - * sequence - * @param read The read action that may read from a release sequence; this may - * be the same as acquire, or else an earlier action in the same thread (i.e., - * when 'acquire' is a fence-acquire) - * @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 ModelExecution::release_seq_heads - */ -void ModelExecution::get_release_seq_heads(ModelAction *acquire, - ModelAction *read, rel_heads_list_t *release_heads) -{ - const ModelAction *rf = read->get_reads_from(); - - release_seq_heads(rf, release_heads); + int i = (processset == NULL) ? 1 : processset->size(); + + ClockVector * vec = NULL; + for(;i > 0 ;i--) { + if (rf->get_rfcv() != NULL) { + vec = rf->get_rfcv(); + } else if (rf->is_acquire() && rf->is_release()) { + vec = rf->get_cv(); + } else if (rf->is_release() && !rf->is_rmw()) { + vec = rf->get_cv(); + } else if (rf->is_release()) { + //have rmw that is release and doesn't have a rfcv + (vec = new ClockVector(vec, NULL))->merge(rf->get_cv()); + rf->set_rfcv(vec); + } else { + //operation that isn't release + if (rf->get_last_fence_release()) { + if (vec == NULL) + vec = rf->get_last_fence_release()->get_cv(); + else + (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv()); + } + rf->set_rfcv(vec); + } + } + if (processset != NULL) + delete processset; + return vec; } /** @@ -1327,7 +1260,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) { * @param curr is the current ModelAction that we are exploring; it must be a * 'read' operation. */ -SnapVector * ModelExecution::build_may_read_from(ModelAction *curr) +SnapVector * ModelExecution::build_may_read_from(ModelAction *curr) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -1338,7 +1271,7 @@ SnapVector * ModelExecution::build_may_read_from(ModelActi if (curr->is_seqcst()) last_sc_write = get_last_seq_cst_write(curr); - SnapVector * rf_set = new SnapVector(); + SnapVector * rf_set = new SnapVector(); /* Iterate over all threads */ for (i = 0;i < thrd_lists->size();i++) { @@ -1346,12 +1279,12 @@ SnapVector * ModelExecution::build_may_read_from(ModelActi action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; for (rit = list->rbegin();rit != list->rend();rit++) { - const ModelAction *act = *rit; + ModelAction *act = *rit; /* Only consider 'write' actions */ if (!act->is_write()) { if (act != curr && act->is_read() && act->happens_before(curr)) { - const ModelAction *tmp = act->get_reads_from(); + ModelAction *tmp = act->get_reads_from(); if (((unsigned int) id_to_int(tmp->get_tid()))==i) act = tmp; else diff --git a/execution.h b/execution.h index fa2b78b8..c87a20fe 100644 --- a/execution.h +++ b/execution.h @@ -19,8 +19,6 @@ #include #include "classlist.h" -/** @brief Shorthand for a list of release sequence heads */ -typedef ModelVector rel_heads_list_t; typedef SnapList action_list_t; struct PendingFutureValue { @@ -31,29 +29,10 @@ struct PendingFutureValue { ModelAction *reader; }; -/** @brief Records information regarding a single pending release sequence */ -struct release_seq { - /** @brief The acquire operation */ - ModelAction *acquire; - /** @brief The read operation that may read from a release sequence; - * may be the same as acquire, or else an earlier action in the same - * thread (i.e., when 'acquire' is a fence-acquire) */ - const ModelAction *read; - /** @brief The head of the RMW chain from which 'read' reads; may be - * equal to 'release' */ - const ModelAction *rf; - /** @brief The head of the potential longest release sequence chain */ - const ModelAction *release; - /** @brief The write(s) that may break the release sequence */ - SnapVector writes; -}; - /** @brief The central structure for model-checking */ class ModelExecution { public: - ModelExecution(ModelChecker *m, - Scheduler *scheduler, - NodeStack *node_stack); + ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack); ~ModelExecution(); struct model_params * get_params() const { return params; } @@ -126,13 +105,13 @@ private: bool next_execution(); bool initialize_curr_action(ModelAction **curr); - void process_read(ModelAction *curr, SnapVector * rf_set); + void process_read(ModelAction *curr, SnapVector * rf_set); void process_write(ModelAction *curr); bool process_fence(ModelAction *curr); bool process_mutex(ModelAction *curr); bool process_thread_action(ModelAction *curr); - bool read_from(ModelAction *act, const ModelAction *rf); + void read_from(ModelAction *act, ModelAction *rf); bool synchronize(const ModelAction *first, ModelAction *second); void add_action_to_lists(ModelAction *act); @@ -140,13 +119,12 @@ private: ModelAction * get_last_seq_cst_write(ModelAction *curr) const; ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const; ModelAction * get_last_unlock(ModelAction *curr) const; - SnapVector * build_may_read_from(ModelAction *curr); + SnapVector * build_may_read_from(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector *priorset, bool *canprune); void w_modification_order(ModelAction *curr); - void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads); - bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const; + ClockVector * get_hb_from_write(ModelAction *rf) const; ModelAction * get_uninitialized_action(const ModelAction *curr) const; action_list_t action_trace; diff --git a/fuzzer.cc b/fuzzer.cc index 3a3f9883..9ad61c3c 100644 --- a/fuzzer.cc +++ b/fuzzer.cc @@ -3,7 +3,7 @@ #include "threads-model.h" #include "model.h" -int Fuzzer::selectWrite(ModelAction *read, SnapVector * rf_set) { +int Fuzzer::selectWrite(ModelAction *read, SnapVector * rf_set) { int random_index = random() % rf_set->size(); return random_index; } diff --git a/fuzzer.h b/fuzzer.h index 691477bd..6cf1efba 100644 --- a/fuzzer.h +++ b/fuzzer.h @@ -7,7 +7,7 @@ class Fuzzer { public: Fuzzer() {} - int selectWrite(ModelAction *read, SnapVector* rf_set); + int selectWrite(ModelAction *read, SnapVector* rf_set); Thread * selectThread(Node *n, int * threadlist, int numthreads); Thread * selectNotify(action_list_t * waiters); MEMALLOC diff --git a/include/impatomic.h b/include/impatomic.h index 02239d5f..7f4dcd4c 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -82,12 +82,12 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile #define _ATOMIC_LOAD_( __a__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__((__a__)->__f__)__r__ = (__typeof__((__a__)->__f__))model_read_action((void *)__p__, __x__); \ + __typeof__((__a__)->__f__) __r__ = (__typeof__((__a__)->__f__))model_read_action((void *)__p__, __x__); \ __r__; }) #define _ATOMIC_STORE_( __a__, __m__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__(__m__)__v__ = (__m__); \ + __typeof__(__m__) __v__ = (__m__); \ model_write_action((void *) __p__, __x__, (uint64_t) __v__); \ __v__ = __v__; /* Silence clang (-Wunused-value) */ \ }) @@ -95,16 +95,16 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile #define _ATOMIC_INIT_( __a__, __m__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__(__m__)__v__ = (__m__); \ + __typeof__(__m__) __v__ = (__m__); \ model_init_action((void *) __p__, (uint64_t) __v__); \ __v__ = __v__; /* Silence clang (-Wunused-value) */ \ }) #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); \ - __typeof__(__m__)__v__ = (__m__); \ - __typeof__((__a__)->__f__)__copy__= __old__; \ + __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); \ + __typeof__(__m__) __v__ = (__m__); \ + __typeof__((__a__)->__f__) __copy__= __old__; \ __copy__ __o__ __v__; \ model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); \ __old__ = __old__; /* Silence clang (-Wunused-value) */ \ @@ -115,10 +115,10 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__(__e__)__q__ = (__e__); \ - __typeof__(__m__)__v__ = (__m__); \ + __typeof__(__e__) __q__ = (__e__); \ + __typeof__(__m__) __v__ = (__m__); \ bool __r__; \ - __typeof__((__a__)->__f__)__t__=(__typeof__((__a__)->__f__))model_rmwrcas_action((void *)__p__, __x__, (uint64_t) *__q__, sizeof((__a__)->__f__)); \ + __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__))model_rmwrcas_action((void *)__p__, __x__, (uint64_t) *__q__, sizeof((__a__)->__f__)); \ if (__t__ == *__q__ ) {; \ model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \ else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \ @@ -2418,8 +2418,8 @@ inline void* atomic_fetch_add_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) { volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); - __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); - __typeof__((__a__)->__f__)__copy__= __old__; + __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); + __typeof__((__a__)->__f__) __copy__= __old__; __copy__ = (void *) (((char *)__copy__) + __m__); model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); return __old__; @@ -2434,8 +2434,8 @@ inline void* atomic_fetch_sub_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) { volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); - __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); - __typeof__((__a__)->__f__)__copy__= __old__; + __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); + __typeof__((__a__)->__f__) __copy__= __old__; __copy__ = (void *) (((char *)__copy__) - __m__); model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); return __old__; diff --git a/include/wildcard.h b/include/wildcard.h index 0eaffd5e..6bcd6acd 100644 --- a/include/wildcard.h +++ b/include/wildcard.h @@ -21,11 +21,11 @@ #define is_normal_mo(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == memory_order_normal) #define assert_infer(x) for (int i = 0;i <= wildcardNum;i++) \ - ASSERT(is_normal_mo_infer((x[i]))); + ASSERT(is_normal_mo_infer((x[i]))); #define assert_infers(x) for (ModelList::iterator iter = \ (x)->begin();iter != (x)->end();iter++) \ - assert_infer((*iter)); + assert_infer((*iter)); #define relaxed memory_order_relaxed #define release memory_order_release diff --git a/model.cc b/model.cc index b8d9f7cb..1be15edb 100644 --- a/model.cc +++ b/model.cc @@ -162,7 +162,7 @@ void ModelChecker::print_bugs() const bugs->size(), bugs->size() > 1 ? "s" : ""); for (unsigned int i = 0;i < bugs->size();i++) - (*bugs)[i] -> print(); + (*bugs)[i]->print(); } /** @@ -173,15 +173,15 @@ void ModelChecker::print_bugs() const */ void ModelChecker::record_stats() { - stats.num_total ++; + stats.num_total++; if (!execution->isfeasibleprefix()) - stats.num_infeasible ++; + stats.num_infeasible++; else if (execution->have_bug_reports()) - stats.num_buggy_executions ++; + stats.num_buggy_executions++; else if (execution->is_complete_execution()) - stats.num_complete ++; + stats.num_complete++; else { - stats.num_redundant ++; + stats.num_redundant++; /** * @todo We can violate this ASSERT() when fairness/sleep sets @@ -262,15 +262,15 @@ bool ModelChecker::next_execution() return true; } // test code - execution_number ++; + execution_number++; reset_to_initial_state(); return false; } /** @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(execution->get_action_trace()); + for (unsigned int i = 0;i < trace_analyses.size();i++) + trace_analyses[i]->analyze(execution->get_action_trace()); } /** diff --git a/nodestack.cc b/nodestack.cc index c1c3cfc5..258c2758 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -86,13 +86,12 @@ void NodeStack::print() const /** Note: The is_enabled set contains what actions were enabled when * act was chosen. */ -ModelAction * NodeStack::explore_action(ModelAction *act) +void NodeStack::add_action(ModelAction *act) { DBG(); node_list.push_back(new Node(act)); head_idx++; - return NULL; } diff --git a/nodestack.h b/nodestack.h index 09a79e40..4efd6029 100644 --- a/nodestack.h +++ b/nodestack.h @@ -56,7 +56,7 @@ public: ~NodeStack(); void register_engine(const ModelExecution *exec); - ModelAction * explore_action(ModelAction *act); + void add_action(ModelAction *act); Node * get_head() const; Node * get_next() const; void reset_execution(); diff --git a/printf.c b/printf.c index 8a700add..b935e7b9 100644 --- a/printf.c +++ b/printf.c @@ -144,6 +144,9 @@ static inline void _out_null(char character, void* buffer, size_t idx, size_t ma (void)character; (void)buffer; (void)idx; (void)maxlen; } +// placeholder so we can compile +void _putchar(char c) { +} // internal _putchar wrapper static inline void _out_char(char character, void* buffer, size_t idx, size_t maxlen) diff --git a/printf.h b/printf.h index f779cd24..3d79ef3f 100644 --- a/printf.h +++ b/printf.h @@ -10,10 +10,10 @@ // to use, copy, modify, merge, publish, distribute, sublicense, and/or sell // copies of the Software, and to permit persons to whom the Software is // furnished to do so, subject to the following conditions: -// +// // The above copyright notice and this permission notice shall be included in // all copies or substantial portions of the Software. -// +// // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -109,4 +109,4 @@ int fctprintf(void (*out)(char character, void* arg), void* arg, const char* for #endif -#endif // _PRINTF_H_ +#endif // _PRINTF_H_ -- 2.34.1