fix tabbing

diff --git a/action.cc b/action.cc
index 8c29c533ac6e66fb9e924590f64d49c4ad4635c5..bbbeceea28cf7c683dced7d95111b624e00576ce 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -32,7 +32,7 @@
  * (default), then a Thread is assigned according to the scheduler.
  */
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
  * (default), then a Thread is assigned according to the scheduler.
  */
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,

-               uint64_t value, Thread *thread) :
+                                                                                                uint64_t value, Thread *thread) :

        type(type),
        order(order),
        original_order(order),
        type(type),
        order(order),
        original_order(order),


@@ -65,7 +65,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
  * (default), then a Thread is assigned according to the scheduler.
  */
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
  * (default), then a Thread is assigned according to the scheduler.
  */
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,

-               uint64_t value, int size) :
+                                                                                                uint64_t value, int size) :

        type(type),
        order(order),
        original_order(order),
        type(type),
        order(order),
        original_order(order),


@@ -95,12 +95,12 @@ ModelAction::~ModelAction()
         */
 
        /*
         */
 
        /*

-        if (cv)
-               delete cv; */
+          if (cv)
+               delete cv; */

 }
 
 int ModelAction::getSize() const {
 }
 
 int ModelAction::getSize() const {

-  return size;
+       return size;

 }
 
 void ModelAction::copy_from_new(ModelAction *newaction)
 }
 
 void ModelAction::copy_from_new(ModelAction *newaction)


@@ -465,7 +465,7 @@ uint64_t ModelAction::get_reads_from_value() const
        ASSERT(is_read());
        if (reads_from)
                return reads_from->get_write_value();
        ASSERT(is_read());
        if (reads_from)
                return reads_from->get_write_value();

-       return VALUE_NONE; /* Only for new actions with no reads-from */
+       return VALUE_NONE;                      /* Only for new actions with no reads-from */

 }
 
 /**
 }
 
 /**


@@ -523,7 +523,7 @@ void ModelAction::set_read_from(const ModelAction *act)
 
        reads_from = act;
 
 
        reads_from = act;
 

-       if (act->is_uninitialized()) { // WL
+       if (act->is_uninitialized()) {                  // WL

                uint64_t val = *((uint64_t *) location);
                ModelAction * act_initialized = (ModelAction *)act;
                act_initialized->set_value(val);
                uint64_t val = *((uint64_t *) location);
                ModelAction * act_initialized = (ModelAction *)act;
                act_initialized->set_value(val);


@@ -531,10 +531,10 @@ void ModelAction::set_read_from(const ModelAction *act)
 
 // disabled by WL, because LLVM IR is unable to detect atomic init
 /*             model->assert_bug("May read from uninitialized atomic:\n"
 
 // disabled by WL, because LLVM IR is unable to detect atomic init
 /*             model->assert_bug("May read from uninitialized atomic:\n"

-                               "    action %d, thread %d, location %p (%s, %s)",
-                               seq_number, id_to_int(tid), location,
-                               get_type_str(), get_mo_str());
-*/
+                                "    action %d, thread %d, location %p (%s, %s)",
+                                seq_number, id_to_int(tid), location,
+                                get_type_str(), get_mo_str());
+ */

        }
 }
 
        }
 }
 


@@ -571,44 +571,44 @@ bool ModelAction::happens_before(const ModelAction *act) const
 const char * ModelAction::get_type_str() const
 {
        switch (this->type) {
 const char * ModelAction::get_type_str() const
 {
        switch (this->type) {

-               case THREAD_CREATE: return "thread create";
-               case THREAD_START: return "thread start";
-               case THREAD_YIELD: return "thread yield";
-               case THREAD_JOIN: return "thread join";
-               case THREAD_FINISH: return "thread finish";
-
-               case PTHREAD_CREATE: return "pthread create";
-               case PTHREAD_JOIN: return "pthread join";
-
-               case ATOMIC_UNINIT: return "uninitialized";
-               case ATOMIC_READ: return "atomic read";
-               case ATOMIC_WRITE: return "atomic write";
-               case ATOMIC_RMW: return "atomic rmw";
-               case ATOMIC_FENCE: return "fence";
-               case ATOMIC_RMWR: return "atomic rmwr";
-               case ATOMIC_RMWRCAS: return "atomic rmwrcas";
-               case ATOMIC_RMWC: return "atomic rmwc";
-               case ATOMIC_INIT: return "init atomic";
-               case ATOMIC_LOCK: return "lock";
-               case ATOMIC_UNLOCK: return "unlock";
-               case ATOMIC_TRYLOCK: return "trylock";
-               case ATOMIC_WAIT: return "wait";
-               case ATOMIC_NOTIFY_ONE: return "notify one";
-               case ATOMIC_NOTIFY_ALL: return "notify all";
-               case ATOMIC_ANNOTATION: return "annotation";
-               default: return "unknown type";
+       case THREAD_CREATE: return "thread create";
+       case THREAD_START: return "thread start";
+       case THREAD_YIELD: return "thread yield";
+       case THREAD_JOIN: return "thread join";
+       case THREAD_FINISH: return "thread finish";
+
+       case PTHREAD_CREATE: return "pthread create";
+       case PTHREAD_JOIN: return "pthread join";
+
+       case ATOMIC_UNINIT: return "uninitialized";
+       case ATOMIC_READ: return "atomic read";
+       case ATOMIC_WRITE: return "atomic write";
+       case ATOMIC_RMW: return "atomic rmw";
+       case ATOMIC_FENCE: return "fence";
+       case ATOMIC_RMWR: return "atomic rmwr";
+       case ATOMIC_RMWRCAS: return "atomic rmwrcas";
+       case ATOMIC_RMWC: return "atomic rmwc";
+       case ATOMIC_INIT: return "init atomic";
+       case ATOMIC_LOCK: return "lock";
+       case ATOMIC_UNLOCK: return "unlock";
+       case ATOMIC_TRYLOCK: return "trylock";
+       case ATOMIC_WAIT: return "wait";
+       case ATOMIC_NOTIFY_ONE: return "notify one";
+       case ATOMIC_NOTIFY_ALL: return "notify all";
+       case ATOMIC_ANNOTATION: return "annotation";
+       default: return "unknown type";

        };
 }
 
 const char * ModelAction::get_mo_str() const
 {
        switch (this->order) {
        };
 }
 
 const char * ModelAction::get_mo_str() const
 {
        switch (this->order) {

-               case std::memory_order_relaxed: return "relaxed";
-               case std::memory_order_acquire: return "acquire";
-               case std::memory_order_release: return "release";
-               case std::memory_order_acq_rel: return "acq_rel";
-               case std::memory_order_seq_cst: return "seq_cst";
-               default: return "unknown";
+       case std::memory_order_relaxed: return "relaxed";
+       case std::memory_order_acquire: return "acquire";
+       case std::memory_order_release: return "release";
+       case std::memory_order_acq_rel: return "acq_rel";
+       case std::memory_order_seq_cst: return "seq_cst";
+       default: return "unknown";

        }
 }
 
        }
 }
 


@@ -618,7 +618,7 @@ void ModelAction::print() const
        const char *type_str = get_type_str(), *mo_str = get_mo_str();
 
        model_print("%-4d %-2d   %-14s  %7s  %14p   %-#18" PRIx64,
        const char *type_str = get_type_str(), *mo_str = get_mo_str();
 
        model_print("%-4d %-2d   %-14s  %7s  %14p   %-#18" PRIx64,

-                       seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());
+                                                       seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());

        if (is_read()) {
                if (reads_from)
                        model_print("  %-3d", reads_from->get_seq_number());
        if (is_read()) {
                if (reads_from)
                        model_print("  %-3d", reads_from->get_seq_number());


@@ -644,9 +644,9 @@ unsigned int ModelAction::hash() const
        hash ^= id_to_int(tid) << 6;
 
        if (is_read()) {
        hash ^= id_to_int(tid) << 6;
 
        if (is_read()) {

-              if (reads_from)
-                      hash ^= reads_from->get_seq_number();
-              hash ^= get_reads_from_value();
+               if (reads_from)
+                       hash ^= reads_from->get_seq_number();
+               hash ^= get_reads_from_value();

        }
        return hash;
 }
        }
        return hash;
 }

diff --git a/action.h b/action.h
index 760e9fb0409143764260103566316525e06ac79c..662d7d7b4c610ee31f2358f8a2e5ea6f15562bce 100644 (file)
--- a/action.h
+++ b/action.h
@@ -15,7 +15,7 @@
 #include "classlist.h"
 
 namespace cdsc {
 #include "classlist.h"
 
 namespace cdsc {

-       class mutex;
+class mutex;

 }
 
 using std::memory_order;
 }
 
 using std::memory_order;


@@ -47,32 +47,32 @@ using std::memory_order_seq_cst;
 /** @brief Represents an action type, identifying one of several types of
  * ModelAction */
 typedef enum action_type {
 /** @brief Represents an action type, identifying one of several types of
  * ModelAction */
 typedef enum action_type {

-       THREAD_CREATE,        /**< A thread creation action */
-       THREAD_START,         /**< First action in each thread */
-       THREAD_YIELD,         /**< A thread yield action */
-       THREAD_JOIN,          /**< A thread join action */
-       THREAD_FINISH,        /**< A thread completion action */
-       PTHREAD_CREATE,       /**< A pthread creation action */
-       PTHREAD_JOIN,         /**< A pthread join action */
-       
-       ATOMIC_UNINIT,        /**< Represents an uninitialized atomic */
-       ATOMIC_READ,          /**< An atomic read action */
-       ATOMIC_WRITE,         /**< An atomic write action */
-       ATOMIC_RMWR,          /**< The read part of an atomic RMW action */
-       ATOMIC_RMWRCAS,          /**< The read part of an atomic RMW action */
-       ATOMIC_RMW,           /**< The write part of an atomic RMW action */
-       ATOMIC_RMWC,          /**< Convert an atomic RMW action into a READ */
-       ATOMIC_INIT,          /**< Initialization of an atomic object (e.g.,
-                              *   atomic_init()) */
-       ATOMIC_FENCE,         /**< A fence action */
-       ATOMIC_LOCK,          /**< A lock action */
-       ATOMIC_TRYLOCK,       /**< A trylock action */
-       ATOMIC_UNLOCK,        /**< An unlock action */
-       ATOMIC_NOTIFY_ONE,    /**< A notify_one action */
-       ATOMIC_NOTIFY_ALL,    /**< A notify all action */
-       ATOMIC_WAIT,          /**< A wait action */
-       ATOMIC_ANNOTATION,     /**< An annotation action to pass information
-                                                                                                        to a trace analysis */
+       THREAD_CREATE,                                                  /**< A thread creation action */
+       THREAD_START,                                                           /**< First action in each thread */
+       THREAD_YIELD,                                                           /**< A thread yield action */
+       THREAD_JOIN,                                                            /**< A thread join action */
+       THREAD_FINISH,                                                  /**< A thread completion action */
+       PTHREAD_CREATE,                                                 /**< A pthread creation action */
+       PTHREAD_JOIN,                                                           /**< A pthread join action */
+
+       ATOMIC_UNINIT,                                                  /**< Represents an uninitialized atomic */
+       ATOMIC_READ,                                                            /**< An atomic read action */
+       ATOMIC_WRITE,                                                           /**< An atomic write action */
+       ATOMIC_RMWR,                                                            /**< The read part of an atomic RMW action */
+       ATOMIC_RMWRCAS,                                                         /**< The read part of an atomic RMW action */
+       ATOMIC_RMW,                                                                     /**< The write part of an atomic RMW action */
+       ATOMIC_RMWC,                                                            /**< Convert an atomic RMW action into a READ */
+       ATOMIC_INIT,                                                            /**< Initialization of an atomic object (e.g.,
+                                                                                                                        *   atomic_init()) */
+       ATOMIC_FENCE,                                                           /**< A fence action */
+       ATOMIC_LOCK,                                                            /**< A lock action */
+       ATOMIC_TRYLOCK,                                                 /**< A trylock action */
+       ATOMIC_UNLOCK,                                                  /**< An unlock action */
+       ATOMIC_NOTIFY_ONE,                                      /**< A notify_one action */
+       ATOMIC_NOTIFY_ALL,                                      /**< A notify all action */
+       ATOMIC_WAIT,                                                            /**< A wait action */
+       ATOMIC_ANNOTATION,                                      /**< An annotation action to pass information
+                                                                                                                                                                                                 to a trace analysis */

        NOOP
 } action_type_t;
 
        NOOP
 } action_type_t;
 


@@ -88,7 +88,7 @@ typedef enum action_type {
 class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
 class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);

-       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size);
+       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size);

        ~ModelAction();
        void print() const;
 
        ~ModelAction();
        void print() const;
 


@@ -138,7 +138,7 @@ public:
        bool is_yield() const;
        bool could_be_write() const;
        bool is_rmwr() const;
        bool is_yield() const;
        bool could_be_write() const;
        bool is_rmwr() const;

-       bool is_rmwrcas() const;
+       bool is_rmwrcas() const;

        bool is_rmwc() const;
        bool is_rmw() const;
        bool is_fence() const;
        bool is_rmwc() const;
        bool is_rmw() const;
        bool is_fence() const;


@@ -152,8 +152,8 @@ public:
        bool same_thread(const ModelAction *act) const;
        bool is_conflicting_lock(const ModelAction *act) const;
        bool could_synchronize_with(const ModelAction *act) const;
        bool same_thread(const ModelAction *act) const;
        bool is_conflicting_lock(const ModelAction *act) const;
        bool could_synchronize_with(const ModelAction *act) const;

-  int getSize() const;
-  
+       int getSize() const;
+

        Thread * get_thread_operand() const;
 
        void create_cv(const ModelAction *parent = NULL);
        Thread * get_thread_operand() const;
 
        void create_cv(const ModelAction *parent = NULL);


@@ -183,7 +183,7 @@ public:
 
        /* to accomodate pthread create and join */
        Thread * thread_operand;
 
        /* to accomodate pthread create and join */
        Thread * thread_operand;

-       void set_thread_operand(Thread *th) { thread_operand = th; } 
+       void set_thread_operand(Thread *th) { thread_operand = th; }

 private:
 
        const char * get_type_str() const;
 private:
 
        const char * get_type_str() const;


@@ -207,15 +207,15 @@ private:
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
 

-  union {
-  /**
-        * @brief The store that this action reads from
-        *
-        * Only valid for reads
-        */
-       const ModelAction *reads_from;
-    int size;
-  };
+       union {
+               /**
+                * @brief The store that this action reads from
+                *
+                * Only valid for reads
+                */
+               const ModelAction *reads_from;
+               int size;
+       };

        /** @brief The last fence release from the same thread */
        const ModelAction *last_fence_release;
 
        /** @brief The last fence release from the same thread */
        const ModelAction *last_fence_release;
 


@@ -245,4 +245,4 @@ private:
        ClockVector *cv;
 };
 
        ClockVector *cv;
 };
 

-#endif /* __ACTION_H__ */
+#endif/* __ACTION_H__ */

diff --git a/bugmessage.h b/bugmessage.h
index bd7d0b68e891eb57004fb4d59a9d344505c33cd8..bab57381c05c227b8df98abea809dff952985bf3 100644 (file)
--- a/bugmessage.h
+++ b/bugmessage.h
@@ -10,7 +10,7 @@ struct bug_message {
                msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
                sprintf(msg, fmt, str);
        }
                msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
                sprintf(msg, fmt, str);
        }

-       ~bug_message() { if (msg) snapshot_free(msg); }
+       ~bug_message() { if (msg) snapshot_free(msg);}

 
        char *msg;
        void print() { model_print("%s", msg); }
 
        char *msg;
        void print() { model_print("%s", msg); }


@@ -18,4 +18,4 @@ struct bug_message {
        SNAPSHOTALLOC
 };
 
        SNAPSHOTALLOC
 };
 

-#endif /* __BUGMESSAGE_H__ */
+#endif/* __BUGMESSAGE_H__ */

diff --git a/clockvector.cc b/clockvector.cc
index 467a27e94372de3a00e356f3b5985298e89ff323..54e8c4a1a9b5188eb0b56875015f13950712eabd 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -47,18 +47,18 @@ bool ClockVector::merge(const ClockVector *cv)
        bool changed = false;
        if (cv->num_threads > num_threads) {
                clock = (modelclock_t *)snapshot_realloc(clock, cv->num_threads * sizeof(modelclock_t));
        bool changed = false;
        if (cv->num_threads > num_threads) {
                clock = (modelclock_t *)snapshot_realloc(clock, cv->num_threads * sizeof(modelclock_t));

-               for (int i = num_threads; i < cv->num_threads; i++)
+               for (int i = num_threads;i < cv->num_threads;i++)

                        clock[i] = 0;
                num_threads = cv->num_threads;
        }
 
        /* Element-wise maximum */
                        clock[i] = 0;
                num_threads = cv->num_threads;
        }
 
        /* Element-wise maximum */

-       for (int i = 0; i < cv->num_threads; i++)
+       for (int i = 0;i < cv->num_threads;i++)

                if (cv->clock[i] > clock[i]) {
                        clock[i] = cv->clock[i];
                        changed = true;
                }
                if (cv->clock[i] > clock[i]) {
                        clock[i] = cv->clock[i];
                        changed = true;
                }

-       
+

        return changed;
 }
 
        return changed;
 }
 


@@ -98,6 +98,6 @@ void ClockVector::print() const
 {
        int i;
        model_print("(");
 {
        int i;
        model_print("(");

-       for (i = 0; i < num_threads; i++)
+       for (i = 0;i < num_threads;i++)

                model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
 }
                model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
 }

diff --git a/clockvector.h b/clockvector.h
index 0e5ba8656c605b5de48108eebf5fd17cee35a7f0..b9987b22a6f310a70fda2d39ede5fe84ccc62906 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -28,4 +28,4 @@ private:
        int num_threads;
 };
 
        int num_threads;
 };
 

-#endif /* __CLOCKVECTOR_H__ */
+#endif/* __CLOCKVECTOR_H__ */

diff --git a/cmodelint.cc b/cmodelint.cc
index fc80b299f0e590312b62a919926e41c30310e8db..cdd8b442616be68ce17d882f97987cd3b959e3d3 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -39,7 +39,7 @@ uint64_t model_rmwr_action(void *obj, memory_order ord) {
  * of the RMW action w/o a write.
  */
 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {
  * of the RMW action w/o a write.
  */
 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {

-  return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
+       return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));

 }
 
 /** Performs the write part of a RMW action. */
 }
 
 /** Performs the write part of a RMW action. */


@@ -75,7 +75,7 @@ void model_fence_action_helper(int atomic_index) {
 }
 
 // cds atomic loads
 }
 
 // cds atomic loads

-uint8_t cds_atomic_load8(void * obj, int atomic_index) {       
+uint8_t cds_atomic_load8(void * obj, int atomic_index) {

        return (uint8_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) );
 }
 uint16_t cds_atomic_load16(void * obj, int atomic_index) {
        return (uint8_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) );
 }
 uint16_t cds_atomic_load16(void * obj, int atomic_index) {


@@ -90,155 +90,155 @@ uint64_t cds_atomic_load64(void * obj, int atomic_index) {
 
 // cds atomic stores
 void cds_atomic_store8(void * obj, int atomic_index, uint8_t val) {
 
 // cds atomic stores
 void cds_atomic_store8(void * obj, int atomic_index, uint8_t val) {

-  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));

 }
 void cds_atomic_store16(void * obj, int atomic_index, uint16_t val) {
 }
 void cds_atomic_store16(void * obj, int atomic_index, uint16_t val) {

-  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));

 }
 void cds_atomic_store32(void * obj, int atomic_index, uint32_t val) {
 }
 void cds_atomic_store32(void * obj, int atomic_index, uint32_t val) {

-  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));

 }
 void cds_atomic_store64(void * obj, int atomic_index, uint64_t val) {
 }
 void cds_atomic_store64(void * obj, int atomic_index, uint64_t val) {

-  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, val));
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, val));

 }
 
 /*
 }
 
 /*

-#define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val )            \
-({                                                                      \
-  uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);   \
-  uint##size##_t _copy = _old;                                          \
-  _copy __op__ ( uint##size##_t ) _val;                                 \
-  model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy);        \
-  return _old;                                                          \
-})*/
+ #define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val )            \
+   ({                                                                      \
+   uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);   \
+   uint##size##_t _copy = _old;                                          \
+   _copy __op__ ( uint##size##_t ) _val;                                 \
+   model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy);        \
+   return _old;                                                          \
+   })*/

 
 #define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val )            \
 
 #define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val )            \

