memoize hb in writes
authorbdemsky <bdemsky@uci.edu>
Tue, 2 Jul 2019 06:02:15 +0000 (23:02 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 2 Jul 2019 06:09:52 +0000 (23:09 -0700)
15 files changed:
action.cc
action.h
clockvector.cc
common.h
execution.cc
execution.h
fuzzer.cc
fuzzer.h
include/impatomic.h
include/wildcard.h
model.cc
nodestack.cc
nodestack.h
printf.c
printf.h

index 3059e0d94be8a90c5db19ce0114cc44062f9c6aa..8dcc9d5124c6b064d7b2e0ad888d5aaa39a4e508 100644 (file)
--- 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"
index c7703094d99ffe12213ec59a44b8c9ef0fdcc7a3..5e8b1b1c7691c75e212bdbaa0daed6b00723b32e 100644 (file)
--- 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;
index c86995bc9bbb555cf9e2381d1b7df91036330a46..2336df2f4720f6bea613891859591ddf47488fc3 100644 (file)
@@ -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 */
index 67ef78634923118c9055961b5fc73c32470ce57b..0f0ad64f9e317b634c38eba45496e60672bfbc64 100644 (file)
--- 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)
index 4b76520660e2f0fedc67d72c8f9f262bbed843fc..40b83e05f9b7c2c6eecdaa7686a6846dceaedd40 100644 (file)
@@ -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<const ModelAction *> * rf_set)
+void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        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<const ModelAction *> * rf_set = NULL;
+       SnapVector<ModelAction *> * 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<const ModelAction *> * 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<const ModelAction *>();
+               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<const ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
+SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@ -1338,7 +1271,7 @@ SnapVector<const ModelAction *> *  ModelExecution::build_may_read_from(ModelActi
        if (curr->is_seqcst())
                last_sc_write = get_last_seq_cst_write(curr);
 
-       SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
+       SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
 
        /* Iterate over all threads */
        for (i = 0;i < thrd_lists->size();i++) {
@@ -1346,12 +1279,12 @@ SnapVector<const ModelAction *> *  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
index fa2b78b8a282fda6234f3090a00bda968104cc54..c87a20fe2eb930c04310b9c9efa67cd0f2c3d0c4 100644 (file)
@@ -19,8 +19,6 @@
 #include <condition_variable>
 #include "classlist.h"
 
-/** @brief Shorthand for a list of release sequence heads */
-typedef ModelVector<const ModelAction *> rel_heads_list_t;
 typedef SnapList<ModelAction *> 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<const ModelAction *> 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<const ModelAction *> * rf_set);
+       void process_read(ModelAction *curr, SnapVector<ModelAction *> * 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<const ModelAction *> * build_may_read_from(ModelAction *curr);
+       SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
 
        bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *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;
index 3a3f98831b1c64245a5ab85569667e604878b361..9ad61c3c5cddbc96073e85c15e8dd05f46bffadb 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -3,7 +3,7 @@
 #include "threads-model.h"
 #include "model.h"
 
-int Fuzzer::selectWrite(ModelAction *read, SnapVector<const ModelAction *> * rf_set) {
+int Fuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set) {
        int random_index = random() % rf_set->size();
        return random_index;
 }
index 691477bd6e2e3db8833add08de8c3d5f619bd94d..6cf1efbad26352782e4a45b985654e8f52069a1b 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -7,7 +7,7 @@
 class Fuzzer {
 public:
        Fuzzer() {}
-       int selectWrite(ModelAction *read, SnapVector<const ModelAction *>* rf_set);
+       int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        Thread * selectThread(Node *n, int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
        MEMALLOC
index 02239d5f9f1b5afb5e66313d3c11c607443fef3b..7f4dcd4cb5ffeb8801f5f68804fb847cd9801a92 100644 (file)
@@ -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__;
index 0eaffd5eafc66753546035d59c628df44db40d6f..6bcd6acd349795839af21bea4212b1ba973a6294 100644 (file)
 #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<memory_order *>::iterator iter = \
                                                                                                                                (x)->begin();iter != (x)->end();iter++) \
-               assert_infer((*iter));
+       assert_infer((*iter));
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
index b8d9f7cb4ce46b7c01ed7aa08fe982985a7a9cd0..1be15edbf2a1a63c4912684c367a338cb1f1da39 100644 (file)
--- 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());
 }
 
 /**
index c1c3cfc502a7cca8b53f984d0584e7e9750cc609..258c27581b600e0433464ab1af321bbe22e71310 100644 (file)
@@ -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;
 }
 
 
index 09a79e4057d882431b9e662373c2b3a19bfff5fb..4efd60292e24175f0aa3cfc7544a5eeab4904328 100644 (file)
@@ -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();
index 8a700add4c85e36e2c9ff01fd1f1a7c3acb28e22..b935e7b9d64fd167df18b7e15c3d3c76145be231 100644 (file)
--- 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;\r
 }\r
 \r
+// placeholder so we can compile\r
+void _putchar(char c) {\r
+}\r
 \r
 // internal _putchar wrapper\r
 static inline void _out_char(char character, void* buffer, size_t idx, size_t maxlen)\r
index f779cd24612cb4432c98731ee0cb70b8ef554826..3d79ef3f1708afefc6a2bb371b562031b2c88ad1 100644 (file)
--- a/printf.h
+++ b/printf.h
 // to use, copy, modify, merge, publish, distribute, sublicense, and/or sell\r
 // copies of the Software, and to permit persons to whom the Software is\r
 // furnished to do so, subject to the following conditions:\r
-// \r
+//\r
 // The above copyright notice and this permission notice shall be included in\r
 // all copies or substantial portions of the Software.\r
-// \r
+//\r
 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\r
 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,\r
 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE\r
@@ -109,4 +109,4 @@ int fctprintf(void (*out)(char character, void* arg), void* arg, const char* for
 #endif\r
 \r
 \r
-#endif  // _PRINTF_H_\r
+#endif // _PRINTF_H_\r