-({                                                                      \
-  uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);   \
-  uint##size##_t _copy = _old;                                          \
-  uint##size##_t _val = val;                                            \
-  _copy __op__ _val;                                                    \
-  model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy);        \
-  return _old;                                                          \
-})
+       ({                                                                      \
+               uint ## size ## _t _old = model_rmwr_action_helper(addr, atomic_index);   \
+               uint ## size ## _t _copy = _old;                                          \
+               uint ## size ## _t _val = val;                                            \
+               _copy __op__ _val;                                                    \
+               model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy);        \
+               return _old;                                                          \
+       })

 
 // cds atomic exchange
 uint8_t cds_atomic_exchange8(void* addr, int atomic_index, uint8_t val) {
 
 // cds atomic exchange
 uint8_t cds_atomic_exchange8(void* addr, int atomic_index, uint8_t val) {

-  _ATOMIC_RMW_( = , 8, addr, atomic_index, val);
+       _ATOMIC_RMW_( =, 8, addr, atomic_index, val);

 }
 uint16_t cds_atomic_exchange16(void* addr, int atomic_index, uint16_t val) {
 }
 uint16_t cds_atomic_exchange16(void* addr, int atomic_index, uint16_t val) {

-  _ATOMIC_RMW_( = , 16, addr, atomic_index, val);
+       _ATOMIC_RMW_( =, 16, addr, atomic_index, val);

 }
 uint32_t cds_atomic_exchange32(void* addr, int atomic_index, uint32_t val) {
 }
 uint32_t cds_atomic_exchange32(void* addr, int atomic_index, uint32_t val) {

-  _ATOMIC_RMW_( = , 32, addr, atomic_index, val);
+       _ATOMIC_RMW_( =, 32, addr, atomic_index, val);

 }
 uint64_t cds_atomic_exchange64(void* addr, int atomic_index, uint64_t val) {
 }
 uint64_t cds_atomic_exchange64(void* addr, int atomic_index, uint64_t val) {

-  _ATOMIC_RMW_( = , 64, addr, atomic_index, val);
+       _ATOMIC_RMW_( =, 64, addr, atomic_index, val);

 }
 
 // cds atomic fetch add
 uint8_t cds_atomic_fetch_add8(void* addr, int atomic_index, uint8_t val) {
 }
 
 // cds atomic fetch add
 uint8_t cds_atomic_fetch_add8(void* addr, int atomic_index, uint8_t val) {

-  _ATOMIC_RMW_( += , 8, addr, atomic_index, val);
+       _ATOMIC_RMW_( +=, 8, addr, atomic_index, val);

 }
 uint16_t cds_atomic_fetch_add16(void* addr, int atomic_index, uint16_t val) {
 }
 uint16_t cds_atomic_fetch_add16(void* addr, int atomic_index, uint16_t val) {

-  _ATOMIC_RMW_( += , 16, addr, atomic_index, val);
+       _ATOMIC_RMW_( +=, 16, addr, atomic_index, val);

 }
 uint32_t cds_atomic_fetch_add32(void* addr, int atomic_index, uint32_t val) {
 }
 uint32_t cds_atomic_fetch_add32(void* addr, int atomic_index, uint32_t val) {

-  _ATOMIC_RMW_( += , 32, addr, atomic_index, val);
+       _ATOMIC_RMW_( +=, 32, addr, atomic_index, val);

 }
 uint64_t cds_atomic_fetch_add64(void* addr, int atomic_index, uint64_t val) {
 }
 uint64_t cds_atomic_fetch_add64(void* addr, int atomic_index, uint64_t val) {

-  _ATOMIC_RMW_( += , 64, addr, atomic_index, val);
+       _ATOMIC_RMW_( +=, 64, addr, atomic_index, val);

 }
 
 // cds atomic fetch sub
 uint8_t cds_atomic_fetch_sub8(void* addr, int atomic_index, uint8_t val) {
 }
 
 // cds atomic fetch sub
 uint8_t cds_atomic_fetch_sub8(void* addr, int atomic_index, uint8_t val) {

-  _ATOMIC_RMW_( -= , 8, addr, atomic_index, val);
+       _ATOMIC_RMW_( -=, 8, addr, atomic_index, val);

 }
 uint16_t cds_atomic_fetch_sub16(void* addr, int atomic_index, uint16_t val) {
 }
 uint16_t cds_atomic_fetch_sub16(void* addr, int atomic_index, uint16_t val) {

-  _ATOMIC_RMW_( -= , 16, addr, atomic_index, val);
+       _ATOMIC_RMW_( -=, 16, addr, atomic_index, val);

 }
 uint32_t cds_atomic_fetch_sub32(void* addr, int atomic_index, uint32_t val) {
 }
 uint32_t cds_atomic_fetch_sub32(void* addr, int atomic_index, uint32_t val) {

-  _ATOMIC_RMW_( -= , 32, addr, atomic_index, val);
+       _ATOMIC_RMW_( -=, 32, addr, atomic_index, val);

 }
 uint64_t cds_atomic_fetch_sub64(void* addr, int atomic_index, uint64_t val) {
 }
 uint64_t cds_atomic_fetch_sub64(void* addr, int atomic_index, uint64_t val) {

-  _ATOMIC_RMW_( -= , 64, addr, atomic_index, val);
+       _ATOMIC_RMW_( -=, 64, addr, atomic_index, val);

 }
 
 // cds atomic fetch and
 uint8_t cds_atomic_fetch_and8(void* addr, int atomic_index, uint8_t val) {
 }
 
 // cds atomic fetch and
 uint8_t cds_atomic_fetch_and8(void* addr, int atomic_index, uint8_t val) {

-  _ATOMIC_RMW_( &= , 8, addr, atomic_index, val);
+       _ATOMIC_RMW_( &=, 8, addr, atomic_index, val);

 }
 uint16_t cds_atomic_fetch_and16(void* addr, int atomic_index, uint16_t val) {
 }
 uint16_t cds_atomic_fetch_and16(void* addr, int atomic_index, uint16_t val) {

-  _ATOMIC_RMW_( &= , 16, addr, atomic_index, val);
+       _ATOMIC_RMW_( &=, 16, addr, atomic_index, val);

 }
 uint32_t cds_atomic_fetch_and32(void* addr, int atomic_index, uint32_t val) {
 }
 uint32_t cds_atomic_fetch_and32(void* addr, int atomic_index, uint32_t val) {

-  _ATOMIC_RMW_( &= , 32, addr, atomic_index, val);
+       _ATOMIC_RMW_( &=, 32, addr, atomic_index, val);

 }
 uint64_t cds_atomic_fetch_and64(void* addr, int atomic_index, uint64_t val) {
 }
 uint64_t cds_atomic_fetch_and64(void* addr, int atomic_index, uint64_t val) {

-  _ATOMIC_RMW_( &= , 64, addr, atomic_index, val);
+       _ATOMIC_RMW_( &=, 64, addr, atomic_index, val);

 }
 
 // cds atomic fetch or
 uint8_t cds_atomic_fetch_or8(void* addr, int atomic_index, uint8_t val) {
 }
 
 // cds atomic fetch or
 uint8_t cds_atomic_fetch_or8(void* addr, int atomic_index, uint8_t val) {

-  _ATOMIC_RMW_( |= , 8, addr, atomic_index, val);
+       _ATOMIC_RMW_( |=, 8, addr, atomic_index, val);

 }
 uint16_t cds_atomic_fetch_or16(void* addr, int atomic_index, uint16_t val) {
 }
 uint16_t cds_atomic_fetch_or16(void* addr, int atomic_index, uint16_t val) {

-  _ATOMIC_RMW_( |= , 16, addr, atomic_index, val);
+       _ATOMIC_RMW_( |=, 16, addr, atomic_index, val);

 }
 uint32_t cds_atomic_fetch_or32(void* addr, int atomic_index, uint32_t val) {
 }
 uint32_t cds_atomic_fetch_or32(void* addr, int atomic_index, uint32_t val) {

-  _ATOMIC_RMW_( |= , 32, addr, atomic_index, val);
+       _ATOMIC_RMW_( |=, 32, addr, atomic_index, val);

 }
 uint64_t cds_atomic_fetch_or64(void* addr, int atomic_index, uint64_t val) {
 }
 uint64_t cds_atomic_fetch_or64(void* addr, int atomic_index, uint64_t val) {

-  _ATOMIC_RMW_( |= , 64, addr, atomic_index, val);
+       _ATOMIC_RMW_( |=, 64, addr, atomic_index, val);

 }
 
 // cds atomic fetch xor
 uint8_t cds_atomic_fetch_xor8(void* addr, int atomic_index, uint8_t val) {
 }
 
 // cds atomic fetch xor
 uint8_t cds_atomic_fetch_xor8(void* addr, int atomic_index, uint8_t val) {

-  _ATOMIC_RMW_( ^= , 8, addr, atomic_index, val);
+       _ATOMIC_RMW_( ^=, 8, addr, atomic_index, val);

 }
 uint16_t cds_atomic_fetch_xor16(void* addr, int atomic_index, uint16_t val) {
 }
 uint16_t cds_atomic_fetch_xor16(void* addr, int atomic_index, uint16_t val) {

-  _ATOMIC_RMW_( ^= , 16, addr, atomic_index, val);
+       _ATOMIC_RMW_( ^=, 16, addr, atomic_index, val);

 }
 uint32_t cds_atomic_fetch_xor32(void* addr, int atomic_index, uint32_t val) {
 }
 uint32_t cds_atomic_fetch_xor32(void* addr, int atomic_index, uint32_t val) {

-  _ATOMIC_RMW_( ^= , 32, addr, atomic_index, val);
+       _ATOMIC_RMW_( ^=, 32, addr, atomic_index, val);

 }
 uint64_t cds_atomic_fetch_xor64(void* addr, int atomic_index, uint64_t val) {
 }
 uint64_t cds_atomic_fetch_xor64(void* addr, int atomic_index, uint64_t val) {

-  _ATOMIC_RMW_( ^= , 64, addr, atomic_index, val);
+       _ATOMIC_RMW_( ^=, 64, addr, atomic_index, val);

 }
 
 // cds atomic compare and exchange
 }
 
 // cds atomic compare and exchange

-// In order to accomodate the LLVM PASS, the return values are not true or false. 
+// In order to accomodate the LLVM PASS, the return values are not true or false.

 
 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index)                            \
 
 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index)                            \

-({                                                                                              \
-  uint##size##_t _desired = desired;                                                            \
-  uint##size##_t _expected = expected;                                                          \
-  uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);                           \
-  if (_old == _expected  ) {                                                                    \
-    model_rmw_action_helper(addr, atomic_index, (uint64_t) _desired ); return _expected; }      \
-  else {                                                                                        \
-    model_rmwc_action_helper(addr, atomic_index); _expected = _old; return _old; }              \
-})
+       ({                                                                                              \
+               uint ## size ## _t _desired = desired;                                                            \
+               uint ## size ## _t _expected = expected;                                                          \
+               uint ## size ## _t _old = model_rmwr_action_helper(addr, atomic_index);                           \
+               if (_old == _expected  ) {                                                                    \
+                       model_rmw_action_helper(addr, atomic_index, (uint64_t) _desired ); return _expected; }      \
+               else {                                                                                        \
+                       model_rmwc_action_helper(addr, atomic_index); _expected = _old; return _old; }              \
+       })

 
 // expected is supposed to be a pointer to an address, but the CmpOperand
 
 // expected is supposed to be a pointer to an address, but the CmpOperand

-// extracted from LLVM IR is an integer type. 
+// extracted from LLVM IR is an integer type.

 
 

-uint8_t cds_atomic_compare_exchange8(void* addr, uint8_t expected, 
-                uint8_t desired, int atomic_index_succ, int atomic_index_fail ) {
-  _ATOMIC_CMPSWP_(8, addr, expected, desired, atomic_index_succ );
+uint8_t cds_atomic_compare_exchange8(void* addr, uint8_t expected,
+                                                                                                                                                uint8_t desired, int atomic_index_succ, int atomic_index_fail ) {
+       _ATOMIC_CMPSWP_(8, addr, expected, desired, atomic_index_succ );

 }
 uint16_t cds_atomic_compare_exchange16(void* addr, uint16_t expected,
 }
 uint16_t cds_atomic_compare_exchange16(void* addr, uint16_t expected,

-                uint16_t desired, int atomic_index_succ, int atomic_index_fail ) {
-  _ATOMIC_CMPSWP_(16, addr, expected, desired, atomic_index_succ );
+                                                                                                                                                        uint16_t desired, int atomic_index_succ, int atomic_index_fail ) {
+       _ATOMIC_CMPSWP_(16, addr, expected, desired, atomic_index_succ );

 }
 }

-uint32_t cds_atomic_compare_exchange32(void* addr, uint32_t expected, 
-                uint32_t desired, int atomic_index_succ, int atomic_index_fail ) {
-  _ATOMIC_CMPSWP_(32, addr, expected, desired, atomic_index_succ );
+uint32_t cds_atomic_compare_exchange32(void* addr, uint32_t expected,
+                                                                                                                                                        uint32_t desired, int atomic_index_succ, int atomic_index_fail ) {
+       _ATOMIC_CMPSWP_(32, addr, expected, desired, atomic_index_succ );

 }
 }

-uint64_t cds_atomic_compare_exchange64(void* addr, uint64_t expected, 
-                uint64_t desired, int atomic_index_succ, int atomic_index_fail ) {
-  _ATOMIC_CMPSWP_(64, addr, expected, desired, atomic_index_succ );
+uint64_t cds_atomic_compare_exchange64(void* addr, uint64_t expected,
+                                                                                                                                                        uint64_t desired, int atomic_index_succ, int atomic_index_fail ) {
+       _ATOMIC_CMPSWP_(64, addr, expected, desired, atomic_index_succ );

 }
 
 // cds atomic thread fence
 }
 
 // cds atomic thread fence


@@ -248,7 +248,7 @@ void cds_atomic_thread_fence(int atomic_index) {
 }
 
 /*
 }
 
 /*

-#define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ )                         \
+ #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ )                         \

         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
                 __typeof__(__e__) __q__ = (__e__);                            \
                 __typeof__(__m__) __v__ = (__m__);                            \
         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
                 __typeof__(__e__) __q__ = (__e__);                            \
                 __typeof__(__m__) __v__ = (__m__);                            \


@@ -259,13 +259,13 @@ void cds_atomic_thread_fence(int atomic_index) {
                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
                 __r__; })
 
                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
                 __r__; })
 

-#define _ATOMIC_FENCE_( __x__ ) \
+ #define _ATOMIC_FENCE_( __x__ ) \

         ({ model_fence_action(__x__);})
         ({ model_fence_action(__x__);})

-*/
+ */

 
 /*
 
 
 /*
 

-#define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ )                         \
+ #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__);                                    \
         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
         __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
         __typeof__(__m__) __v__ = (__m__);                                    \


@@ -273,5 +273,5 @@ void cds_atomic_thread_fence(int atomic_index) {
         __copy__ __o__ __v__;                                                 \
         model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);          \
         __old__ = __old__;  Silence clang (-Wunused-value)                    \
         __copy__ __o__ __v__;                                                 \
         model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);          \
         __old__ = __old__;  Silence clang (-Wunused-value)                    \

-         })                           
-*/
+         })
+ */

diff --git a/common.cc b/common.cc
index 26f6d5d8cd42bdd28484c231a995b5fbe84c633b..f327d27ed9e122a68ab1c8a1a831c9f62a928ef6 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -33,11 +33,11 @@ void print_trace(void)
 
        model_print("\nDumping stack trace (%d frames):\n", size);
 
 
        model_print("\nDumping stack trace (%d frames):\n", size);
 

-       for (i = 0; i < size; i++)
+       for (i = 0;i < size;i++)

                model_print("\t%s\n", strings[i]);
 
        free(strings);
                model_print("\t%s\n", strings[i]);
 
        free(strings);

-#endif /* CONFIG_STACKTRACE */
+#endif/* CONFIG_STACKTRACE */

 }
 
 void assert_hook(void)
 }
 
 void assert_hook(void)


@@ -50,14 +50,14 @@ void model_assert(bool expr, const char *file, int line)
        if (!expr) {
                char msg[100];
                sprintf(msg, "Program has hit assertion in file %s at line %d\n",
        if (!expr) {
                char msg[100];
                sprintf(msg, "Program has hit assertion in file %s at line %d\n",

-                               file, line);
+                                               file, line);

                model->assert_user_bug(msg);
        }
 }
 
 #ifndef CONFIG_DEBUG
 
                model->assert_user_bug(msg);
        }
 }
 
 #ifndef CONFIG_DEBUG
 

-static int fd_user_out; /**< @brief File descriptor from which to read user program output */
+static int fd_user_out;        /**< @brief File descriptor from which to read user program output */

 
 /**
  * @brief Setup output redirecting
 
 /**
  * @brief Setup output redirecting


@@ -139,7 +139,7 @@ void clear_program_output()
 {
        fflush(stdout);
        char buf[200];
 {
        fflush(stdout);
        char buf[200];

-       while (read_to_buf(fd_user_out, buf, sizeof(buf)));
+       while (read_to_buf(fd_user_out, buf, sizeof(buf))) ;

 }
 
 /** @brief Print out any pending program output */
 }
 
 /** @brief Print out any pending program output */


@@ -170,4 +170,4 @@ void print_program_output()
 
        model_print("---- END PROGRAM OUTPUT   ----\n");
 }
 
        model_print("---- END PROGRAM OUTPUT   ----\n");
 }

-#endif /* ! CONFIG_DEBUG */
+#endif/* ! CONFIG_DEBUG */

diff --git a/common.h b/common.h
index 7be72d72f8e0b56fc8f333ffe25489685b053f60..1b2b673f1fd3c81b8e342fbfa68205163b216135 100644 (file)
--- a/common.h
+++ b/common.h
@@ -11,10 +11,10 @@
 extern int model_out;
 extern int switch_alloc;
 
 extern int model_out;
 extern int switch_alloc;
 

-#define model_print(fmt, ...) do { switch_alloc = 1; dprintf(model_out, fmt, ##__VA_ARGS__); switch_alloc = 0; } while (0)
+#define model_print(fmt, ...) do { switch_alloc = 1; dprintf(model_out, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)

 
 #ifdef CONFIG_DEBUG
 
 #ifdef CONFIG_DEBUG

-#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
+#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ## __VA_ARGS__); } while (0)

 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else
 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else


@@ -27,20 +27,20 @@ void assert_hook(void);
 
 #ifdef CONFIG_ASSERT
 #define ASSERT(expr) \
 
 #ifdef CONFIG_ASSERT
 #define ASSERT(expr) \

-do { \
-       if (!(expr)) { \
-               fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
-               /* print_trace(); // Trace printing may cause dynamic memory allocation */ \
-               assert_hook();                           \
-               exit(EXIT_FAILURE); \
-       } \
-} while (0)
+       do { \
+               if (!(expr)) { \
+                       fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
+                       /* print_trace(); // Trace printing may cause dynamic memory allocation */ \
+                       assert_hook();                           \
+                       exit(EXIT_FAILURE); \
+               } \
+       } while (0)

 #else
 #define ASSERT(expr) \
        do { } while (0)
 #else
 #define ASSERT(expr) \
        do { } while (0)

-#endif /* CONFIG_ASSERT */
+#endif/* CONFIG_ASSERT */

 
 #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
 
 void print_trace(void);
 
 #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
 
 void print_trace(void);

-#endif /* __COMMON_H__ */
+#endif/* __COMMON_H__ */

diff --git a/conditionvariable.cc b/conditionvariable.cc
index d5d0fc83e3bad340c15a85b97f611dfb50224b57..1d049f1893c4bd66fb799ef0caba1eedd814f933 100644 (file)
--- a/conditionvariable.cc
+++ b/conditionvariable.cc
@@ -6,11 +6,11 @@
 namespace cdsc {
 
 condition_variable::condition_variable() {
 namespace cdsc {
 
 condition_variable::condition_variable() {

-               
+

 }
 
 condition_variable::~condition_variable() {
 }
 
 condition_variable::~condition_variable() {

-               
+

 }
 
 void condition_variable::notify_one() {
 }
 
 void condition_variable::notify_one() {

diff --git a/config.h b/config.h
index afbac874d785b3a31b7af13a7c284f30ac51ff2f..ac725c3582c6f05c9d39c7d176b82ddd430c97fa 100644 (file)
--- a/config.h
+++ b/config.h
@@ -7,13 +7,13 @@
 
 /** Turn on debugging. */
 /*             #ifndef CONFIG_DEBUG
 
 /** Turn on debugging. */
 /*             #ifndef CONFIG_DEBUG

-               #define CONFIG_DEBUG
-               #endif
+ #define CONFIG_DEBUG
+ #endif

 
 

-               #ifndef CONFIG_ASSERT
-               #define CONFIG_ASSERT
-               #endif
-*/
+ #ifndef CONFIG_ASSERT
+ #define CONFIG_ASSERT
+ #endif
+ */

 
 /** Turn on support for dumping cyclegraphs as dot files at each
  *  printed summary.*/
 
 /** Turn on support for dumping cyclegraphs as dot files at each
  *  printed summary.*/


@@ -27,11 +27,11 @@
 #else
 #define BIT48 0
 #endif
 #else
 #define BIT48 0
 #endif

-#endif /* BIT48 */
+#endif/* BIT48 */

 
 /** Snapshotting configurables */
 
 
 /** Snapshotting configurables */
 

-/** 
+/**

  * If USE_MPROTECT_SNAPSHOT=2, then snapshot by tuned mmap() algorithm
  * If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
  * If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */
  * If USE_MPROTECT_SNAPSHOT=2, then snapshot by tuned mmap() algorithm
  * If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
  * If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */

diff --git a/context.cc b/context.cc
index b5ae0ba553b6fae105d2a9c008f5393c9f6cb513..d446fa76ba9248fec4a6666775b5c11bd192d907 100644 (file)
--- a/context.cc
+++ b/context.cc
@@ -24,4 +24,4 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
        return 0;
 }
 
        return 0;
 }
 

-#endif /* MAC */
+#endif/* MAC */

diff --git a/context.h b/context.h
index fb56e24761174fdb598f8f055c066ed6420ba02c..f0003ce4c4fd4637f9b86cef7d0e45a08382c552 100644 (file)
--- a/context.h
+++ b/context.h
@@ -13,13 +13,13 @@
 
 int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp);
 
 
 int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp);
 

-#else /* !MAC */
+#else  /* !MAC */

 
 static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
 
 static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)

-{      
+{

        return swapcontext(oucp, ucp);
 }
 
        return swapcontext(oucp, ucp);
 }
 

-#endif /* !MAC */
+#endif/* !MAC */

 
 

-#endif /* __CONTEXT_H__ */
+#endif/* __CONTEXT_H__ */

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 439e61969b22cf4a72220ba73aedbeb8d3651e2d..f4590bfb6fa1cd44b41efdd91157ddcdfa812d78 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -69,7 +69,7 @@ bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
                if (!hasCycles)
                        hasCycles = checkReachable(tonode, fromnode);
        } else
                if (!hasCycles)
                        hasCycles = checkReachable(tonode, fromnode);
        } else

-               return false; /* No new edge */
+               return false;                                                   /* No new edge */

 
        /*
         * If the fromnode has a rmwnode that is not the tonode, we should
 
        /*
         * If the fromnode has a rmwnode that is not the tonode, we should


@@ -130,7 +130,7 @@ void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
         * (2) the fromnode is the new node and therefore it should not
         * have any outgoing edges.
         */
         * (2) the fromnode is the new node and therefore it should not
         * have any outgoing edges.
         */

-       for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) {
+       for (unsigned int i = 0;i < fromnode->getNumEdges();i++) {

                CycleNode *tonode = fromnode->getEdge(i);
                if (tonode != rmwnode) {
                        if (rmwnode->addEdge(tonode))
                CycleNode *tonode = fromnode->getEdge(i);
                if (tonode != rmwnode) {
                        if (rmwnode->addEdge(tonode))


@@ -174,11 +174,11 @@ template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to
 
 static void print_node(FILE *file, const CycleNode *node, int label)
 {
 
 static void print_node(FILE *file, const CycleNode *node, int label)
 {

-               const ModelAction *act = node->getAction();
-               modelclock_t idx = act->get_seq_number();
-               fprintf(file, "N%u", idx);
-               if (label)
-                       fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
+       const ModelAction *act = node->getAction();
+       modelclock_t idx = act->get_seq_number();
+       fprintf(file, "N%u", idx);
+       if (label)
+               fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());

 }
 
 static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop)
 }
 
 static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop)


@@ -209,13 +209,13 @@ template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, co
 
 void CycleGraph::dumpNodes(FILE *file) const
 {
 
 void CycleGraph::dumpNodes(FILE *file) const
 {

-       for (unsigned int i = 0; i < nodeList.size(); i++) {
+       for (unsigned int i = 0;i < nodeList.size();i++) {

                CycleNode *n = nodeList[i];
                print_node(file, n, 1);
                fprintf(file, ";\n");
                if (n->getRMW())
                        print_edge(file, n, n->getRMW(), "style=dotted");
                CycleNode *n = nodeList[i];
                print_node(file, n, 1);
                fprintf(file, ";\n");
                if (n->getRMW())
                        print_edge(file, n, n->getRMW(), "style=dotted");

-               for (unsigned int j = 0; j < n->getNumEdges(); j++)
+               for (unsigned int j = 0;j < n->getNumEdges();j++)

                        print_edge(file, n, n->getEdge(j), NULL);
        }
 }
                        print_edge(file, n, n->getEdge(j), NULL);
        }
 }


@@ -249,7 +249,7 @@ bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) cons
                queue->pop_back();
                if (node == to)
                        return true;
                queue->pop_back();
                if (node == to)
                        return true;

-               for (unsigned int i = 0; i < node->getNumEdges(); i++) {
+               for (unsigned int i = 0;i < node->getNumEdges();i++) {

                        CycleNode *next = node->getEdge(i);
                        if (!discovered->contains(next)) {
                                discovered->put(next, next);
                        CycleNode *next = node->getEdge(i);
                        if (!discovered->contains(next)) {
                                discovered->put(next, next);


@@ -279,7 +279,7 @@ bool CycleGraph::checkReachable(const T *from, const U *to) const
 }
 /* Instantiate four forms of CycleGraph::checkReachable */
 template bool CycleGraph::checkReachable(const ModelAction *from,
 }
 /* Instantiate four forms of CycleGraph::checkReachable */
 template bool CycleGraph::checkReachable(const ModelAction *from,

-               const ModelAction *to) const;
+                                                                                                                                                                const ModelAction *to) const;

 
 /** @brief Begin a new sequence of graph additions which can be rolled back */
 void CycleGraph::startChanges()
 
 /** @brief Begin a new sequence of graph additions which can be rolled back */
 void CycleGraph::startChanges()


@@ -300,10 +300,10 @@ void CycleGraph::commitChanges()
 /** Rollback changes to the previous commit. */
 void CycleGraph::rollbackChanges()
 {
 /** Rollback changes to the previous commit. */
 void CycleGraph::rollbackChanges()
 {

-       for (unsigned int i = 0; i < rollbackvector.size(); i++)
+       for (unsigned int i = 0;i < rollbackvector.size();i++)

                rollbackvector[i]->removeEdge();
 
                rollbackvector[i]->removeEdge();
 

-       for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
+       for (unsigned int i = 0;i < rmwrollbackvector.size();i++)

                rmwrollbackvector[i]->clearRMW();
 
        hasCycles = oldCycles;
                rmwrollbackvector[i]->clearRMW();
 
        hasCycles = oldCycles;


@@ -366,7 +366,7 @@ unsigned int CycleNode::getNumBackEdges() const
 template <typename T>
 static bool vector_remove_node(SnapVector<T>& v, const T n)
 {
 template <typename T>
 static bool vector_remove_node(SnapVector<T>& v, const T n)
 {

-       for (unsigned int i = 0; i < v.size(); i++) {
+       for (unsigned int i = 0;i < v.size();i++) {

                if (v[i] == n) {
                        v.erase(v.begin() + i);
                        return true;
                if (v[i] == n) {
                        v.erase(v.begin() + i);
                        return true;


@@ -412,7 +412,7 @@ CycleNode * CycleNode::removeBackEdge()
  */
 bool CycleNode::addEdge(CycleNode *node)
 {
  */
 bool CycleNode::addEdge(CycleNode *node)
 {

-       for (unsigned int i = 0; i < edges.size(); i++)
+       for (unsigned int i = 0;i < edges.size();i++)

                if (edges[i] == node)
                        return false;
        edges.push_back(node);
                if (edges[i] == node)
                        return false;
        edges.push_back(node);

diff --git a/cyclegraph.h b/cyclegraph.h
index 556af1cfdd04627c8b9a5d70d05c3078b01c3469..d273279a6e8aa322e2eb01aed3ebb5d1082a15eb 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -20,7 +20,7 @@
 
 /** @brief A graph of Model Actions for tracking cycles. */
 class CycleGraph {
 
 /** @brief A graph of Model Actions for tracking cycles. */
 class CycleGraph {

- public:
+public:

        CycleGraph();
        ~CycleGraph();
 
        CycleGraph();
        ~CycleGraph();
 


@@ -49,7 +49,7 @@ class CycleGraph {
        CycleNode * getNode_noCreate(const ModelAction *act) const;
 
        SNAPSHOTALLOC
        CycleNode * getNode_noCreate(const ModelAction *act) const;
 
        SNAPSHOTALLOC

- private:
+private:

        bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode);
        void putNode(const ModelAction *act, CycleNode *node);
        CycleNode * getNode(const ModelAction *act);
        bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode);
        void putNode(const ModelAction *act, CycleNode *node);
        CycleNode * getNode(const ModelAction *act);


@@ -81,7 +81,7 @@ class CycleGraph {
  * @brief A node within a CycleGraph; corresponds either to one ModelAction
  */
 class CycleNode {
  * @brief A node within a CycleGraph; corresponds either to one ModelAction
  */
 class CycleNode {

- public:
+public:

        CycleNode(const ModelAction *act);
        bool addEdge(CycleNode *node);
        CycleNode * getEdge(unsigned int i) const;
        CycleNode(const ModelAction *act);
        bool addEdge(CycleNode *node);
        CycleNode * getEdge(unsigned int i) const;


@@ -97,7 +97,7 @@ class CycleNode {
        const ModelAction * getAction() const { return action; }
 
        SNAPSHOTALLOC
        const ModelAction * getAction() const { return action; }
 
        SNAPSHOTALLOC

- private:
+private:

        /** @brief The ModelAction that this node represents */
        const ModelAction *action;
 
        /** @brief The ModelAction that this node represents */
        const ModelAction *action;
 


@@ -112,4 +112,4 @@ class CycleNode {
        CycleNode *hasRMW;
 };
 
        CycleNode *hasRMW;
 };
 

-#endif /* __CYCLEGRAPH_H__ */
+#endif/* __CYCLEGRAPH_H__ */

diff --git a/datarace.cc b/datarace.cc
index 653039b3307e3ebfb195e2dc99efda36ae123a7c..9ba59399f2a07c52cf62136a897e59cd55717739 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -69,7 +69,7 @@ static uint64_t * lookupAddressEntry(const void *address)
  * @return true if the current clock allows a race with the event at clock2/tid2
  */
 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
  * @return true if the current clock allows a race with the event at clock2/tid2
  */
 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,

-                           modelclock_t clock2, thread_id_t tid2)
+                                                                                                        modelclock_t clock2, thread_id_t tid2)

 {
        return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
 }
 {
        return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
 }


@@ -133,7 +133,7 @@ bool checkDataRaces()
        if (get_execution()->isfeasibleprefix()) {
                bool race_asserted = false;
                /* Prune the non-racing unrealized dataraces */
        if (get_execution()->isfeasibleprefix()) {
                bool race_asserted = false;
                /* Prune the non-racing unrealized dataraces */

-               for (unsigned i = 0; i < unrealizedraces->size(); i++) {
+               for (unsigned i = 0;i < unrealizedraces->size();i++) {

                        struct DataRace *race = (*unrealizedraces)[i];
                        if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
                                assert_race(race);
                        struct DataRace *race = (*unrealizedraces)[i];
                        if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
                                assert_race(race);


@@ -158,16 +158,16 @@ bool checkDataRaces()
 void assert_race(struct DataRace *race)
 {
        model->assert_bug(
 void assert_race(struct DataRace *race)
 {
        model->assert_bug(

-                       "Data race detected @ address %p:\n"
-                       "    Access 1: %5s in thread %2d @ clock %3u\n"
-                       "    Access 2: %5s in thread %2d @ clock %3u",
-                       race->address,
-                       race->isoldwrite ? "write" : "read",
-                       id_to_int(race->oldthread),
-                       race->oldclock,
-                       race->isnewwrite ? "write" : "read",
-                       id_to_int(race->newaction->get_tid()),
-                       race->newaction->get_seq_number()
+               "Data race detected @ address %p:\n"
+               "    Access 1: %5s in thread %2d @ clock %3u\n"
+               "    Access 2: %5s in thread %2d @ clock %3u",
+               race->address,
+               race->isoldwrite ? "write" : "read",
+               id_to_int(race->oldthread),
+               race->oldclock,
+               race->isnewwrite ? "write" : "read",
+               id_to_int(race->newaction->get_tid()),
+               race->newaction->get_seq_number()

                );
 }
 
                );
 }
 


@@ -178,12 +178,12 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
        /* Check for datarace against last read. */
 
 
        /* Check for datarace against last read. */
 

-       for (int i = 0; i < record->numReads; i++) {
+       for (int i = 0;i < record->numReads;i++) {

                modelclock_t readClock = record->readClock[i];
                thread_id_t readThread = record->thread[i];
 
                /* Note that readClock can't actuall be zero here, so it could be
                modelclock_t readClock = record->readClock[i];
                thread_id_t readThread = record->thread[i];
 
                /* Note that readClock can't actuall be zero here, so it could be

-                        optimized. */
+                        optimized. */

 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* We have a datarace */
 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* We have a datarace */


@@ -271,15 +271,15 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
 
        int copytoindex = 0;
 
 
        int copytoindex = 0;
 

-       for (int i = 0; i < record->numReads; i++) {
+       for (int i = 0;i < record->numReads;i++) {

                modelclock_t readClock = record->readClock[i];
                thread_id_t readThread = record->thread[i];
 
                /*  Note that is not really a datarace check as reads cannott
                modelclock_t readClock = record->readClock[i];
                thread_id_t readThread = record->thread[i];
 
                /*  Note that is not really a datarace check as reads cannott

-                               actually race.  It is just determining that this read subsumes
-                               another in the sense that either this read races or neither
-                               read races. Note that readClock can't actually be zero, so it
-                               could be optimized.  */
+                               actually race.  It is just determining that this read subsumes
+                               another in the sense that either this read races or neither
+                               read races. Note that readClock can't actually be zero, so it
+                               could be optimized.  */

 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* Still need this read in vector */
 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* Still need this read in vector */

diff --git a/datarace.h b/datarace.h
index a8f0ba323c05df01937e0b953c5b0e8abd22a70d..ce659d1ac7792793f253fa93378437f6060351c5 100644 (file)
--- a/datarace.h
+++ b/datarace.h
@@ -20,7 +20,7 @@ struct ShadowBaseTable {
 
 struct DataRace {
        /* Clock and thread associated with first action.  This won't change in
 
 struct DataRace {
        /* Clock and thread associated with first action.  This won't change in

-                response to synchronization. */
+                response to synchronization. */

 
        thread_id_t oldthread;
        modelclock_t oldclock;
 
        thread_id_t oldthread;
        modelclock_t oldclock;


@@ -28,7 +28,7 @@ struct DataRace {
        bool isoldwrite;
 
        /* Model action associated with second action.  This could change as
        bool isoldwrite;
 
        /* Model action associated with second action.  This could change as

-                a result of synchronization. */
+                a result of synchronization. */

        ModelAction *newaction;
        /* Record whether this is a write, so we can tell the user. */
        bool isnewwrite;
        ModelAction *newaction;
        /* Record whether this is a write, so we can tell the user. */
        bool isnewwrite;


@@ -89,4 +89,4 @@ struct RaceRecord {
 #define MAXREADVECTOR (READMASK-1)
 #define MAXWRITEVECTOR (WRITEMASK-1)
 
 #define MAXREADVECTOR (READMASK-1)
 #define MAXWRITEVECTOR (WRITEMASK-1)
 

-#endif /* __DATARACE_H__ */
+#endif/* __DATARACE_H__ */

diff --git a/execution.cc b/execution.cc
index 3a994892b7102692ea0423d8cc572cc00ed10163..f498efbb8d5250df4d07304802516ea8e7f1573f 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -16,7 +16,7 @@
 #include "bugmessage.h"
 #include "fuzzer.h"
 
 #include "bugmessage.h"
 #include "fuzzer.h"
 

-#define INITIAL_THREAD_ID      0
+#define INITIAL_THREAD_ID       0

 
 /**
  * Structure for holding small ModelChecker members that should be snapshotted
 
 /**
  * Structure for holding small ModelChecker members that should be snapshotted


@@ -33,7 +33,7 @@ struct model_snapshot_members {
        { }
 
        ~model_snapshot_members() {
        { }
 
        ~model_snapshot_members() {

-               for (unsigned int i = 0; i < bugs.size(); i++)
+               for (unsigned int i = 0;i < bugs.size();i++)

                        delete bugs[i];
                bugs.clear();
        }
                        delete bugs[i];
                bugs.clear();
        }


@@ -51,13 +51,13 @@ struct model_snapshot_members {
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,

-               Scheduler *scheduler,
-               NodeStack *node_stack) :
+                                                                                                                        Scheduler *scheduler,
+                                                                                                                        NodeStack *node_stack) :

        model(m),
        params(NULL),
        scheduler(scheduler),
        action_trace(),
        model(m),
        params(NULL),
        scheduler(scheduler),
        action_trace(),

-       thread_map(2), /* We'll always need at least 2 threads */
+       thread_map(2),                  /* We'll always need at least 2 threads */

        pthread_map(0),
        pthread_counter(0),
        obj_map(),
        pthread_map(0),
        pthread_counter(0),
        obj_map(),


@@ -67,8 +67,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
        thrd_last_action(1),
        thrd_last_fence_release(),
        node_stack(node_stack),
        thrd_last_action(1),
        thrd_last_fence_release(),
        node_stack(node_stack),

-       priv(new struct model_snapshot_members()),
-       mo_graph(new CycleGraph()),
+       priv(new struct model_snapshot_members ()),
+                        mo_graph(new CycleGraph()),

        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */
        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */


@@ -81,7 +81,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
 /** @brief Destructor */
 ModelExecution::~ModelExecution()
 {
 /** @brief Destructor */
 ModelExecution::~ModelExecution()
 {

-       for (unsigned int i = 0; i < get_num_threads(); i++)
+       for (unsigned int i = 0;i < get_num_threads();i++)

                delete get_thread(int_to_id(i));
 
        delete mo_graph;
                delete get_thread(int_to_id(i));
 
        delete mo_graph;


@@ -173,7 +173,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa
 
 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 {
 
 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 {

-       for (unsigned int i = 0; i < get_num_threads(); i++) {
+       for (unsigned int i = 0;i < get_num_threads();i++) {

                Thread *thr = get_thread(int_to_id(i));
                if (scheduler->is_sleep_set(thr)) {
                        if (should_wake_up(curr, thr))
                Thread *thr = get_thread(int_to_id(i));
                if (scheduler->is_sleep_set(thr)) {
                        if (should_wake_up(curr, thr))


@@ -250,7 +250,7 @@ void ModelExecution::set_assert()
 bool ModelExecution::is_deadlocked() const
 {
        bool blocking_threads = false;
 bool ModelExecution::is_deadlocked() const
 {
        bool blocking_threads = false;

-       for (unsigned int i = 0; i < get_num_threads(); i++) {
+       for (unsigned int i = 0;i < get_num_threads();i++) {

                thread_id_t tid = int_to_id(i);
                if (is_enabled(tid))
                        return false;
                thread_id_t tid = int_to_id(i);
                if (is_enabled(tid))
                        return false;


@@ -270,7 +270,7 @@ bool ModelExecution::is_deadlocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
  */
 bool ModelExecution::is_complete_execution() const
 {

-       for (unsigned int i = 0; i < get_num_threads(); i++)
+       for (unsigned int i = 0;i < get_num_threads();i++)

                if (is_enabled(int_to_id(i)))
                        return false;
        return true;
                if (is_enabled(int_to_id(i)))
                        return false;
        return true;


@@ -285,26 +285,26 @@ bool ModelExecution::is_complete_execution() const
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {

-  while(true) {
-               
-    int index = fuzzer->selectWrite(curr, rf_set);
-    const ModelAction *rf = (*rf_set)[index];
-
-    
-    ASSERT(rf);
-    
-    mo_graph->startChanges();
-    bool updated = r_modification_order(curr, rf);
-    if (!is_infeasible()) {
-      read_from(curr, rf);
-      mo_graph->commitChanges();
-      get_thread(curr)->set_return_value(curr->get_return_value());
-      return updated;
-    }
-    mo_graph->rollbackChanges();
-    (*rf_set)[index] = rf_set->back();
-    rf_set->pop_back();
-  }
+       while(true) {
+
+               int index = fuzzer->selectWrite(curr, rf_set);
+               const ModelAction *rf = (*rf_set)[index];
+
+
+               ASSERT(rf);
+
+               mo_graph->startChanges();
+               bool updated = r_modification_order(curr, rf);
+               if (!is_infeasible()) {
+                       read_from(curr, rf);
+                       mo_graph->commitChanges();
+                       get_thread(curr)->set_return_value(curr->get_return_value());
+                       return updated;
+               }
+               mo_graph->rollbackChanges();
+               (*rf_set)[index] = rf_set->back();
+               rf_set->pop_back();
+       }

 }
 
 /**
 }
 
 /**


@@ -341,7 +341,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                }
                get_thread(curr)->set_return_value(1);
        }
                }
                get_thread(curr)->set_return_value(1);
        }

-               //otherwise fall into the lock case
+       //otherwise fall into the lock case

        case ATOMIC_LOCK: {
                if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
                        assert_bug("Lock access before initialization");
        case ATOMIC_LOCK: {
                if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
                        assert_bug("Lock access before initialization");


@@ -357,7 +357,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        case ATOMIC_WAIT:
        case ATOMIC_UNLOCK: {
                /* wake up the other threads */
        case ATOMIC_WAIT:
        case ATOMIC_UNLOCK: {
                /* wake up the other threads */

-               for (unsigned int i = 0; i < get_num_threads(); i++) {
+               for (unsigned int i = 0;i < get_num_threads();i++) {

                        Thread *t = get_thread(int_to_id(i));
                        Thread *curr_thrd = get_thread(curr);
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
                        Thread *t = get_thread(int_to_id(i));
                        Thread *curr_thrd = get_thread(curr);
                        if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())


@@ -368,14 +368,14 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                state->locked = NULL;
 
                if (!curr->is_wait())
                state->locked = NULL;
 
                if (!curr->is_wait())

-                       break; /* The rest is only for ATOMIC_WAIT */
+                       break;                                                                  /* The rest is only for ATOMIC_WAIT */

 
                break;
        }
        case ATOMIC_NOTIFY_ALL: {
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                //activate all the waiting threads
 
                break;
        }
        case ATOMIC_NOTIFY_ALL: {
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                //activate all the waiting threads

-               for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+               for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {

                        scheduler->wake(get_thread(*rit));
                }
                waiters->clear();
                        scheduler->wake(get_thread(*rit));
                }
                waiters->clear();


@@ -430,7 +430,7 @@ bool ModelExecution::process_fence(ModelAction *curr)
                action_list_t *list = &action_trace;
                action_list_t::reverse_iterator rit;
                /* Find X : is_read(X) && X --sb-> curr */
                action_list_t *list = &action_trace;
                action_list_t::reverse_iterator rit;
                /* Find X : is_read(X) && X --sb-> curr */

-               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+               for (rit = list->rbegin();rit != list->rend();rit++) {

                        ModelAction *act = *rit;
                        if (act == curr)
                                continue;
                        ModelAction *act = *rit;
                        if (act == curr)
                                continue;


@@ -451,7 +451,7 @@ bool ModelExecution::process_fence(ModelAction *curr)
                        /* Establish hypothetical release sequences */
                        rel_heads_list_t release_heads;
                        get_release_seq_heads(curr, act, &release_heads);
                        /* 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++)
+                       for (unsigned int i = 0;i < release_heads.size();i++)

                                synchronize(release_heads[i], curr);
                        if (release_heads.size() != 0)
                                updated = true;
                                synchronize(release_heads[i], curr);
                        if (release_heads.size() != 0)
                                updated = true;


@@ -486,7 +486,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                break;
        }
        case PTHREAD_CREATE: {
                break;
        }
        case PTHREAD_CREATE: {

-         (*(uint32_t *)curr->get_location()) = pthread_counter++;
+               (*(uint32_t *)curr->get_location()) = pthread_counter++;

 
                struct pthread_params *params = (struct pthread_params *)curr->get_value();
                Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
 
                struct pthread_params *params = (struct pthread_params *)curr->get_value();
                Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));


@@ -494,8 +494,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                add_thread(th);
                th->set_creation(curr);
 
                add_thread(th);
                th->set_creation(curr);
 

-               if ( pthread_map.size() < pthread_counter )
-                       pthread_map.resize( pthread_counter );
+               if ( pthread_map.size() < pthread_counter )
+                       pthread_map.resize( pthread_counter );

                pthread_map[ pthread_counter-1 ] = th;
 
                break;
                pthread_map[ pthread_counter-1 ] = th;
 
                break;


@@ -504,28 +504,28 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);

-               updated = true; /* trigger rel-seq checks */
+               updated = true;                                                 /* trigger rel-seq checks */

                break;
        }
        case PTHREAD_JOIN: {
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
                break;
        }
        case PTHREAD_JOIN: {
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);

-               updated = true; /* trigger rel-seq checks */
-               break; // WL: to be add (modified)
+               updated = true;                                                 /* trigger rel-seq checks */
+               break;                                          // WL: to be add (modified)

        }
 
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                /* Wake up any joining threads */
        }
 
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                /* Wake up any joining threads */

-               for (unsigned int i = 0; i < get_num_threads(); i++) {
+               for (unsigned int i = 0;i < get_num_threads();i++) {

                        Thread *waiting = get_thread(int_to_id(i));
                        if (waiting->waiting_on() == th &&
                                        waiting->get_pending()->is_thread_join())
                                scheduler->wake(waiting);
                }
                th->complete();
                        Thread *waiting = get_thread(int_to_id(i));
                        if (waiting->waiting_on() == th &&
                                        waiting->get_pending()->is_thread_join())
                                scheduler->wake(waiting);
                }
                th->complete();

-               updated = true; /* trigger rel-seq checks */
+               updated = true;                                                 /* trigger rel-seq checks */

                break;
        }
        case THREAD_START: {
                break;
        }
        case THREAD_START: {


@@ -579,7 +579,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 
                *curr = newcurr;
                newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 
                *curr = newcurr;

-               return false; /* Action was explored previously */
+               return false;                                                   /* Action was explored previously */

        } else {
                newcurr = *curr;
 
        } else {
                newcurr = *curr;
 


@@ -589,7 +589,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                /* Assign most recent release fence */
                newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
 
                /* Assign most recent release fence */
                newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
 

-               return true; /* This was a new ModelAction */
+               return true;                                            /* This was a new ModelAction */

        }
 }
 
        }
 }
 


@@ -615,7 +615,7 @@ bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
                rel_heads_list_t release_heads;
                get_release_seq_heads(act, act, &release_heads);
                int num_heads = release_heads.size();
                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++)
+               for (unsigned int i = 0;i < release_heads.size();i++)

                        if (!synchronize(release_heads[i], act))
                                num_heads--;
                return num_heads > 0;
                        if (!synchronize(release_heads[i], act))
                                num_heads--;
                return num_heads > 0;


@@ -699,25 +699,25 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        ModelVector<ModelAction *> * rf_set = NULL;
        /* Build may_read_from set for newly-created actions */
        if (newly_explored && curr->is_read())
        ModelVector<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);
+               rf_set = build_may_read_from(curr);

 
        process_thread_action(curr);
 
        process_thread_action(curr);

-       
+

        if (curr->is_read() && !second_part_of_rmw) {
        if (curr->is_read() && !second_part_of_rmw) {

-         process_read(curr, rf_set);
-         delete rf_set;
+               process_read(curr, rf_set);
+               delete rf_set;

        } else {
        } else {

-         ASSERT(rf_set == NULL);
+               ASSERT(rf_set == NULL);

        }
        }

-       
+

        if (curr->is_write())
        if (curr->is_write())

-         process_write(curr);
-       
+               process_write(curr);
+

        if (curr->is_fence())
        if (curr->is_fence())

-         process_fence(curr);
-       
+               process_fence(curr);
+

        if (curr->is_mutex_op())
        if (curr->is_mutex_op())

-         process_mutex(curr);
+               process_mutex(curr);

 
        return curr;
 }
 
        return curr;
 }


@@ -729,7 +729,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
  */
 bool ModelExecution::isfeasibleprefix() const
 {
  */
 bool ModelExecution::isfeasibleprefix() const
 {

-  return !is_infeasible();
+       return !is_infeasible();

 }
 
 /**
 }
 
 /**


@@ -760,8 +760,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 bool ModelExecution::is_infeasible() const
 {
        return mo_graph->checkForCycles() ||
 bool ModelExecution::is_infeasible() const
 {
        return mo_graph->checkForCycles() ||

-               priv->bad_synchronization ||
-         priv->bad_sc_read;
+                                priv->bad_synchronization ||
+                                priv->bad_sc_read;

 }
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 }
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */


@@ -769,7 +769,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
        ModelAction *lastread = get_last_action(act->get_tid());
        lastread->process_rmw(act);
        if (act->is_rmw()) {
        ModelAction *lastread = get_last_action(act->get_tid());
        lastread->process_rmw(act);
        if (act->is_rmw()) {

-         mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+               mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);

                mo_graph->commitChanges();
        }
        return lastread;
                mo_graph->commitChanges();
        }
        return lastread;


@@ -806,7 +806,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                last_sc_write = get_last_seq_cst_write(curr);
 
        /* Iterate over all threads */
                last_sc_write = get_last_seq_cst_write(curr);
 
        /* Iterate over all threads */

-       for (i = 0; i < thrd_lists->size(); i++) {
+       for (i = 0;i < thrd_lists->size();i++) {

                /* Last SC fence in thread i */
                ModelAction *last_sc_fence_thread_local = NULL;
                if (int_to_id((int)i) != curr->get_tid())
                /* Last SC fence in thread i */
                ModelAction *last_sc_fence_thread_local = NULL;
                if (int_to_id((int)i) != curr->get_tid())


@@ -820,7 +820,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
                /* 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++) {
+               for (rit = list->rbegin();rit != list->rend();rit++) {

                        ModelAction *act = *rit;
 
                        /* Skip curr */
                        ModelAction *act = *rit;
 
                        /* Skip curr */


@@ -843,13 +843,13 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                                }
                                /* C++, Section 29.3 statement 4 */
                                else if (act->is_seqcst() && last_sc_fence_local &&
                                }
                                /* C++, Section 29.3 statement 4 */
                                else if (act->is_seqcst() && last_sc_fence_local &&

-                                               *act < *last_sc_fence_local) {
+                                                                *act < *last_sc_fence_local) {

                                        added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }
                                /* C++, Section 29.3 statement 6 */
                                else if (last_sc_fence_thread_before &&
                                        added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }
                                /* C++, Section 29.3 statement 6 */
                                else if (last_sc_fence_thread_before &&

-                                               *act < *last_sc_fence_thread_before) {
+                                                                *act < *last_sc_fence_thread_before) {

                                        added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }
                                        added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }


@@ -865,7 +865,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        if (!prevrf->equals(rf))
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        if (!prevrf->equals(rf))

-                                         added = mo_graph->addEdge(prevrf, rf) || added;
+                                               added = mo_graph->addEdge(prevrf, rf) || added;

                                }
                                break;
                        }
                                }
                                break;
                        }


@@ -908,7 +908,7 @@ bool ModelExecution::w_modification_order(ModelAction *curr)
 
        if (curr->is_seqcst()) {
                /* We have to at least see the last sequentially consistent write,
 
        if (curr->is_seqcst()) {
                /* We have to at least see the last sequentially consistent write,

-                        so we are initialized. */
+                        so we are initialized. */

                ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
                if (last_seq_cst != NULL) {
                        added = mo_graph->addEdge(last_seq_cst, curr) || added;
                ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
                if (last_seq_cst != NULL) {
                        added = mo_graph->addEdge(last_seq_cst, curr) || added;


@@ -919,7 +919,7 @@ bool ModelExecution::w_modification_order(ModelAction *curr)
        ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 
        /* Iterate over all threads */
        ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 
        /* Iterate over all threads */

-       for (i = 0; i < thrd_lists->size(); i++) {
+       for (i = 0;i < thrd_lists->size();i++) {

                /* Last SC fence in thread i, before last SC fence in current thread */
                ModelAction *last_sc_fence_thread_before = NULL;
                if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
                /* Last SC fence in thread i, before last SC fence in current thread */
                ModelAction *last_sc_fence_thread_before = NULL;
                if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())


@@ -928,7 +928,7 @@ bool ModelExecution::w_modification_order(ModelAction *curr)
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
                /* 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++) {
+               for (rit = list->rbegin();rit != list->rend();rit++) {

                        ModelAction *act = *rit;
                        if (act == curr) {
                                /*
                        ModelAction *act = *rit;
                        if (act == curr) {
                                /*


@@ -973,11 +973,11 @@ bool ModelExecution::w_modification_order(ModelAction *curr)
                                        added = mo_graph->addEdge(act, curr) || added;
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
                                        added = mo_graph->addEdge(act, curr) || added;
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going

-                                 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+                                       added = mo_graph->addEdge(act->get_reads_from(), curr) || added;

                                }
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&
                                }
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&

-                                                    !act->same_thread(curr)) {
+                                                                !act->same_thread(curr)) {

                                /* We have an action that:
                                   (1) did not happen before us
                                   (2) is a read and we are a write
                                /* We have an action that:
                                   (1) did not happen before us
                                   (2) is a read and we are a write


@@ -1011,13 +1011,13 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
        unsigned int i;
        /* Iterate over all threads */
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
        unsigned int i;
        /* Iterate over all threads */

-       for (i = 0; i < thrd_lists->size(); i++) {
+       for (i = 0;i < thrd_lists->size();i++) {

                const ModelAction *write_after_read = NULL;
 
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
                const ModelAction *write_after_read = NULL;
 
                /* 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++) {
+               for (rit = list->rbegin();rit != list->rend();rit++) {

                        ModelAction *act = *rit;
 
                        /* Don't disallow due to act == reader */
                        ModelAction *act = *rit;
 
                        /* Don't disallow due to act == reader */


@@ -1056,13 +1056,13 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *
  * false otherwise
  */
 bool ModelExecution::release_seq_heads(const ModelAction *rf,
  * false otherwise
  */
 bool ModelExecution::release_seq_heads(const ModelAction *rf,

-               rel_heads_list_t *release_heads) const
+                                                                                                                                                        rel_heads_list_t *release_heads) const

 {
        /* Only check for release sequences if there are no cycles */
        if (mo_graph->checkForCycles())
                return false;
 
 {
        /* Only check for release sequences if there are no cycles */
        if (mo_graph->checkForCycles())
                return false;
 

-       for ( ; rf != NULL; rf = rf->get_reads_from()) {
+       for ( ;rf != NULL;rf = rf->get_reads_from()) {

                ASSERT(rf->is_write());
 
                if (rf->is_release())
                ASSERT(rf->is_write());
 
                if (rf->is_release())


@@ -1070,7 +1070,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf,
                else if (rf->get_last_fence_release())
                        release_heads->push_back(rf->get_last_fence_release());
                if (!rf->is_rmw())
                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 */
+                       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
 
                /** @todo Need to be smarter here...  In the linux lock
                 * example, this will run to the beginning of the program for


@@ -1081,12 +1081,12 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf,
 
                /* acq_rel RMW is a sufficient stopping condition */
                if (rf->is_acquire() && rf->is_release())
 
                /* acq_rel RMW is a sufficient stopping condition */
                if (rf->is_acquire() && rf->is_release())

-                       return true; /* complete */
+                       return true;                                                                    /* complete */

        };
        };

-       ASSERT(rf); // Needs to be real write
+       ASSERT(rf);                             // Needs to be real write

 
        if (rf->is_release())
 
        if (rf->is_release())

-               return true; /* complete */
+               return true;                                            /* complete */

 
        /* else relaxed write
         * - check for fence-release in the same thread (29.8, stmt. 3)
 
        /* else relaxed write
         * - check for fence-release in the same thread (29.8, stmt. 3)


@@ -1099,7 +1099,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf,
        if (fence_release)
                release_heads->push_back(fence_release);
 
        if (fence_release)
                release_heads->push_back(fence_release);
 

-       return true; /* complete */
+       return true;                    /* complete */

 }
 
 /**
 }
 
 /**


@@ -1120,7 +1120,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf,
  * @see ModelExecution::release_seq_heads
  */
 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
  * @see ModelExecution::release_seq_heads
  */
 void ModelExecution::get_release_seq_heads(ModelAction *acquire,

-               ModelAction *read, rel_heads_list_t *release_heads)
+                                                                                                                                                                        ModelAction *read, rel_heads_list_t *release_heads)

 {
        const ModelAction *rf = read->get_reads_from();
 
 {
        const ModelAction *rf = read->get_reads_from();
 


@@ -1223,10 +1223,10 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
        action_list_t *list = obj_map.get(location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        action_list_t *list = obj_map.get(location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;

-       for (rit = list->rbegin(); (*rit) != curr; rit++)
+       for (rit = list->rbegin();(*rit) != curr;rit++)

                ;
                ;

-       rit++; /* Skip past curr */
-       for ( ; rit != list->rend(); rit++)
+       rit++;                  /* Skip past curr */
+       for ( ;rit != list->rend();rit++)

                if ((*rit)->is_write() && (*rit)->is_seqcst())
                        return *rit;
        return NULL;
                if ((*rit)->is_write() && (*rit)->is_seqcst())
                        return *rit;
        return NULL;


@@ -1251,7 +1251,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode
        action_list_t::reverse_iterator rit = list->rbegin();
 
        if (before_fence) {
        action_list_t::reverse_iterator rit = list->rbegin();
 
        if (before_fence) {

-               for (; rit != list->rend(); rit++)
+               for (;rit != list->rend();rit++)

                        if (*rit == before_fence)
                                break;
 
                        if (*rit == before_fence)
                                break;
 


@@ -1259,7 +1259,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode
                rit++;
        }
 
                rit++;
        }
 

-       for (; rit != list->rend(); rit++)
+       for (;rit != list->rend();rit++)

                if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
                        return *rit;
        return NULL;
                if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
                        return *rit;
        return NULL;


@@ -1280,7 +1280,7 @@ ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
        action_list_t *list = obj_map.get(location);
        /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        action_list_t *list = obj_map.get(location);
        /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;

-       for (rit = list->rbegin(); rit != list->rend(); rit++)
+       for (rit = list->rbegin();rit != list->rend();rit++)

                if ((*rit)->is_unlock() || (*rit)->is_wait())
                        return *rit;
        return NULL;
                if ((*rit)->is_unlock() || (*rit)->is_wait())
                        return *rit;
        return NULL;


@@ -1305,19 +1305,19 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const
 }
 
 bool valequals(uint64_t val1, uint64_t val2, int size) {
 }
 
 bool valequals(uint64_t val1, uint64_t val2, int size) {

-  switch(size) {
-  case 1:
-    return ((uint8_t)val1) == ((uint8_t)val2);
-  case 2:
-    return ((uint16_t)val1) == ((uint16_t)val2);
-  case 4:
-    return ((uint32_t)val1) == ((uint32_t)val2);
-  case 8:
-    return val1==val2;
-  default:
-    ASSERT(0);
-    return false;
-  }
+       switch(size) {
+       case 1:
+               return ((uint8_t)val1) == ((uint8_t)val2);
+       case 2:
+               return ((uint16_t)val1) == ((uint16_t)val2);
+       case 4:
+               return ((uint32_t)val1) == ((uint32_t)val2);
+       case 8:
+               return val1==val2;
+       default:
+               ASSERT(0);
+               return false;
+       }

 }
 
 /**
 }
 
 /**


@@ -1339,13 +1339,13 @@ ModelVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *c
                last_sc_write = get_last_seq_cst_write(curr);
 
        ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();
                last_sc_write = get_last_seq_cst_write(curr);
 
        ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();

-       
+

        /* Iterate over all threads */
        /* Iterate over all threads */

-       for (i = 0; i < thrd_lists->size(); i++) {
+       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;
                /* 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++) {
+               for (rit = list->rbegin();rit != list->rend();rit++) {

                        ModelAction *act = *rit;
 
                        /* Only consider 'write' actions */
                        ModelAction *act = *rit;
 
                        /* Only consider 'write' actions */


@@ -1360,24 +1360,24 @@ ModelVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *c
 
                        /* Need to check whether we will have two RMW reading from the same value */
                        if (curr->is_rmwr()) {
 
                        /* Need to check whether we will have two RMW reading from the same value */
                        if (curr->is_rmwr()) {

-                         /* It is okay if we have a failing CAS */
-                         if (!curr->is_rmwrcas() ||
-                             valequals(curr->get_value(), act->get_value(), curr->getSize())) {
-                               //Need to make sure we aren't the second RMW
-                               CycleNode * node = mo_graph->getNode_noCreate(act);
-                               if (node != NULL && node->getRMW() != NULL) {
-                                 //we are the second RMW
-                                 allow_read = false;
+                               /* It is okay if we have a failing CAS */
+                               if (!curr->is_rmwrcas() ||
+                                               valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+                                       //Need to make sure we aren't the second RMW
+                                       CycleNode * node = mo_graph->getNode_noCreate(act);
+                                       if (node != NULL && node->getRMW() != NULL) {
+                                               //we are the second RMW
+                                               allow_read = false;
+                                       }

                                }
                                }

-                             }

                        }
                        }

-                       
+

                        if (allow_read) {
                                /* Only add feasible reads */
                                mo_graph->startChanges();
                                r_modification_order(curr, act);
                                if (!is_infeasible())
                        if (allow_read) {
                                /* Only add feasible reads */
                                mo_graph->startChanges();
                                r_modification_order(curr, act);
                                if (!is_infeasible())

-                                 rf_set->push_back(act);
+                                       rf_set->push_back(act);

                                mo_graph->rollbackChanges();
                        }
 
                                mo_graph->rollbackChanges();
                        }
 


@@ -1425,7 +1425,7 @@ static void print_list(const action_list_t *list)
 
        unsigned int hash = 0;
 
 
        unsigned int hash = 0;
 

-       for (it = list->begin(); it != list->end(); it++) {
+       for (it = list->begin();it != list->end();it++) {

                const ModelAction *act = *it;
                if (act->get_seq_number() > 0)
                        act->print();
                const ModelAction *act = *it;
                if (act->get_seq_number() > 0)
                        act->print();


@@ -1445,20 +1445,20 @@ void ModelExecution::dumpGraph(char *filename) const
        mo_graph->dumpNodes(file);
        ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 
        mo_graph->dumpNodes(file);
        ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 

-       for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
+       for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {

                ModelAction *act = *it;
                if (act->is_read()) {
                        mo_graph->dot_print_node(file, act);
                        mo_graph->dot_print_edge(file,
                ModelAction *act = *it;
                if (act->is_read()) {
                        mo_graph->dot_print_node(file, act);
                        mo_graph->dot_print_edge(file,

-                                               act->get_reads_from(),
-                                               act,
-                                               "label=\"rf\", color=red, weight=2");
+                                                                                                                        act->get_reads_from(),
+                                                                                                                        act,
+                                                                                                                        "label=\"rf\", color=red, weight=2");

                }
                if (thread_array[act->get_tid()]) {
                        mo_graph->dot_print_edge(file,
                }
                if (thread_array[act->get_tid()]) {
                        mo_graph->dot_print_edge(file,

-                                       thread_array[id_to_int(act->get_tid())],
-                                       act,
-                                       "label=\"sb\", color=blue, weight=400");
+                                                                                                                        thread_array[id_to_int(act->get_tid())],
+                                                                                                                        act,
+                                                                                                                        "label=\"sb\", color=blue, weight=400");

                }
 
                thread_array[act->get_tid()] = act;
                }
 
                thread_array[act->get_tid()] = act;


@@ -1539,14 +1539,14 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const
  * @return A Thread reference
  */
 Thread * ModelExecution::get_pthread(pthread_t pid) {
  * @return A Thread reference
  */
 Thread * ModelExecution::get_pthread(pthread_t pid) {

-  union {
-    pthread_t p;
-    uint32_t v;
-  } x;
-  x.p = pid;
-  uint32_t thread_id = x.v;
-  if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
-        else return NULL;
+       union {
+               pthread_t p;
+               uint32_t v;
+       } x;
+       x.p = pid;
+       uint32_t thread_id = x.v;
+       if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
+       else return NULL;

 }
 
 /**
 }
 
 /**


@@ -1586,21 +1586,21 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons
        if (curr->is_rmwr())
                return get_thread(curr);
        if (curr->is_write()) {
        if (curr->is_rmwr())
                return get_thread(curr);
        if (curr->is_write()) {

-               std::memory_order order = curr->get_mo(); 
+               std::memory_order order = curr->get_mo();

                switch(order) {
                switch(order) {

-                       case std::memory_order_relaxed: 
-                               return get_thread(curr);
-                       case std::memory_order_release:
-                               return get_thread(curr);
-                       default:
-                               return NULL;
-               }       
+               case std::memory_order_relaxed:
+                       return get_thread(curr);
+               case std::memory_order_release:
+                       return get_thread(curr);
+               default:
+                       return NULL;
+               }

        }
 
        /* Follow CREATE with the created thread */
        /* which is not needed, because model.cc takes care of this */
        if (curr->get_type() == THREAD_CREATE)
        }
 
        /* Follow CREATE with the created thread */
        /* which is not needed, because model.cc takes care of this */
        if (curr->get_type() == THREAD_CREATE)

-               return curr->get_thread_operand(); 
+               return curr->get_thread_operand();

        if (curr->get_type() == PTHREAD_CREATE) {
                return curr->get_thread_operand();
        }
        if (curr->get_type() == PTHREAD_CREATE) {
                return curr->get_thread_operand();
        }


@@ -1618,7 +1618,7 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        Thread *curr_thrd = get_thread(curr);
        ASSERT(curr_thrd->get_state() == THREAD_READY);
 
        Thread *curr_thrd = get_thread(curr);
        ASSERT(curr_thrd->get_state() == THREAD_READY);
 

-       ASSERT(check_action_enabled(curr)); /* May have side effects? */
+       ASSERT(check_action_enabled(curr));                             /* May have side effects? */

        curr = check_current_action(curr);
        ASSERT(curr);
 
        curr = check_current_action(curr);
        ASSERT(curr);
 


@@ -1629,5 +1629,5 @@ Thread * ModelExecution::take_step(ModelAction *curr)
 }
 
 Fuzzer * ModelExecution::getFuzzer() {
 }
 
 Fuzzer * ModelExecution::getFuzzer() {

-  return fuzzer;
+       return fuzzer;

 }
 }

diff --git a/execution.h b/execution.h
index 737477fea7fc2ddb8871e9c34b873bf854c5c526..9ad7469af605755094d7213b7118396c42b7c5d3 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -52,13 +52,13 @@ struct release_seq {
 class ModelExecution {
 public:
        ModelExecution(ModelChecker *m,
 class ModelExecution {
 public:
        ModelExecution(ModelChecker *m,

-                       Scheduler *scheduler,
-                       NodeStack *node_stack);
+                                                                Scheduler *scheduler,
+                                                                NodeStack *node_stack);

        ~ModelExecution();
 
        struct model_params * get_params() const { return params; }
        void setParams(struct model_params * _params) {params = _params;}
        ~ModelExecution();
 
        struct model_params * get_params() const { return params; }
        void setParams(struct model_params * _params) {params = _params;}

-  
+

        Thread * take_step(ModelAction *curr);
 
        void print_summary() const;
        Thread * take_step(ModelAction *curr);
 
        void print_summary() const;


@@ -102,18 +102,18 @@ public:
        bool is_deadlocked() const;
 
        action_list_t * get_action_trace() { return &action_trace; }
        bool is_deadlocked() const;
 
        action_list_t * get_action_trace() { return &action_trace; }

-  Fuzzer * getFuzzer();
+       Fuzzer * getFuzzer();

        CycleGraph * const get_mo_graph() { return mo_graph; }
        CycleGraph * const get_mo_graph() { return mo_graph; }

-  HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
-  HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
-  
+       HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
+       HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
+

        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
 
        ModelChecker *model;
 
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
 
        ModelChecker *model;
 

-  struct model_params * params;
+       struct model_params * params;

 
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler * const scheduler;
 
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler * const scheduler;


@@ -128,7 +128,7 @@ private:
        bool next_execution();
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool next_execution();
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);

-  bool process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set);
+       bool process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set);

        bool process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        bool process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);


@@ -142,7 +142,7 @@ 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;
        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;

-  ModelVector<ModelAction *> * build_may_read_from(ModelAction *curr);
+       ModelVector<ModelAction *> * build_may_read_from(ModelAction *curr);

        ModelAction * process_rmw(ModelAction *curr);
 
        template <typename rf_type>
        ModelAction * process_rmw(ModelAction *curr);
 
        template <typename rf_type>


@@ -150,13 +150,13 @@ private:
 
        bool w_modification_order(ModelAction *curr);
        void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
 
        bool 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;
+       bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;

        ModelAction * get_uninitialized_action(const ModelAction *curr) const;
 
        action_list_t action_trace;
        SnapVector<Thread *> thread_map;
        SnapVector<Thread *> pthread_map;
        ModelAction * get_uninitialized_action(const ModelAction *curr) const;
 
        action_list_t action_trace;
        SnapVector<Thread *> thread_map;
        SnapVector<Thread *> pthread_map;

-  uint32_t pthread_counter;
+       uint32_t pthread_counter;

 
        /** Per-object list of actions. Maps an object (i.e., memory location)
         * to a trace of all actions performed on the object. */
 
        /** Per-object list of actions. Maps an object (i.e., memory location)
         * to a trace of all actions performed on the object. */


@@ -168,7 +168,7 @@ private:
 
        HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
 
 
        HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
 

-  HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
+       HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;

        HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
 
        /**
        HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
 
        /**


@@ -206,9 +206,9 @@ private:
         */
        CycleGraph * const mo_graph;
 
         */
        CycleGraph * const mo_graph;
 

-  Fuzzer * fuzzer;
-  
+       Fuzzer * fuzzer;
+

        Thread * action_select_next_thread(const ModelAction *curr) const;
 };
 
        Thread * action_select_next_thread(const ModelAction *curr) const;
 };
 

-#endif /* __EXECUTION_H__ */
+#endif/* __EXECUTION_H__ */

diff --git a/futex.cc b/futex.cc
index fa32e9a28d4a4bbab28dee48813dc15ea42d58f1..ce130446f8455f19e6adfe6e7512311e5e7b7def 100644 (file)
--- a/futex.cc
+++ b/futex.cc
@@ -2,7 +2,7 @@
 
 // Copyright (C) 2015-2019 Free Software Foundation, Inc.
 //
 
 // Copyright (C) 2015-2019 Free Software Foundation, Inc.
 //

-// This is a reimplementation of libstdc++-v3/src/c++11/futex.cc. 
+// This is a reimplementation of libstdc++-v3/src/c++11/futex.cc.

 
 #include <bits/atomic_futex.h>
 #ifdef _GLIBCXX_HAS_GTHREADS
 
 #include <bits/atomic_futex.h>
 #ifdef _GLIBCXX_HAS_GTHREADS


@@ -26,19 +26,19 @@ const unsigned futex_wake_op = 1;
 
 namespace std _GLIBCXX_VISIBILITY(default)
 {
 
 namespace std _GLIBCXX_VISIBILITY(default)
 {

-_GLIBCXX_BEGIN_NAMESPACE_VERSION
+       _GLIBCXX_BEGIN_NAMESPACE_VERSION

 
        bool
        __atomic_futex_unsigned_base::_M_futex_wait_until(unsigned *__addr,
 
        bool
        __atomic_futex_unsigned_base::_M_futex_wait_until(unsigned *__addr,

-               unsigned __val,
-               bool __has_timeout, chrono::seconds __s, chrono::nanoseconds __ns)
+                                                                                                                                                                                                               unsigned __val,
+                                                                                                                                                                                                               bool __has_timeout, chrono::seconds __s, chrono::nanoseconds __ns)

        {
                // do nothing if the two values are not equal
                if ( *__addr != __val ) {
                        return true;
                }
 
        {
                // do nothing if the two values are not equal
                if ( *__addr != __val ) {
                        return true;
                }
 

-               // if a timeout is specified, return immedialy. Letting the scheduler decide how long this thread will wait.  
+               // if a timeout is specified, return immedialy. Letting the scheduler decide how long this thread will wait.

                if (__has_timeout) {
                        return true;
                }
                if (__has_timeout) {
                        return true;
                }


@@ -64,7 +64,7 @@ _GLIBCXX_BEGIN_NAMESPACE_VERSION
                v->notify_all();
        }
 
                v->notify_all();
        }
 

-_GLIBCXX_END_NAMESPACE_VERSION
+       _GLIBCXX_END_NAMESPACE_VERSION

 }
 }

-#endif // defined(_GLIBCXX_HAVE_LINUX_FUTEX) && ATOMIC_INT_LOCK_FREE > 1
-#endif // _GLIBCXX_HAS_GTHREADS
+#endif// defined(_GLIBCXX_HAVE_LINUX_FUTEX) && ATOMIC_INT_LOCK_FREE > 1
+#endif// _GLIBCXX_HAS_GTHREADS

diff --git a/fuzzer.cc b/fuzzer.cc
index 550a0a16210e1c016315c97dd1f47c2601ddbdba..d3d9d2c52059ae87b2097f227a175856aac9a9e4 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -4,23 +4,23 @@
 #include "model.h"
 
 int Fuzzer::selectWrite(ModelAction *read, ModelVector<ModelAction *> * rf_set) {
 #include "model.h"
 
 int Fuzzer::selectWrite(ModelAction *read, ModelVector<ModelAction *> * rf_set) {

-  int random_index = random() % rf_set->size();
-  return random_index;
+       int random_index = random() % rf_set->size();
+       return random_index;

 }
 
 Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) {
 }
 
 Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) {

-  int random_index = random() % numthreads;
-  int thread = threadlist[random_index];
-  thread_id_t curr_tid = int_to_id(thread);
-  return model->get_thread(curr_tid);
+       int random_index = random() % numthreads;
+       int thread = threadlist[random_index];
+       thread_id_t curr_tid = int_to_id(thread);
+       return model->get_thread(curr_tid);

 }
 
 Thread * Fuzzer::selectNotify(action_list_t * waiters) {
 }
 
 Thread * Fuzzer::selectNotify(action_list_t * waiters) {

-  int numwaiters = waiters->size();
-  int random_index = random() % numwaiters;
-  action_list_t::iterator it = waiters->begin();
-  advance(it, random_index);
-  Thread *thread = model->get_thread(*it);
-  waiters->erase(it);
-  return thread;
+       int numwaiters = waiters->size();
+       int random_index = random() % numwaiters;
+       action_list_t::iterator it = waiters->begin();
+       advance(it, random_index);
+       Thread *thread = model->get_thread(*it);
+       waiters->erase(it);
+       return thread;

 }
 }

diff --git a/fuzzer.h b/fuzzer.h
index a6318d04ff941aada044e7a81f757c1185c56ea1..3a84351067690a66463a8651d260d8950cc269c8 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -6,11 +6,11 @@
 
 class Fuzzer {
 public:
 
 class Fuzzer {
 public:

-  Fuzzer() {}
-  int selectWrite(ModelAction *read, ModelVector<ModelAction *>* rf_set);
-  Thread * selectThread(Node *n, int * threadlist, int numthreads);
-  Thread * selectNotify(action_list_t * waiters);
-  MEMALLOC
+       Fuzzer() {}
+       int selectWrite(ModelAction *read, ModelVector<ModelAction *>* rf_set);
+       Thread * selectThread(Node *n, int * threadlist, int numthreads);
+       Thread * selectNotify(action_list_t * waiters);
+       MEMALLOC

 private:
 };
 #endif
 private:
 };
 #endif

diff --git a/hashtable.h b/hashtable.h
index 2802eabead5af4f48ec49196a21ad34edfe1fa1a..22c9022135a1b0bf85183b402b9cc0a5cb984e15 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -45,7 +45,7 @@ struct hashlistnode {
  */
 template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free>
 class HashTable {
  */
 template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free>
 class HashTable {

- public:
+public:

        /**
         * @brief Hash table constructor
         * @param initialcapacity Sets the initial capacity of the hash table.
        /**
         * @brief Hash table constructor
         * @param initialcapacity Sets the initial capacity of the hash table.


@@ -61,7 +61,7 @@ class HashTable {
                capacitymask = initialcapacity - 1;
 
                threshold = (unsigned int)(initialcapacity * loadfactor);
                capacitymask = initialcapacity - 1;
 
                threshold = (unsigned int)(initialcapacity * loadfactor);

-               size = 0; // Initial number of elements in the hash
+               size = 0;                                                       // Initial number of elements in the hash

        }
 
        /** @brief Hash table destructor */
        }
 
        /** @brief Hash table destructor */


@@ -183,7 +183,7 @@ class HashTable {
                        exit(EXIT_FAILURE);
                }
 
                        exit(EXIT_FAILURE);
                }
 

-               table = newtable;          // Update the global hashtable upon resize()
+               table = newtable;                                                                                       // Update the global hashtable upon resize()

                capacity = newsize;
                capacitymask = newsize - 1;
 
                capacity = newsize;
                capacitymask = newsize - 1;
 


@@ -191,7 +191,7 @@ class HashTable {
 
                struct hashlistnode<_Key, _Val> *bin = &oldtable[0];
                struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity];
 
                struct hashlistnode<_Key, _Val> *bin = &oldtable[0];
                struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity];

-               for (; bin < lastbin; bin++) {
+               for (;bin < lastbin;bin++) {

                        _Key key = bin->key;
 
                        struct hashlistnode<_Key, _Val> *search;
                        _Key key = bin->key;
 
                        struct hashlistnode<_Key, _Val> *search;


@@ -207,10 +207,10 @@ class HashTable {
                        search->val = bin->val;
                }
 
                        search->val = bin->val;
                }
 

-               _free(oldtable);            // Free the memory of the old hash table
+               _free(oldtable);                                                                                                // Free the memory of the old hash table

        }
 
        }
 

- private:
+private:

        struct hashlistnode<_Key, _Val> *table;
        unsigned int capacity;
        unsigned int size;
        struct hashlistnode<_Key, _Val> *table;
        unsigned int capacity;
        unsigned int size;


@@ -219,4 +219,4 @@ class HashTable {
        double loadfactor;
 };
 
        double loadfactor;
 };
 

-#endif /* __HASHTABLE_H__ */
+#endif/* __HASHTABLE_H__ */

diff --git a/impatomic.cc b/impatomic.cc
index 4b5d1c28941246fe1c0a1e2dc1567e4bac22a81e..a25518030544acde77e682aaf6938ad4852265c1 100644 (file)
--- a/impatomic.cc
+++ b/impatomic.cc
@@ -17,7 +17,7 @@ bool atomic_flag_test_and_set( volatile atomic_flag* __a__ )
 { return atomic_flag_test_and_set_explicit( __a__, memory_order_seq_cst ); }
 
 void atomic_flag_clear_explicit
 { return atomic_flag_test_and_set_explicit( __a__, memory_order_seq_cst ); }
 
 void atomic_flag_clear_explicit

-( volatile atomic_flag* __a__, memory_order __x__ )
+       ( volatile atomic_flag* __a__, memory_order __x__ )

 {
        volatile bool * __p__ = &((__a__)->__f__);
        model->switch_to_master(new ModelAction(ATOMIC_WRITE, __x__, (void *) __p__, false));
 {
        volatile bool * __p__ = &((__a__)->__f__);
        model->switch_to_master(new ModelAction(ATOMIC_WRITE, __x__, (void *) __p__, false));


@@ -26,13 +26,13 @@ void atomic_flag_clear_explicit
 void atomic_flag_clear( volatile atomic_flag* __a__ )
 { atomic_flag_clear_explicit( __a__, memory_order_seq_cst ); }
 
 void atomic_flag_clear( volatile atomic_flag* __a__ )
 { atomic_flag_clear_explicit( __a__, memory_order_seq_cst ); }
 

-void __atomic_flag_wait__( volatile atomic_flag* __a__ ) { 
+void __atomic_flag_wait__( volatile atomic_flag* __a__ ) {

        while ( atomic_flag_test_and_set( __a__ ) )
        while ( atomic_flag_test_and_set( __a__ ) )

-               ; 
+               ;

 }
 
 void __atomic_flag_wait_explicit__( volatile atomic_flag* __a__,
 }
 
 void __atomic_flag_wait_explicit__( volatile atomic_flag* __a__,

-                                    memory_order __x__ ) {
+                                                                                                                                               memory_order __x__ ) {

        while ( atomic_flag_test_and_set_explicit( __a__, __x__ ))
                ;
 }
        while ( atomic_flag_test_and_set_explicit( __a__, __x__ ))
                ;
 }

diff --git a/librace.cc b/librace.cc
index b7836278477596c9d673e20e1183e8fcffad674a..a9bb7052ebca835ae5fc0fd69cf212cdb410f983 100644 (file)
--- a/librace.cc
+++ b/librace.cc
@@ -96,18 +96,18 @@ uint64_t load_64(const void *addr)
 // helper functions used by CdsPass
 // The CdsPass implementation does not replace normal load/stores with cds load/stores,
 // but inserts cds load/stores to check dataraces. Thus, the cds load/stores do not
 // helper functions used by CdsPass
 // The CdsPass implementation does not replace normal load/stores with cds load/stores,
 // but inserts cds load/stores to check dataraces. Thus, the cds load/stores do not

-// return anything. 
+// return anything.

 
 void cds_store8(void *addr)
 {
 
 void cds_store8(void *addr)
 {

-  //DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
+       //DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);

        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
 }
 
 void cds_store16(void *addr)
 {
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
 }
 
 void cds_store16(void *addr)
 {

-  //DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
+       //DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);

        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));


@@ -115,7 +115,7 @@ void cds_store16(void *addr)
 
 void cds_store32(void *addr)
 {
 
 void cds_store32(void *addr)
 {

-  //DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
+       //DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);

        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));


@@ -125,7 +125,7 @@ void cds_store32(void *addr)
 
 void cds_store64(void *addr)
 {
 
 void cds_store64(void *addr)
 {

-  //DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
+       //DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);

        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));

diff --git a/main.cc b/main.cc
index 1e5ad1662c9c2872639ba8e53ad866969ccb65ad..9375ac0d80e0a86aa72014d75972b712704372b2 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -31,30 +31,30 @@ static void print_usage(const char *program_name, struct model_params *params)
        param_defaults(params);
 
        model_print(
        param_defaults(params);
 
        model_print(

-"Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
-"Distributed under the GPLv2\n"
-"Written by Brian Norris and Brian Demsky\n"
-"\n"
-"Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
-"\n"
-"MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
-"provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
-"\n"
-"Model-checker options:\n"
-"-h, --help                  Display this help message and exit\n"
-"-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
-"                              0 is quiet; 1 shows valid executions; 2 is noisy;\n"
-"                              3 is noisier.\n"
-"                              Default: %d\n"
-"-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
-"                              uninitialized atomic.\n"
-"                              Default: %u\n"
-"-t, --analysis=NAME         Use Analysis Plugin.\n"
-"-o, --options=NAME          Option for previous analysis plugin.  \n"
-"-x, --maxexec=NUM           Maximum number of executions.\n"
-"                            Default: %u\n"
-"                            -o help for a list of options\n"
-" --                         Program arguments follow.\n\n",
+               "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
+               "Distributed under the GPLv2\n"
+               "Written by Brian Norris and Brian Demsky\n"
+               "\n"
+               "Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
+               "\n"
+               "MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
+               "provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
+               "\n"
+               "Model-checker options:\n"
+               "-h, --help                  Display this help message and exit\n"
+               "-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
+               "                              0 is quiet; 1 shows valid executions; 2 is noisy;\n"
+               "                              3 is noisier.\n"
+               "                              Default: %d\n"
+               "-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
+               "                              uninitialized atomic.\n"
+               "                              Default: %u\n"
+               "-t, --analysis=NAME         Use Analysis Plugin.\n"
+               "-o, --options=NAME          Option for previous analysis plugin.  \n"
+               "-x, --maxexec=NUM           Maximum number of executions.\n"
+               "                            Default: %u\n"
+               "                            -o help for a list of options\n"
+               " --                         Program arguments follow.\n\n",

                program_name,
                params->verbose,
                params->uninitvalue,
                program_name,
                params->verbose,
                params->uninitvalue,


@@ -92,7 +92,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                {"analysis", required_argument, NULL, 't'},
                {"options", required_argument, NULL, 'o'},
                {"maxexecutions", required_argument, NULL, 'x'},
                {"analysis", required_argument, NULL, 't'},
                {"options", required_argument, NULL, 'o'},
                {"maxexecutions", required_argument, NULL, 'x'},

-               {0, 0, 0, 0} /* Terminator */
+               {0, 0, 0, 0}                                            /* Terminator */

        };
        int opt, longindex;
        bool error = false;
        };
        int opt, longindex;
        bool error = false;


@@ -115,13 +115,13 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                                error = true;
                        break;
                case 'o':
                                error = true;
                        break;
                case 'o':

-                       {
-                               ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
-                               if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
-                                       error = true;
-                       }
-                       break;
-               default: /* '?' */
+               {
+                       ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
+                       if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
+                               error = true;
+               }
+               break;
+               default:                                                /* '?' */

                        error = true;
                        break;
                }
                        error = true;
                        break;
                }


@@ -172,7 +172,7 @@ static void model_main()
        snapshot_stack_init();
 
        if (!model)
        snapshot_stack_init();
 
        if (!model)

-         model = new ModelChecker();
+               model = new ModelChecker();

        model->setParams(params);
        install_trace_analyses(model->get_execution());
 
        model->setParams(params);
        install_trace_analyses(model->get_execution());
 

diff --git a/model.cc b/model.cc
index f5f20dd75dcc0147fd4f62ee200d7674bf2df6fe..1d55182db6fef9ffae6a8b6334b7f8ada58fecda 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -44,8 +44,8 @@ ModelChecker::~ModelChecker()
 
 /** Method to set parameters */
 void ModelChecker::setParams(struct model_params params) {
 
 /** Method to set parameters */
 void ModelChecker::setParams(struct model_params params) {

-  this->params = params;
-  execution->setParams(&params);
+       this->params = params;
+       execution->setParams(&params);

 }
 
 /**
 }
 
 /**


@@ -62,7 +62,7 @@ void ModelChecker::reset_to_initial_state()
         * those pending actions which were NOT pending before the rollback
         * point
         */
         * those pending actions which were NOT pending before the rollback
         * point
         */

-       for (unsigned int i = 0; i < get_num_threads(); i++)
+       for (unsigned int i = 0;i < get_num_threads();i++)

                delete get_thread(int_to_id(i))->get_pending();
 
        snapshot_backtrack_before(0);
                delete get_thread(int_to_id(i))->get_pending();
 
        snapshot_backtrack_before(0);


@@ -148,9 +148,9 @@ void ModelChecker::print_bugs() const
        SnapVector<bug_message *> *bugs = execution->get_bugs();
 
        model_print("Bug report: %zu bug%s detected\n",
        SnapVector<bug_message *> *bugs = execution->get_bugs();
 
        model_print("Bug report: %zu bug%s detected\n",

-                       bugs->size(),
-                       bugs->size() > 1 ? "s" : "");
-       for (unsigned int i = 0; i < bugs->size(); i++)
+                                                       bugs->size(),
+                                                       bugs->size() > 1 ? "s" : "");
+       for (unsigned int i = 0;i < bugs->size();i++)

                (*bugs)[i]->print();
 }
 
                (*bugs)[i]->print();
 }
 


@@ -198,7 +198,7 @@ void ModelChecker::print_stats() const
 void ModelChecker::print_execution(bool printbugs) const
 {
        model_print("Program output from execution %d:\n",
 void ModelChecker::print_execution(bool printbugs) const
 {
        model_print("Program output from execution %d:\n",

-                       get_execution_number());
+                                                       get_execution_number());

        print_program_output();
 
        if (params.verbose >= 3) {
        print_program_output();
 
        if (params.verbose >= 3) {


@@ -227,8 +227,8 @@ bool ModelChecker::next_execution()
        DBG();
        /* Is this execution a feasible execution that's worth bug-checking? */
        bool complete = execution->isfeasibleprefix() &&
        DBG();
        /* Is this execution a feasible execution that's worth bug-checking? */
        bool complete = execution->isfeasibleprefix() &&

-               (execution->is_complete_execution() ||
-                execution->have_bug_reports());
+                                                                       (execution->is_complete_execution() ||
+                                                                        execution->have_bug_reports());

 
        /* End-of-execution bug checks */
        if (complete) {
 
        /* End-of-execution bug checks */
        if (complete) {


@@ -237,7 +237,7 @@ bool ModelChecker::next_execution()
 
                checkDataRaces();
                run_trace_analyses();
 
                checkDataRaces();
                run_trace_analyses();

-       } 
+       }

 
        record_stats();
        /* Output */
 
        record_stats();
        /* Output */


@@ -259,7 +259,7 @@ bool ModelChecker::next_execution()
 
 /** @brief Run trace analyses on complete trace */
 void ModelChecker::run_trace_analyses() {
 
 /** @brief Run trace analyses on complete trace */
 void ModelChecker::run_trace_analyses() {

-       for (unsigned int i = 0; i < trace_analyses.size(); i++)
+       for (unsigned int i = 0;i < trace_analyses.size();i++)

                trace_analyses[i]->analyze(execution->get_action_trace());
 }
 
                trace_analyses[i]->analyze(execution->get_action_trace());
 }
 


@@ -314,9 +314,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
 /* W: No plugin
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
 /* W: No plugin

-       if (inspect_plugin != NULL) {
-               inspect_plugin->inspectModelAction(act); 
-       }*/
+        if (inspect_plugin != NULL) {
+                inspect_plugin->inspectModelAction(act);
+        }*/

        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");


@@ -366,9 +366,9 @@ void ModelChecker::run()
        char random_state[256];
        initstate(423121, random_state, sizeof(random_state));
 
        char random_state[256];
        initstate(423121, random_state, sizeof(random_state));
 

-       for(int exec = 0; exec < params.maxexecutions; exec++) {
+       for(int exec = 0;exec < params.maxexecutions;exec++) {

                thrd_t user_thread;
                thrd_t user_thread;

-               Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
+               Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL);                                                 // L: user_main_wrapper passes the user program

                execution->add_thread(t);
                //Need to seed random number generator, otherwise its state gets reset
                do {
                execution->add_thread(t);
                //Need to seed random number generator, otherwise its state gets reset
                do {


@@ -379,18 +379,18 @@ void ModelChecker::run()
                         * for any newly-created thread
                         */
 
                         * for any newly-created thread
                         */
 

-                       for (unsigned int i = 0; i < get_num_threads(); i++) {
+                       for (unsigned int i = 0;i < get_num_threads();i++) {

                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
                                if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
                                if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {

-                                       switch_from_master(thr);        // L: context swapped, and action type of thr changed. 
+                                       switch_from_master(thr);                                                                                                                                                        // L: context swapped, and action type of thr changed.

                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                }
                        }
 
                        /* Don't schedule threads which should be disabled */
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                }
                        }
 
                        /* Don't schedule threads which should be disabled */

-                       for (unsigned int i = 0; i < get_num_threads(); i++) {
+                       for (unsigned int i = 0;i < get_num_threads();i++) {

                                Thread *th = get_thread(int_to_id(i));
                                ModelAction *act = th->get_pending();
                                if (act && execution->is_enabled(th) && !execution->check_action_enabled(act)) {
                                Thread *th = get_thread(int_to_id(i));
                                ModelAction *act = th->get_pending();
                                if (act && execution->is_enabled(th) && !execution->check_action_enabled(act)) {


@@ -398,33 +398,33 @@ void ModelChecker::run()
                                }
                        }
 
                                }
                        }
 

-                       for (unsigned int i = 1; i < get_num_threads(); i++) {
+                       for (unsigned int i = 1;i < get_num_threads();i++) {

                                Thread *th = get_thread(int_to_id(i));
                                ModelAction *act = th->get_pending();
                                Thread *th = get_thread(int_to_id(i));
                                ModelAction *act = th->get_pending();

-                               if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ){
-                                       if (act->is_write()){
-                                               std::memory_order order = act->get_mo(); 
-                                               if (order == std::memory_order_relaxed || \
-                                                       order == std::memory_order_release) {
+                               if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ) {
+                                       if (act->is_write()) {
+                                               std::memory_order order = act->get_mo();
+                                               if (order == std::memory_order_relaxed || \
+                                                               order == std::memory_order_release) {

                                                        t = th;
                                                        break;
                                                }
                                        } else if (act->get_type() == THREAD_CREATE || \
                                                        t = th;
                                                        break;
                                                }
                                        } else if (act->get_type() == THREAD_CREATE || \

-                                                       act->get_type() == PTHREAD_CREATE || \
-                                                       act->get_type() == THREAD_START || \
-                                                       act->get_type() == THREAD_FINISH) {
+                                                                                act->get_type() == PTHREAD_CREATE || \
+                                                                                act->get_type() == THREAD_START || \
+                                                                                act->get_type() == THREAD_FINISH) {

                                                t = th;
                                                break;
                                                t = th;
                                                break;

-                                       }                               
+                                       }

                                }
                        }
 
                        /* Catch assertions from prior take_step or from
                                }
                        }
 
                        /* Catch assertions from prior take_step or from

-                        * between-ModelAction bugs (e.g., data races) */
+                       * between-ModelAction bugs (e.g., data races) */

 
                        if (execution->has_asserted())
                                break;
 
                        if (execution->has_asserted())
                                break;

-                       if (!t)                         
+                       if (!t)

                                t = get_next_thread();
                        if (!t || t->is_model_thread())
                                break;
                                t = get_next_thread();
                        if (!t || t->is_model_thread())
                                break;


@@ -443,6 +443,6 @@ void ModelChecker::run()
        print_stats();
 
        /* Have the trace analyses dump their output. */
        print_stats();
 
        /* Have the trace analyses dump their output. */

-       for (unsigned int i = 0; i < trace_analyses.size(); i++)
+       for (unsigned int i = 0;i < trace_analyses.size();i++)

                trace_analyses[i]->finish();
 }
                trace_analyses[i]->finish();
 }

diff --git a/model.h b/model.h
index 166eb12d21de204e9b69e5bfd0872d8f55cbab23..95fc6abebe752050dbeb81b0116ba6612ff3fa80 100644 (file)
--- a/model.h
+++ b/model.h
@@ -21,11 +21,11 @@ typedef SnapList<ModelAction *> action_list_t;
 
 /** @brief Model checker execution stats */
 struct execution_stats {
 
 /** @brief Model checker execution stats */
 struct execution_stats {

-       int num_total; /**< @brief Total number of executions */
-       int num_infeasible; /**< @brief Number of infeasible executions */
-       int num_buggy_executions; /** @brief Number of buggy executions */
-       int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
-       int num_redundant; /**< @brief Number of redundant, aborted executions */
+       int num_total;                  /**< @brief Total number of executions */
+       int num_infeasible;                             /**< @brief Number of infeasible executions */
+       int num_buggy_executions;                               /** @brief Number of buggy executions */
+       int num_complete;                               /**< @brief Number of feasible, non-buggy, complete executions */
+       int num_redundant;                      /**< @brief Number of redundant, aborted executions */

 };
 
 /** @brief The central structure for model-checking */
 };
 
 /** @brief The central structure for model-checking */


@@ -60,9 +60,9 @@ public:
        bool assert_bug(const char *msg, ...);
        void assert_user_bug(const char *msg);
 
        bool assert_bug(const char *msg, ...);
        void assert_user_bug(const char *msg);
 

-  model_params params;
-       void add_trace_analysis(TraceAnalysis *a) {     trace_analyses.push_back(a); }
-       void set_inspect_plugin(TraceAnalysis *a) {     inspect_plugin=a;       }
+       model_params params;
+       void add_trace_analysis(TraceAnalysis *a) {     trace_analyses.push_back(a); }
+       void set_inspect_plugin(TraceAnalysis *a) {     inspect_plugin=a;       }

        MEMALLOC
 private:
        /** Flag indicates whether to restart the model checker. */
        MEMALLOC
 private:
        /** Flag indicates whether to restart the model checker. */


@@ -104,4 +104,4 @@ private:
 
 extern ModelChecker *model;
 
 
 extern ModelChecker *model;
 

-#endif /* __MODEL_H__ */
+#endif/* __MODEL_H__ */

diff --git a/mutex.cc b/mutex.cc
index a431321e1aba9a11e1d7f56a630978d453ce3d6a..44f64ff764b3c0c80a2c789d4f5bfcff40a7ef1e 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -15,12 +15,12 @@ mutex::mutex()
        state.alloc_tid = tid;
        state.alloc_clock = model->get_execution()->get_cv(tid)->getClock(tid);
 }
        state.alloc_tid = tid;
        state.alloc_clock = model->get_execution()->get_cv(tid)->getClock(tid);
 }

-       
+

 void mutex::lock()
 {
        model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
 }
 void mutex::lock()
 {
        model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
 }

-       
+

 bool mutex::try_lock()
 {
        return model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
 bool mutex::try_lock()
 {
        return model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));

diff --git a/mymemory.cc b/mymemory.cc
index e8ec08050f5d8e5389c01e136fe1c0a27f374f13..eff66348e7b9cd0e71a5321fe8cf6b15d9397683 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -259,7 +259,7 @@ void operator delete[](void *p, size_t size)
        free(p);
 }
 
        free(p);
 }
 

-#else /* !USE_MPROTECT_SNAPSHOT */
+#else  /* !USE_MPROTECT_SNAPSHOT */

 
 /** @brief Snapshotting allocation function for use by the Thread class only */
 void * Thread_malloc(size_t size)
 
 /** @brief Snapshotting allocation function for use by the Thread class only */
 void * Thread_malloc(size_t size)


@@ -273,4 +273,4 @@ void Thread_free(void *ptr)
        free(ptr);
 }
 
        free(ptr);
 }
 

-#endif /* !USE_MPROTECT_SNAPSHOT */
+#endif/* !USE_MPROTECT_SNAPSHOT */

diff --git a/mymemory.h b/mymemory.h
index a62ab83b9ce5cbcd82999bc9463b2949ba7a0394..aaf54c395742dcb10a29f4027e04422d3b1bb0d5 100644 (file)
--- a/mymemory.h
+++ b/mymemory.h
@@ -24,7 +24,7 @@
        void operator delete[](void *p, size_t size) { \
                model_free(p); \
        } \
        void operator delete[](void *p, size_t size) { \
                model_free(p); \
        } \

-       void * operator new(size_t size, void *p) { /* placement new */ \
+       void * operator new(size_t size, void *p) {                             /* placement new */ \

                return p; \
        }
 
                return p; \
        }
 


@@ -43,7 +43,7 @@
        void operator delete[](void *p, size_t size) { \
                snapshot_free(p); \
        } \
        void operator delete[](void *p, size_t size) { \
                snapshot_free(p); \
        } \

-       void * operator new(size_t size, void *p) { /* placement new */ \
+       void * operator new(size_t size, void *p) {                             /* placement new */ \

                return p; \
        }
 
                return p; \
        }
 


@@ -71,15 +71,15 @@ void Thread_free(void *ptr);
  */
 template <class T>
 class ModelAlloc {
  */
 template <class T>
 class ModelAlloc {

- public:
+public:

        // type definitions
        // type definitions

-       typedef T        value_type;
+       typedef T value_type;

        typedef T*       pointer;
        typedef const T* const_pointer;
        typedef T&       reference;
        typedef const T& const_reference;
        typedef T*       pointer;
        typedef const T* const_pointer;
        typedef T&       reference;
        typedef const T& const_reference;

-       typedef size_t   size_type;
-       typedef size_t   difference_type;
+       typedef size_t size_type;
+       typedef size_t difference_type;

 
        // rebind allocator to type U
        template <class U>
 
        // rebind allocator to type U
        template <class U>


@@ -140,14 +140,14 @@ class ModelAlloc {
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator ==(const ModelAlloc<T1>&,
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator ==(const ModelAlloc<T1>&,

-               const ModelAlloc<T2>&) throw() {
+                                                                const ModelAlloc<T2>&) throw() {

        return true;
 }
 
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator!= (const ModelAlloc<T1>&,
        return true;
 }
 
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator!= (const ModelAlloc<T1>&,

-               const ModelAlloc<T2>&) throw() {
+                                                                const ModelAlloc<T2>&) throw() {

        return false;
 }
 
        return false;
 }
 


@@ -163,15 +163,15 @@ bool operator!= (const ModelAlloc<T1>&,
  */
 template <class T>
 class SnapshotAlloc {
  */
 template <class T>
 class SnapshotAlloc {

- public:
+public:

        // type definitions
        // type definitions

-       typedef T        value_type;
+       typedef T value_type;

        typedef T*       pointer;
        typedef const T* const_pointer;
        typedef T&       reference;
        typedef const T& const_reference;
        typedef T*       pointer;
        typedef const T* const_pointer;
        typedef T&       reference;
        typedef const T& const_reference;

-       typedef size_t   size_type;
-       typedef size_t   difference_type;
+       typedef size_t size_type;
+       typedef size_t difference_type;

 
        // rebind allocator to type U
        template <class U>
 
        // rebind allocator to type U
        template <class U>


@@ -232,36 +232,36 @@ class SnapshotAlloc {
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator ==(const SnapshotAlloc<T1>&,
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator ==(const SnapshotAlloc<T1>&,

-               const SnapshotAlloc<T2>&) throw() {
+                                                                const SnapshotAlloc<T2>&) throw() {

        return true;
 }
 
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator!= (const SnapshotAlloc<T1>&,
        return true;
 }
 
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator!= (const SnapshotAlloc<T1>&,

-               const SnapshotAlloc<T2>&) throw() {
+                                                                const SnapshotAlloc<T2>&) throw() {

        return false;
 }
 
 #ifdef __cplusplus
 extern "C" {
 #endif
        return false;
 }
 
 #ifdef __cplusplus
 extern "C" {
 #endif

-       typedef void * mspace;
-       extern void * mspace_malloc(mspace msp, size_t bytes);
-       extern void mspace_free(mspace msp, void* mem);
-       extern void * mspace_realloc(mspace msp, void* mem, size_t newsize);
-       extern void * mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
-       extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
-       extern mspace create_mspace(size_t capacity, int locked);
+typedef void * mspace;
+extern void * mspace_malloc(mspace msp, size_t bytes);
+extern void mspace_free(mspace msp, void* mem);
+extern void * mspace_realloc(mspace msp, void* mem, size_t newsize);
+extern void * mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
+extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
+extern mspace create_mspace(size_t capacity, int locked);

 
 #if USE_MPROTECT_SNAPSHOT
 
 #if USE_MPROTECT_SNAPSHOT

-       extern mspace user_snapshot_space;
+extern mspace user_snapshot_space;

 #endif
 
 #endif
 

-       extern mspace model_snapshot_space;
+extern mspace model_snapshot_space;

 
 #ifdef __cplusplus
 
 #ifdef __cplusplus

-};  /* end of extern "C" */
+};     /* end of extern "C" */

 #endif
 
 #endif
 

-#endif /* _MY_MEMORY_H */
+#endif/* _MY_MEMORY_H */

diff --git a/nodestack.cc b/nodestack.cc
index b9aaf6fd54dd1dfcae3dff1437afd3ba05b7ec4c..c1c3cfc502a7cca8b53f984d0584e7e9750cc609 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -54,7 +54,7 @@ NodeStack::NodeStack() :
 
 NodeStack::~NodeStack()
 {
 
 NodeStack::~NodeStack()
 {

-       for (unsigned int i = 0; i < node_list.size(); i++)
+       for (unsigned int i = 0;i < node_list.size();i++)

                delete node_list[i];
 }
 
                delete node_list[i];
 }
 


@@ -76,7 +76,7 @@ void NodeStack::print() const
 {
        model_print("............................................\n");
        model_print("NodeStack printing node_list:\n");
 {
        model_print("............................................\n");
        model_print("NodeStack printing node_list:\n");

-       for (unsigned int it = 0; it < node_list.size(); it++) {
+       for (unsigned int it = 0;it < node_list.size();it++) {

                if ((int)it == this->head_idx)
                        model_print("vvv following action is the current iterator vvv\n");
                node_list[it]->print();
                if ((int)it == this->head_idx)
                        model_print("vvv following action is the current iterator vvv\n");
                node_list[it]->print();


@@ -97,9 +97,9 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
 
 /** Reset the node stack. */
 
 
 /** Reset the node stack. */

-void NodeStack::full_reset() 
+void NodeStack::full_reset()

 {
 {

-       for (unsigned int i = 0; i < node_list.size(); i++)
+       for (unsigned int i = 0;i < node_list.size();i++)

                delete node_list[i];
        node_list.clear();
        reset_execution();
                delete node_list[i];
        node_list.clear();
        reset_execution();

diff --git a/nodestack.h b/nodestack.h
index edaf397e2ee7d4c335ac35f5cce60debaae9b546..c5e6d415d2d7fa6bb9579efeaaa44b5f7d36cf63 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -1,6 +1,6 @@
 /** @file nodestack.h
  *  @brief Stack of operations for use in backtracking.
 /** @file nodestack.h
  *  @brief Stack of operations for use in backtracking.

-*/
+ */

 
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__
 
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__


@@ -80,4 +80,4 @@ private:
        int head_idx;
 };
 
        int head_idx;
 };
 

-#endif /* __NODESTACK_H__ */
+#endif/* __NODESTACK_H__ */

diff --git a/output.h b/output.h
index e390bb613510539958a1507eb2aaaddebd374ae3..53afb2c5972e13b1a4964a45c8ef00c39e5fdf0f 100644 (file)
--- a/output.h
+++ b/output.h
@@ -15,6 +15,6 @@ static inline void print_program_output() { }
 void redirect_output();
 void clear_program_output();
 void print_program_output();
 void redirect_output();
 void clear_program_output();
 void print_program_output();

-#endif /* ! CONFIG_DEBUG */
+#endif/* ! CONFIG_DEBUG */

 
 

-#endif /* __OUTPUT_H__ */
+#endif/* __OUTPUT_H__ */

diff --git a/params.h b/params.h
index 4f49d81f83d0bfab96884f85a5818a074a42ba8e..597ce1ca67c85e95c91668a042d4df01dfed577d 100644 (file)
--- a/params.h
+++ b/params.h
@@ -19,4 +19,4 @@ struct model_params {
        char **argv;
 };
 
        char **argv;
 };
 

-#endif /* __PARAMS_H__ */
+#endif/* __PARAMS_H__ */

diff --git a/pthread.cc b/pthread.cc
index 87dc206510b142ae48886237b15181a5262a1245..f0f968489d4857c86f60b5ee13972d735fada982 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -15,7 +15,7 @@
 #include "execution.h"
 
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
 #include "execution.h"
 
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,

-          pthread_start_t start_routine, void * arg) {
+                                                                        pthread_start_t start_routine, void * arg) {

        struct pthread_params params = { start_routine, arg };
 
        ModelAction *act = new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params);
        struct pthread_params params = { start_routine, arg };
 
        ModelAction *act = new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params);


@@ -37,19 +37,19 @@ int pthread_join(pthread_t t, void **value_ptr) {
                // store return value
                void *rtval = th->get_pthread_return();
                *value_ptr = rtval;
                // store return value
                void *rtval = th->get_pthread_return();
                *value_ptr = rtval;

-       } 
+       }

        return 0;
 }
 
 void pthread_exit(void *value_ptr) {
        Thread * th = thread_current();
        model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, th));
        return 0;
 }
 
 void pthread_exit(void *value_ptr) {
        Thread * th = thread_current();
        model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, th));

-       while(1) ; //make warning goaway
+       while(1) ;                      //make warning goaway

 }
 
 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
        if (!model) {
 }
 
 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
        if (!model) {

-         model = new ModelChecker();
+               model = new ModelChecker();

        }
 
        cdsc::mutex *m = new cdsc::mutex();
        }
 
        cdsc::mutex *m = new cdsc::mutex();


@@ -62,10 +62,10 @@ int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
 int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
        ModelExecution *execution = model->get_execution();
 
 int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
        ModelExecution *execution = model->get_execution();
 

-       /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used 
+       /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used

           instead of pthread_mutex_init, or where *p_mutex is not stored
           in the execution->mutex_map for some reason. */
           instead of pthread_mutex_init, or where *p_mutex is not stored
           in the execution->mutex_map for some reason. */

-       if (!execution->getMutexMap()->contains(p_mutex)) {     
+       if (!execution->getMutexMap()->contains(p_mutex)) {

                pthread_mutex_init(p_mutex, NULL);
        }
 
                pthread_mutex_init(p_mutex, NULL);
        }
 


@@ -85,7 +85,7 @@ int pthread_mutex_trylock(pthread_mutex_t *p_mutex) {
        cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
        return m->try_lock();
 }
        cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
        return m->try_lock();
 }

-int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {   
+int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {

        ModelExecution *execution = model->get_execution();
        cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 
        ModelExecution *execution = model->get_execution();
        cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 


@@ -99,24 +99,24 @@ int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {
 }
 
 int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,
 }
 
 int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,

-                               const struct timespec *__restrict abstime) {
+                                                                                                                const struct timespec *__restrict abstime) {

 // timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next
 
 /*
 // timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next
 
 /*

-       ModelExecution *execution = model->get_execution();
-       if (!execution->mutex_map.contains(p_mutex)) {  
-               pthread_mutex_init(p_mutex, NULL);
-       }
-       cdsc::mutex *m = execution->mutex_map.get(p_mutex);
-
-       if (m != NULL) {
-               m->lock();
-       } else {
-               printf("something is wrong with pthread_mutex_timedlock\n");
-       }
-
-       printf("pthread_mutex_timedlock is called. It is currently implemented as a normal lock operation without no timeout\n");
-*/
+        ModelExecution *execution = model->get_execution();
+        if (!execution->mutex_map.contains(p_mutex)) {
+                pthread_mutex_init(p_mutex, NULL);
+        }
+        cdsc::mutex *m = execution->mutex_map.get(p_mutex);
+
+        if (m != NULL) {
+                m->lock();
+        } else {
+                printf("something is wrong with pthread_mutex_timedlock\n");
+        }
+
+        printf("pthread_mutex_timedlock is called. It is currently implemented as a normal lock operation without no timeout\n");
+ */

        return 0;
 }
 
        return 0;
 }
 


@@ -150,8 +150,8 @@ int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) {
        return 0;
 }
 
        return 0;
 }
 

-int pthread_cond_timedwait(pthread_cond_t *p_cond, 
-    pthread_mutex_t *p_mutex, const struct timespec *abstime) {
+int pthread_cond_timedwait(pthread_cond_t *p_cond,
+                                                                                                        pthread_mutex_t *p_mutex, const struct timespec *abstime) {

 // implement cond_timedwait as a noop and let the scheduler decide which thread goes next
        ModelExecution *execution = model->get_execution();
 
 // implement cond_timedwait as a noop and let the scheduler decide which thread goes next
        ModelExecution *execution = model->get_execution();
 

diff --git a/schedule.cc b/schedule.cc
index fff26ce2128a40d7258e13bfd4ab40e3fa2e35f0..f26a1a6a133b569ed25c72141545ae061fbdb9b2 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -115,7 +115,7 @@ bool Scheduler::is_sleep_set(const Thread *t) const
 bool Scheduler::all_threads_sleeping() const
 {
        bool sleeping = false;
 bool Scheduler::all_threads_sleeping() const
 {
        bool sleeping = false;

-       for (int i = 0; i < enabled_len; i++)
+       for (int i = 0;i < enabled_len;i++)

                if (enabled[i] == THREAD_ENABLED)
                        return false;
                else if (enabled[i] == THREAD_SLEEP_SET)
                if (enabled[i] == THREAD_ENABLED)
                        return false;
                else if (enabled[i] == THREAD_SLEEP_SET)


@@ -206,14 +206,14 @@ Thread * Scheduler::select_next_thread(Node *n)
 {
        int avail_threads = 0;
        int thread_list[enabled_len];
 {
        int avail_threads = 0;
        int thread_list[enabled_len];

-       for (int i = 0; i< enabled_len; i++) {
-         if (enabled[i] == THREAD_ENABLED)
-           thread_list[avail_threads++] = i;
+       for (int i = 0;i< enabled_len;i++) {
+               if (enabled[i] == THREAD_ENABLED)
+                       thread_list[avail_threads++] = i;

        }
 
        if (avail_threads == 0)
        }
 
        if (avail_threads == 0)

-           return NULL; // No threads availablex
-           
+               return NULL;                            // No threads availablex
+

        Thread * thread = execution->getFuzzer()->selectThread(n, thread_list, avail_threads);
        curr_thread_index = id_to_int(thread->get_id());
        return thread;
        Thread * thread = execution->getFuzzer()->selectThread(n, thread_list, avail_threads);
        curr_thread_index = id_to_int(thread->get_id());
        return thread;


@@ -254,7 +254,7 @@ void Scheduler::print() const
        int curr_id = current ? id_to_int(current->get_id()) : -1;
 
        model_print("Scheduler: ");
        int curr_id = current ? id_to_int(current->get_id()) : -1;
 
        model_print("Scheduler: ");

-       for (int i = 0; i < enabled_len; i++) {
+       for (int i = 0;i < enabled_len;i++) {

                char str[20];
                enabled_type_to_string(enabled[i], str);
                model_print("[%i: %s%s]", i, i == curr_id ? "current, " : "", str);
                char str[20];
                enabled_type_to_string(enabled[i], str);
                model_print("[%i: %s%s]", i, i == curr_id ? "current, " : "", str);

diff --git a/schedule.h b/schedule.h
index 6498789a9a91ca1bce92a7d17453d663eb4ab2b0..16ddb341e64e9b96830740af38f5dc1e2dee97aa 100644 (file)
--- a/schedule.h
+++ b/schedule.h
@@ -55,4 +55,4 @@ private:
        Thread *current;
 };
 
        Thread *current;
 };
 

-#endif /* __SCHEDULE_H__ */
+#endif/* __SCHEDULE_H__ */

diff --git a/snapshot-interface.cc b/snapshot-interface.cc
index 5242d168fb4072552cda80f5069b85c3a29fd95b..bf12fe8ae77f60471327b8cd9ccc41a4521acb9a 100644 (file)
--- a/snapshot-interface.cc
+++ b/snapshot-interface.cc
@@ -22,12 +22,12 @@ struct snapshot_entry {
 };
 
 class SnapshotStack {
 };
 
 class SnapshotStack {

- public:
+public:

        int backTrackBeforeStep(int seq_index);
        void snapshotStep(int seq_index);
 
        MEMALLOC
        int backTrackBeforeStep(int seq_index);
        void snapshotStep(int seq_index);
 
        MEMALLOC

- private:
+private:

        ModelVector<struct snapshot_entry> stack;
 };
 
        ModelVector<struct snapshot_entry> stack;
 };
 


@@ -73,7 +73,7 @@ static void SnapshotGlobalSegments()
                sscanf(buf, "%22s %p-%p", type, &begin, &end);
 
                char * secondpart = strstr(buf, "]");
                sscanf(buf, "%22s %p-%p", type, &begin, &end);
 
                char * secondpart = strstr(buf, "]");

-               
+

                sscanf(&secondpart[2], "%c%c%c/%c%c%c SM=%3s %200s\n", &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
                if (w == 'w' && strstr(regionname, MYBINARYNAME)) {
                        size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
                sscanf(&secondpart[2], "%c%c%c/%c%c%c SM=%3s %200s\n", &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
                if (w == 'w' && strstr(regionname, MYBINARYNAME)) {
                        size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;


@@ -141,7 +141,7 @@ static void SnapshotGlobalSegments()
 int SnapshotStack::backTrackBeforeStep(int seqindex)
 {
        int i;
 int SnapshotStack::backTrackBeforeStep(int seqindex)
 {
        int i;

-       for (i = (int)stack.size() - 1; i >= 0; i++)
+       for (i = (int)stack.size() - 1;i >= 0;i++)

                if (stack[i].index <= seqindex)
                        break;
                else
                if (stack[i].index <= seqindex)
                        break;
                else

diff --git a/snapshot-interface.h b/snapshot-interface.h
index 7f4de211badfe57b580d224306b08c3ffce5929b..d926c74e691dd762ccf06b2cd1bca1dfc2fd1a41 100644 (file)
--- a/snapshot-interface.h
+++ b/snapshot-interface.h
@@ -10,8 +10,8 @@ typedef unsigned int snapshot_id;
 
 typedef void (*VoidFuncPtr)();
 void snapshot_system_init(unsigned int numbackingpages,
 
 typedef void (*VoidFuncPtr)();
 void snapshot_system_init(unsigned int numbackingpages,

-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint);
+                                                                                                       unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                       unsigned int numheappages, VoidFuncPtr entryPoint);

 
 void snapshot_stack_init();
 void snapshot_record(int seq_index);
 
 void snapshot_stack_init();
 void snapshot_record(int seq_index);

diff --git a/snapshot.cc b/snapshot.cc
index 7deaeff4339a0dcdd6e6d535bf4cc67245cab08e..826046f0341e80d5ab5384ba46adb0a2d47312d7 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -40,8 +40,8 @@ struct BackingPageRecord {
 
 /* Struct for each memory region */
 struct MemoryRegion {
 
 /* Struct for each memory region */
 struct MemoryRegion {

-       void *basePtr; // base of memory region
-       int sizeInPages; // size of memory region in pages
+       void *basePtr;                  // base of memory region
+       int sizeInPages;                        // size of memory region in pages

 };
 
 /** ReturnPageAlignedAddress returns a page aligned address for the
 };
 
 /** ReturnPageAlignedAddress returns a page aligned address for the


@@ -57,19 +57,19 @@ struct mprot_snapshotter {
        mprot_snapshotter(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions);
        ~mprot_snapshotter();
 
        mprot_snapshotter(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions);
        ~mprot_snapshotter();
 

-       struct MemoryRegion *regionsToSnapShot; //This pointer references an array of memory regions to snapshot
-       snapshot_page_t *backingStore; //This pointer references an array of snapshotpage's that form the backing store
-       void *backingStoreBasePtr; //This pointer references an array of snapshotpage's that form the backing store
-       struct BackingPageRecord *backingRecords; //This pointer references an array of backingpagerecord's (same number of elements as backingstore
-       struct SnapShotRecord *snapShots; //This pointer references the snapshot array
+       struct MemoryRegion *regionsToSnapShot;                         //This pointer references an array of memory regions to snapshot
+       snapshot_page_t *backingStore;                  //This pointer references an array of snapshotpage's that form the backing store
+       void *backingStoreBasePtr;                      //This pointer references an array of snapshotpage's that form the backing store
+       struct BackingPageRecord *backingRecords;                               //This pointer references an array of backingpagerecord's (same number of elements as backingstore
+       struct SnapShotRecord *snapShots;                               //This pointer references the snapshot array

 
 

-       unsigned int lastSnapShot; //Stores the next snapshot record we should use
-       unsigned int lastBackingPage; //Stores the next backingpage we should use
-       unsigned int lastRegion; //Stores the next memory region to be used
+       unsigned int lastSnapShot;                      //Stores the next snapshot record we should use
+       unsigned int lastBackingPage;                           //Stores the next backingpage we should use
+       unsigned int lastRegion;                        //Stores the next memory region to be used

 
 

-       unsigned int maxRegions; //Stores the max number of memory regions we support
-       unsigned int maxBackingPages; //Stores the total number of backing pages
-       unsigned int maxSnapShots; //Stores the total number of snapshots we allow
+       unsigned int maxRegions;                        //Stores the max number of memory regions we support
+       unsigned int maxBackingPages;                           //Stores the total number of backing pages
+       unsigned int maxSnapShots;                      //Stores the total number of snapshots we allow

 
        MEMALLOC
 };
 
        MEMALLOC
 };


@@ -108,13 +108,13 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
        if (si->si_code == SEGV_MAPERR) {
                model_print("Segmentation fault at %p\n", si->si_addr);
                model_print("For debugging, place breakpoint at: %s:%d\n",
        if (si->si_code == SEGV_MAPERR) {
                model_print("Segmentation fault at %p\n", si->si_addr);
                model_print("For debugging, place breakpoint at: %s:%d\n",

-                               __FILE__, __LINE__);
+                                                               __FILE__, __LINE__);

                // print_trace(); // Trace printing may cause dynamic memory allocation
                // print_trace(); // Trace printing may cause dynamic memory allocation

-               exit(EXIT_FAILURE);
+               exit(EXIT_FAILURE);

        }
        void* addr = ReturnPageAlignedAddress(si->si_addr);
 
        }
        void* addr = ReturnPageAlignedAddress(si->si_addr);
 

-       unsigned int backingpage = mprot_snap->lastBackingPage++; //Could run out of pages...
+       unsigned int backingpage = mprot_snap->lastBackingPage++;                               //Could run out of pages...

        if (backingpage == mprot_snap->maxBackingPages) {
                model_print("Out of backing pages at %p\n", si->si_addr);
                exit(EXIT_FAILURE);
        if (backingpage == mprot_snap->maxBackingPages) {
                model_print("Out of backing pages at %p\n", si->si_addr);
                exit(EXIT_FAILURE);


@@ -132,8 +132,8 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
 }
 
 static void mprot_snapshot_init(unsigned int numbackingpages,
 }
 
 static void mprot_snapshot_init(unsigned int numbackingpages,

-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                                               unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                                               unsigned int numheappages, VoidFuncPtr entryPoint)

 {
        /* Setup a stack for our signal handler....  */
        stack_t ss;
 {
        /* Setup a stack for our signal handler....  */
        stack_t ss;


@@ -167,7 +167,7 @@ static void mprot_snapshot_init(unsigned int numbackingpages,
        memset(&si, 0, sizeof(si));
        si.si_addr = ss.ss_sp;
        mprot_handle_pf(SIGSEGV, &si, NULL);
        memset(&si, 0, sizeof(si));
        si.si_addr = ss.ss_sp;
        mprot_handle_pf(SIGSEGV, &si, NULL);

-       mprot_snap->lastBackingPage--; //remove the fake page we copied
+       mprot_snap->lastBackingPage--;                  //remove the fake page we copied

 
        void *basemySpace = model_malloc((numheappages + 1) * PAGESIZE);
        void *pagealignedbase = PageAlignAddressUpward(basemySpace);
 
        void *basemySpace = model_malloc((numheappages + 1) * PAGESIZE);
        void *pagealignedbase = PageAlignAddressUpward(basemySpace);


@@ -191,15 +191,15 @@ static void mprot_add_to_snapshot(void *addr, unsigned int numPages)
        }
 
        DEBUG("snapshot region %p-%p (%u page%s)\n",
        }
 
        DEBUG("snapshot region %p-%p (%u page%s)\n",

-                       addr, (char *)addr + numPages * PAGESIZE, numPages,
-                       numPages > 1 ? "s" : "");
+                               addr, (char *)addr + numPages * PAGESIZE, numPages,
+                               numPages > 1 ? "s" : "");

        mprot_snap->regionsToSnapShot[memoryregion].basePtr = addr;
        mprot_snap->regionsToSnapShot[memoryregion].sizeInPages = numPages;
 }
 
 static snapshot_id mprot_take_snapshot()
 {
        mprot_snap->regionsToSnapShot[memoryregion].basePtr = addr;
        mprot_snap->regionsToSnapShot[memoryregion].sizeInPages = numPages;
 }
 
 static snapshot_id mprot_take_snapshot()
 {

-       for (unsigned int region = 0; region < mprot_snap->lastRegion; region++) {
+       for (unsigned int region = 0;region < mprot_snap->lastRegion;region++) {

                if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ) == -1) {
                        perror("mprotect");
                        model_print("Failed to mprotect inside of takeSnapShot\n");
                if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ) == -1) {
                        perror("mprotect");
                        model_print("Failed to mprotect inside of takeSnapShot\n");


@@ -220,7 +220,7 @@ static void mprot_roll_back(snapshot_id theID)
 {
 #if USE_MPROTECT_SNAPSHOT == 2
        if (mprot_snap->lastSnapShot == (theID + 1)) {
 {
 #if USE_MPROTECT_SNAPSHOT == 2
        if (mprot_snap->lastSnapShot == (theID + 1)) {

-               for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage; page < mprot_snap->lastBackingPage; page++) {
+               for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage;page < mprot_snap->lastBackingPage;page++) {

                        memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
                }
                return;
                        memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
                }
                return;


@@ -228,14 +228,14 @@ static void mprot_roll_back(snapshot_id theID)
 #endif
 
        HashTable< void *, bool, uintptr_t, 4, model_malloc, model_calloc, model_free> duplicateMap;
 #endif
 
        HashTable< void *, bool, uintptr_t, 4, model_malloc, model_calloc, model_free> duplicateMap;

-       for (unsigned int region = 0; region < mprot_snap->lastRegion; region++) {
+       for (unsigned int region = 0;region < mprot_snap->lastRegion;region++) {

                if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ | PROT_WRITE) == -1) {
                        perror("mprotect");
                        model_print("Failed to mprotect inside of takeSnapShot\n");
                        exit(EXIT_FAILURE);
                }
        }
                if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ | PROT_WRITE) == -1) {
                        perror("mprotect");
                        model_print("Failed to mprotect inside of takeSnapShot\n");
                        exit(EXIT_FAILURE);
                }
        }

-       for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage; page < mprot_snap->lastBackingPage; page++) {
+       for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage;page < mprot_snap->lastBackingPage;page++) {

                if (!duplicateMap.contains(mprot_snap->backingRecords[page].basePtrOfPage)) {
                        duplicateMap.put(mprot_snap->backingRecords[page].basePtrOfPage, true);
                        memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
                if (!duplicateMap.contains(mprot_snap->backingRecords[page].basePtrOfPage)) {
                        duplicateMap.put(mprot_snap->backingRecords[page].basePtrOfPage, true);
                        memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));


@@ -243,13 +243,13 @@ static void mprot_roll_back(snapshot_id theID)
        }
        mprot_snap->lastSnapShot = theID;
        mprot_snap->lastBackingPage = mprot_snap->snapShots[theID].firstBackingPage;
        }
        mprot_snap->lastSnapShot = theID;
        mprot_snap->lastBackingPage = mprot_snap->snapShots[theID].firstBackingPage;

-       mprot_take_snapshot(); //Make sure current snapshot is still good...All later ones are cleared
+       mprot_take_snapshot();                  //Make sure current snapshot is still good...All later ones are cleared

 }
 
 }
 

-#else /* !USE_MPROTECT_SNAPSHOT */
+#else  /* !USE_MPROTECT_SNAPSHOT */

 
 

-#define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20)) // 100mb for the shared memory
-#define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)  // 20 mb out of the above 100 mb for my stack
+#define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20))// 100mb for the shared memory
+#define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)       // 20 mb out of the above 100 mb for my stack

 
 struct fork_snapshotter {
        /** @brief Pointer to the shared (non-snapshot) memory heap base
 
 struct fork_snapshotter {
        /** @brief Pointer to the shared (non-snapshot) memory heap base


@@ -289,19 +289,19 @@ struct fork_snapshotter {
 static struct fork_snapshotter *fork_snap = NULL;
 
 /** @statics
 static struct fork_snapshotter *fork_snap = NULL;
 
 /** @statics

-*   These variables are necessary because the stack is shared region and
-*   there exists a race between all processes executing the same function.
-*   To avoid the problem above, we require variables allocated in 'safe' regions.
-*   The bug was actually observed with the forkID, these variables below are
-*   used to indicate the various contexts to which to switch to.
-*
-*   @private_ctxt: the context which is internal to the current process. Used
-*   for running the internal snapshot/rollback loop.
-*   @exit_ctxt: a special context used just for exiting from a process (so we
-*   can use swapcontext() instead of setcontext() + hacks)
-*   @snapshotid: it is a running counter for the various forked processes
-*   snapshotid. it is incremented and set in a persistently shared record
-*/
+ *   These variables are necessary because the stack is shared region and
+ *   there exists a race between all processes executing the same function.
+ *   To avoid the problem above, we require variables allocated in 'safe' regions.
+ *   The bug was actually observed with the forkID, these variables below are
+ *   used to indicate the various contexts to which to switch to.
+ *
+ *   @private_ctxt: the context which is internal to the current process. Used
+ *   for running the internal snapshot/rollback loop.
+ *   @exit_ctxt: a special context used just for exiting from a process (so we
+ *   can use swapcontext() instead of setcontext() + hacks)
+ *   @snapshotid: it is a running counter for the various forked processes
+ *   snapshotid. it is incremented and set in a persistently shared record
+ */

 static ucontext_t private_ctxt;
 static ucontext_t exit_ctxt;
 static snapshot_id snapshotid = 0;
 static ucontext_t private_ctxt;
 static ucontext_t exit_ctxt;
 static snapshot_id snapshotid = 0;


@@ -314,7 +314,7 @@ static snapshot_id snapshotid = 0;
  * @param func The entry point function for the context
  */
 static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize,
  * @param func The entry point function for the context
  */
 static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize,

-               void (*func)(void))
+                                                                                                        void (*func)(void))

 {
        getcontext(ctxt);
        ctxt->uc_stack.ss_sp = stack;
 {
        getcontext(ctxt);
        ctxt->uc_stack.ss_sp = stack;


@@ -361,8 +361,8 @@ mspace create_shared_mspace()
 }
 
 static void fork_snapshot_init(unsigned int numbackingpages,
 }
 
 static void fork_snapshot_init(unsigned int numbackingpages,

-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                                        unsigned int numheappages, VoidFuncPtr entryPoint)

 {
        if (!fork_snap)
                createSharedMemory();
 {
        if (!fork_snap)
                createSharedMemory();


@@ -377,7 +377,7 @@ static void fork_snapshot_init(unsigned int numbackingpages,
 
        /* setup the shared-stack context */
        create_context(&fork_snap->shared_ctxt, fork_snap->mStackBase,
 
        /* setup the shared-stack context */
        create_context(&fork_snap->shared_ctxt, fork_snap->mStackBase,

-                       STACK_SIZE_DEFAULT, entryPoint);
+                                                                STACK_SIZE_DEFAULT, entryPoint);

        /* switch to a new entryPoint context, on a new stack */
        model_swapcontext(&private_ctxt, &fork_snap->shared_ctxt);
 
        /* switch to a new entryPoint context, on a new stack */
        model_swapcontext(&private_ctxt, &fork_snap->shared_ctxt);
 


@@ -393,7 +393,7 @@ static void fork_snapshot_init(unsigned int numbackingpages,
                        setcontext(&fork_snap->shared_ctxt);
                } else {
                        DEBUG("parent PID: %d, child PID: %d, snapshot ID: %d\n",
                        setcontext(&fork_snap->shared_ctxt);
                } else {
                        DEBUG("parent PID: %d, child PID: %d, snapshot ID: %d\n",

-                               getpid(), forkedID, snapshotid);
+                                               getpid(), forkedID, snapshotid);

 
                        while (waitpid(forkedID, NULL, 0) < 0) {
                                /* waitpid() may be interrupted */
 
                        while (waitpid(forkedID, NULL, 0) < 0) {
                                /* waitpid() may be interrupted */


@@ -424,15 +424,15 @@ static void fork_roll_back(snapshot_id theID)
        fork_snap->mIDToRollback = -1;
 }
 
        fork_snap->mIDToRollback = -1;
 }
 

-#endif /* !USE_MPROTECT_SNAPSHOT */
+#endif/* !USE_MPROTECT_SNAPSHOT */

 
 /**
  * @brief Initializes the snapshot system
  * @param entryPoint the function that should run the program.
  */
 void snapshot_system_init(unsigned int numbackingpages,
 
 /**
  * @brief Initializes the snapshot system
  * @param entryPoint the function that should run the program.
  */
 void snapshot_system_init(unsigned int numbackingpages,

-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                       unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                       unsigned int numheappages, VoidFuncPtr entryPoint)

 {
 #if USE_MPROTECT_SNAPSHOT
        mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);
 {
 #if USE_MPROTECT_SNAPSHOT
        mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);

diff --git a/stacktrace.h b/stacktrace.h
index a3b035096e796f13809eb4eedcfeada7bc84c9ba..6444c41881fa4519222b0309d5ced73615539640 100644 (file)
--- a/stacktrace.h
+++ b/stacktrace.h
@@ -38,12 +38,12 @@ static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_fra
 
        // iterate over the returned symbol lines. skip the first, it is the
        // address of this function.
 
        // iterate over the returned symbol lines. skip the first, it is the
        // address of this function.

-       for (int i = 1; i < addrlen; i++) {
+       for (int i = 1;i < addrlen;i++) {

                char *begin_name = 0, *begin_offset = 0, *end_offset = 0;
 
                // find parentheses and +address offset surrounding the mangled name:
                // ./module(function+0x15c) [0x8048a6d]
                char *begin_name = 0, *begin_offset = 0, *end_offset = 0;
 
                // find parentheses and +address offset surrounding the mangled name:
                // ./module(function+0x15c) [0x8048a6d]

-               for (char *p = symbollist[i]; *p; ++p) {
+               for (char *p = symbollist[i];*p;++p) {

                        if (*p == '(')
                                begin_name = p;
                        else if (*p == '+')
                        if (*p == '(')
                                begin_name = p;
                        else if (*p == '+')


@@ -65,16 +65,16 @@ static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_fra
 
                        int status;
                        char* ret = abi::__cxa_demangle(begin_name,
 
                        int status;
                        char* ret = abi::__cxa_demangle(begin_name,

-                                       funcname, &funcnamesize, &status);
+                                                                                                                                                       funcname, &funcnamesize, &status);

                        if (status == 0) {
                        if (status == 0) {

-                               funcname = ret; // use possibly realloc()-ed string
+                               funcname = ret;                                                                                                 // use possibly realloc()-ed string

                                dprintf(fd, "  %s : %s+%s\n",
                                dprintf(fd, "  %s : %s+%s\n",

-                                               symbollist[i], funcname, begin_offset);
+                                                               symbollist[i], funcname, begin_offset);

                        } else {
                                // demangling failed. Output function name as a C function with
                                // no arguments.
                                dprintf(fd, "  %s : %s()+%s\n",
                        } else {
                                // demangling failed. Output function name as a C function with
                                // no arguments.
                                dprintf(fd, "  %s : %s()+%s\n",

-                                               symbollist[i], begin_name, begin_offset);
+                                                               symbollist[i], begin_name, begin_offset);

                        }
                } else {
                        // couldn't parse the line? print the whole line.
                        }
                } else {
                        // couldn't parse the line? print the whole line.


@@ -91,4 +91,4 @@ static inline void print_stacktrace(FILE *out, unsigned int max_frames = 63)
        print_stacktrace(fileno(out), max_frames);
 }
 
        print_stacktrace(fileno(out), max_frames);
 }
 

-#endif // __STACKTRACE_H__
+#endif// __STACKTRACE_H__

diff --git a/stl-model.h b/stl-model.h
index ae6e8b27c8443a79fcf69631cacdf10a0dc256e0..9fa7cf9f3b64bac31c9c10a80f37da4a5ae1a2a9 100644 (file)
--- a/stl-model.h
+++ b/stl-model.h
@@ -8,7 +8,7 @@
 template<typename _Tp>
 class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
 {
 template<typename _Tp>
 class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
 {

- public:
+public:

        typedef std::list< _Tp, ModelAlloc<_Tp> > list;
 
        ModelList() :
        typedef std::list< _Tp, ModelAlloc<_Tp> > list;
 
        ModelList() :


@@ -25,7 +25,7 @@ class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
 template<typename _Tp>
 class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
 {
 template<typename _Tp>
 class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
 {

- public:
+public:

        typedef std::list<_Tp, SnapshotAlloc<_Tp> > list;
 
        SnapList() :
        typedef std::list<_Tp, SnapshotAlloc<_Tp> > list;
 
        SnapList() :


@@ -42,7 +42,7 @@ class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
 template<typename _Tp>
 class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
 {
 template<typename _Tp>
 class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
 {

- public:
+public:

        typedef std::vector< _Tp, ModelAlloc<_Tp> > vector;
 
        ModelVector() :
        typedef std::vector< _Tp, ModelAlloc<_Tp> > vector;
 
        ModelVector() :


@@ -59,7 +59,7 @@ class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
 template<typename _Tp>
 class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
 {
 template<typename _Tp>
 class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
 {

- public:
+public:

        typedef std::vector< _Tp, SnapshotAlloc<_Tp> > vector;
 
        SnapVector() :
        typedef std::vector< _Tp, SnapshotAlloc<_Tp> > vector;
 
        SnapVector() :


@@ -73,4 +73,4 @@ class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
        SNAPSHOTALLOC
 };
 
        SNAPSHOTALLOC
 };
 

-#endif /* __STL_MODEL_H__ */
+#endif/* __STL_MODEL_H__ */

diff --git a/threads-model.h b/threads-model.h
index c6e3a3aff6486f1769f0b19dcb7caae07d05f973..ad178329eec4b38ce5042de6936e9e5f0d516ea2 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -187,4 +187,4 @@ static inline int id_to_int(thread_id_t id)
        return id;
 }
 
        return id;
 }
 

-#endif /* __THREADS_MODEL_H__ */
+#endif/* __THREADS_MODEL_H__ */

diff --git a/threads.cc b/threads.cc
index d1929cd7ad5e6e3c3a781e813d8583a39e94e12d..b87ae4e4488356764aa4974a261a8ed84ac09577 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -143,7 +143,7 @@ Thread::Thread(thread_id_t tid) :
        stack(NULL),
        user_thread(NULL),
        id(tid),
        stack(NULL),
        user_thread(NULL),
        id(tid),

-       state(THREAD_READY), /* Thread is always ready? */
+       state(THREAD_READY),                    /* Thread is always ready? */

        last_action_val(0),
        model_thread(true)
 {
        last_action_val(0),
        model_thread(true)
 {


@@ -176,7 +176,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread
        if (ret)
                model_print("Error in create_context\n");
 
        if (ret)
                model_print("Error in create_context\n");
 

-       user_thread->priv = this; // WL
+       user_thread->priv = this;                               // WL

 }
 
 /**
 }
 
 /**


@@ -258,7 +258,7 @@ Thread * Thread::waiting_on() const
 bool Thread::is_waiting_on(const Thread *t) const
 {
        Thread *wait;
 bool Thread::is_waiting_on(const Thread *t) const
 {
        Thread *wait;

-       for (wait = waiting_on(); wait != NULL; wait = wait->waiting_on())
+       for (wait = waiting_on();wait != NULL;wait = wait->waiting_on())

                if (wait == t)
                        return true;
        return false;
                if (wait == t)
                        return true;
        return false;

diff --git a/traceanalysis.h b/traceanalysis.h
index d363150ab3c72e2c3efcd46a2b8dd7d88dd970a8..3f8c768868c03db71906808e92934fce93f51dfb 100644 (file)
--- a/traceanalysis.h
+++ b/traceanalysis.h
@@ -4,12 +4,12 @@
 
 
 class TraceAnalysis {
 
 
 class TraceAnalysis {

- public:
+public:

        /** setExecution is called once after installation with a reference to
         *  the ModelExecution object. */
 
        virtual void setExecution(ModelExecution * execution) = 0;
        /** setExecution is called once after installation with a reference to
         *  the ModelExecution object. */
 
        virtual void setExecution(ModelExecution * execution) = 0;

-       
+

        /** analyze is called once for each feasible trace with the complete
         *  action_list object. */
 
        /** analyze is called once for each feasible trace with the complete
         *  action_list object. */