From 89ecd60fab0d93d6df6aa35e663ab67db860fa1d Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 10 Jun 2019 21:37:55 -0700 Subject: [PATCH] fix tabbing --- action.cc | 94 +++++++------- action.h | 84 ++++++------- bugmessage.h | 4 +- clockvector.cc | 8 +- clockvector.h | 2 +- cmodelint.cc | 148 +++++++++++----------- common.cc | 12 +- common.h | 24 ++-- conditionvariable.cc | 4 +- config.h | 16 +-- context.cc | 2 +- context.h | 8 +- cyclegraph.cc | 30 ++--- cyclegraph.h | 10 +- datarace.cc | 38 +++--- datarace.h | 6 +- execution.cc | 286 +++++++++++++++++++++--------------------- execution.h | 32 ++--- futex.cc | 16 +-- fuzzer.cc | 26 ++-- fuzzer.h | 10 +- hashtable.h | 14 +-- impatomic.cc | 8 +- librace.cc | 10 +- main.cc | 66 +++++----- model.cc | 64 +++++----- model.h | 18 +-- mutex.cc | 4 +- mymemory.cc | 4 +- mymemory.h | 50 ++++---- nodestack.cc | 8 +- nodestack.h | 4 +- output.h | 4 +- params.h | 2 +- pthread.cc | 48 +++---- schedule.cc | 14 +-- schedule.h | 2 +- snapshot-interface.cc | 8 +- snapshot-interface.h | 4 +- snapshot.cc | 100 +++++++-------- stacktrace.h | 14 +-- stl-model.h | 10 +- threads-model.h | 2 +- threads.cc | 6 +- traceanalysis.h | 4 +- 45 files changed, 664 insertions(+), 664 deletions(-) diff --git a/action.cc b/action.cc index 8c29c533..bbbeceea 100644 --- 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, - uint64_t value, Thread *thread) : + uint64_t value, Thread *thread) : 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, - uint64_t value, int size) : + uint64_t value, int size) : 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 { - return size; + return size; } 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(); - 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; - 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); @@ -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" - " 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) { - 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) { - 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, - 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()); @@ -644,9 +644,9 @@ unsigned int ModelAction::hash() const 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; } diff --git a/action.h b/action.h index 760e9fb0..662d7d7b 100644 --- a/action.h +++ b/action.h @@ -15,7 +15,7 @@ #include "classlist.h" namespace cdsc { - class mutex; +class mutex; } 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 { - 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; @@ -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); - 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; @@ -138,7 +138,7 @@ public: 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; @@ -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; - int getSize() const; - + int getSize() const; + 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; - 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; @@ -207,15 +207,15 @@ private: /** @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; @@ -245,4 +245,4 @@ private: ClockVector *cv; }; -#endif /* __ACTION_H__ */ +#endif/* __ACTION_H__ */ diff --git a/bugmessage.h b/bugmessage.h index bd7d0b68..bab57381 100644 --- 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); } - ~bug_message() { if (msg) snapshot_free(msg); } + ~bug_message() { if (msg) snapshot_free(msg);} char *msg; void print() { model_print("%s", msg); } @@ -18,4 +18,4 @@ struct bug_message { SNAPSHOTALLOC }; -#endif /* __BUGMESSAGE_H__ */ +#endif/* __BUGMESSAGE_H__ */ diff --git a/clockvector.cc b/clockvector.cc index 467a27e9..54e8c4a1 100644 --- 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)); - 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 */ - 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; } - + return changed; } @@ -98,6 +98,6 @@ void ClockVector::print() const { 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" : ", "); } diff --git a/clockvector.h b/clockvector.h index 0e5ba865..b9987b22 100644 --- a/clockvector.h +++ b/clockvector.h @@ -28,4 +28,4 @@ private: int num_threads; }; -#endif /* __CLOCKVECTOR_H__ */ +#endif/* __CLOCKVECTOR_H__ */ diff --git a/cmodelint.cc b/cmodelint.cc index fc80b299..cdd8b442 100644 --- 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) { - 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. */ @@ -75,7 +75,7 @@ void model_fence_action_helper(int atomic_index) { } // 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) { @@ -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) { - 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) { - 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) { - 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) { - 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 ) \ -({ \ - 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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _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) { - _ATOMIC_RMW_( ^= , 64, addr, atomic_index, val); + _ATOMIC_RMW_( ^=, 64, addr, atomic_index, val); } // 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) \ -({ \ - 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 -// 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 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 @@ -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__); \ @@ -259,13 +259,13 @@ void cds_atomic_thread_fence(int atomic_index) { else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \ __r__; }) -#define _ATOMIC_FENCE_( __x__ ) \ + #define _ATOMIC_FENCE_( __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__); \ @@ -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) \ - }) -*/ + }) + */ diff --git a/common.cc b/common.cc index 26f6d5d8..f327d27e 100644 --- a/common.cc +++ b/common.cc @@ -33,11 +33,11 @@ void print_trace(void) 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); -#endif /* CONFIG_STACKTRACE */ +#endif/* CONFIG_STACKTRACE */ } 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", - file, line); + file, line); 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 @@ -139,7 +139,7 @@ void clear_program_output() { 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 */ @@ -170,4 +170,4 @@ void print_program_output() model_print("---- END PROGRAM OUTPUT ----\n"); } -#endif /* ! CONFIG_DEBUG */ +#endif/* ! CONFIG_DEBUG */ diff --git a/common.h b/common.h index 7be72d72..1b2b673f 100644 --- a/common.h +++ b/common.h @@ -11,10 +11,10 @@ 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 -#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 @@ -27,20 +27,20 @@ void assert_hook(void); #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) -#endif /* CONFIG_ASSERT */ +#endif/* CONFIG_ASSERT */ #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 d5d0fc83..1d049f18 100644 --- a/conditionvariable.cc +++ b/conditionvariable.cc @@ -6,11 +6,11 @@ namespace cdsc { condition_variable::condition_variable() { - + } condition_variable::~condition_variable() { - + } void condition_variable::notify_one() { diff --git a/config.h b/config.h index afbac874..ac725c35 100644 --- a/config.h +++ b/config.h @@ -7,13 +7,13 @@ /** 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.*/ @@ -27,11 +27,11 @@ #else #define BIT48 0 #endif -#endif /* BIT48 */ +#endif/* BIT48 */ /** 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() */ diff --git a/context.cc b/context.cc index b5ae0ba5..d446fa76 100644 --- a/context.cc +++ b/context.cc @@ -24,4 +24,4 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp) return 0; } -#endif /* MAC */ +#endif/* MAC */ diff --git a/context.h b/context.h index fb56e247..f0003ce4 100644 --- a/context.h +++ b/context.h @@ -13,13 +13,13 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp); -#else /* !MAC */ +#else /* !MAC */ static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp) -{ +{ return swapcontext(oucp, ucp); } -#endif /* !MAC */ +#endif/* !MAC */ -#endif /* __CONTEXT_H__ */ +#endif/* __CONTEXT_H__ */ diff --git a/cyclegraph.cc b/cyclegraph.cc index 439e6196..f4590bfb 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -69,7 +69,7 @@ bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode) 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 @@ -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. */ - 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)) @@ -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) { - 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) @@ -209,13 +209,13 @@ template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, co 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"); - 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); } } @@ -249,7 +249,7 @@ bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) cons 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); @@ -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, - const ModelAction *to) const; + const ModelAction *to) const; /** @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() { - for (unsigned int i = 0; i < rollbackvector.size(); i++) + for (unsigned int i = 0;i < rollbackvector.size();i++) 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; @@ -366,7 +366,7 @@ unsigned int CycleNode::getNumBackEdges() const template static bool vector_remove_node(SnapVector& 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; @@ -412,7 +412,7 @@ CycleNode * CycleNode::removeBackEdge() */ 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); diff --git a/cyclegraph.h b/cyclegraph.h index 556af1cf..d273279a 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -20,7 +20,7 @@ /** @brief A graph of Model Actions for tracking cycles. */ class CycleGraph { - public: +public: CycleGraph(); ~CycleGraph(); @@ -49,7 +49,7 @@ class CycleGraph { 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); @@ -81,7 +81,7 @@ class CycleGraph { * @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; @@ -97,7 +97,7 @@ class CycleNode { const ModelAction * getAction() const { return action; } SNAPSHOTALLOC - private: +private: /** @brief The ModelAction that this node represents */ const ModelAction *action; @@ -112,4 +112,4 @@ class CycleNode { CycleNode *hasRMW; }; -#endif /* __CYCLEGRAPH_H__ */ +#endif/* __CYCLEGRAPH_H__ */ diff --git a/datarace.cc b/datarace.cc index 653039b3..9ba59399 100644 --- 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, - modelclock_t clock2, thread_id_t tid2) + modelclock_t clock2, thread_id_t tid2) { 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 */ - 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); @@ -158,16 +158,16 @@ bool checkDataRaces() 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. */ - 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 - optimized. */ + optimized. */ 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; - 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 - 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 */ diff --git a/datarace.h b/datarace.h index a8f0ba32..ce659d1a 100644 --- 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 - response to synchronization. */ + response to synchronization. */ 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 - a result of synchronization. */ + a result of synchronization. */ 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) -#endif /* __DATARACE_H__ */ +#endif/* __DATARACE_H__ */ diff --git a/execution.cc b/execution.cc index 3a994892..f498efbb 100644 --- a/execution.cc +++ b/execution.cc @@ -16,7 +16,7 @@ #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 @@ -33,7 +33,7 @@ struct 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(); } @@ -51,13 +51,13 @@ struct model_snapshot_members { /** @brief Constructor */ ModelExecution::ModelExecution(ModelChecker *m, - Scheduler *scheduler, - NodeStack *node_stack) : + Scheduler *scheduler, + NodeStack *node_stack) : 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(), @@ -67,8 +67,8 @@ ModelExecution::ModelExecution(ModelChecker *m, 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 */ @@ -81,7 +81,7 @@ ModelExecution::ModelExecution(ModelChecker *m, /** @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; @@ -173,7 +173,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa 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)) @@ -250,7 +250,7 @@ void ModelExecution::set_assert() 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; @@ -270,7 +270,7 @@ bool ModelExecution::is_deadlocked() 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; @@ -285,26 +285,26 @@ bool ModelExecution::is_complete_execution() const */ bool ModelExecution::process_read(ModelAction *curr, ModelVector * 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); } - //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"); @@ -357,7 +357,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) 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()) @@ -368,14 +368,14 @@ bool ModelExecution::process_mutex(ModelAction *curr) 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 - 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(); @@ -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 */ - for (rit = list->rbegin(); rit != list->rend(); rit++) { + for (rit = list->rbegin();rit != list->rend();rit++) { 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); - 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; @@ -486,7 +486,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr) 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)); @@ -494,8 +494,8 @@ bool ModelExecution::process_thread_action(ModelAction *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; @@ -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); - 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); - 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 */ - 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(); - updated = true; /* trigger rel-seq checks */ + updated = true; /* trigger rel-seq checks */ 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; - return false; /* Action was explored previously */ + return false; /* Action was explored previously */ } 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())); - 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(); - 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; @@ -699,25 +699,25 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) ModelVector * 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); - + 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 { - ASSERT(rf_set == NULL); + ASSERT(rf_set == NULL); } - + if (curr->is_write()) - process_write(curr); - + process_write(curr); + if (curr->is_fence()) - process_fence(curr); - + process_fence(curr); + if (curr->is_mutex_op()) - process_mutex(curr); + process_mutex(curr); return curr; } @@ -729,7 +729,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) */ 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() || - 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. */ @@ -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()) { - mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); + mo_graph->addRMWEdge(lastread->get_reads_from(), 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 */ - 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()) @@ -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; - for (rit = list->rbegin(); rit != list->rend(); rit++) { + for (rit = list->rbegin();rit != list->rend();rit++) { 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 && - *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 && - *act < *last_sc_fence_thread_before) { + *act < *last_sc_fence_thread_before) { 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)) - added = mo_graph->addEdge(prevrf, rf) || added; + added = mo_graph->addEdge(prevrf, rf) || added; } 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, - 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; @@ -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 */ - 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()) @@ -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; - for (rit = list->rbegin(); rit != list->rend(); rit++) { + for (rit = list->rbegin();rit != list->rend();rit++) { 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->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) && - !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 @@ -1011,13 +1011,13 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * SnapVector *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; - 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 */ @@ -1056,13 +1056,13 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * * 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; - for ( ; rf != NULL; rf = rf->get_reads_from()) { + for ( ;rf != NULL;rf = rf->get_reads_from()) { 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()) - 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 @@ -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()) - return true; /* complete */ + return true; /* complete */ }; - ASSERT(rf); // Needs to be real write + ASSERT(rf); // Needs to be real write 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) @@ -1099,7 +1099,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf, 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, - ModelAction *read, rel_heads_list_t *release_heads) + ModelAction *read, rel_heads_list_t *release_heads) { 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; - 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; @@ -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) { - for (; rit != list->rend(); rit++) + for (;rit != list->rend();rit++) if (*rit == before_fence) break; @@ -1259,7 +1259,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode 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; @@ -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; - 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; @@ -1305,19 +1305,19 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const } 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 * ModelExecution::build_may_read_from(ModelAction *c last_sc_write = get_last_seq_cst_write(curr); ModelVector * rf_set = new ModelVector(); - + /* 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; - for (rit = list->rbegin(); rit != list->rend(); rit++) { + for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; /* Only consider 'write' actions */ @@ -1360,24 +1360,24 @@ ModelVector * 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()) { - /* 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()) - rf_set->push_back(act); + rf_set->push_back(act); mo_graph->rollbackChanges(); } @@ -1425,7 +1425,7 @@ static void print_list(const action_list_t *list) 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(); @@ -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()); - 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, - 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, - 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; @@ -1539,14 +1539,14 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const * @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()) { - std::memory_order order = curr->get_mo(); + std::memory_order order = curr->get_mo(); 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) - return curr->get_thread_operand(); + 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); - 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); @@ -1629,5 +1629,5 @@ Thread * ModelExecution::take_step(ModelAction *curr) } Fuzzer * ModelExecution::getFuzzer() { - return fuzzer; + return fuzzer; } diff --git a/execution.h b/execution.h index 737477fe..9ad7469a 100644 --- a/execution.h +++ b/execution.h @@ -52,13 +52,13 @@ struct release_seq { 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;} - + 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; } - Fuzzer * getFuzzer(); + Fuzzer * getFuzzer(); CycleGraph * const get_mo_graph() { return mo_graph; } - HashTable * getCondMap() {return &cond_map;} - HashTable * getMutexMap() {return &mutex_map;} - + HashTable * getCondMap() {return &cond_map;} + HashTable * getMutexMap() {return &mutex_map;} + 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; @@ -128,7 +128,7 @@ private: bool next_execution(); ModelAction * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); - bool process_read(ModelAction *curr, ModelVector * rf_set); + bool process_read(ModelAction *curr, ModelVector * rf_set); 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; - ModelVector * build_may_read_from(ModelAction *curr); + ModelVector * build_may_read_from(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); template @@ -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 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_map; SnapVector 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. */ @@ -168,7 +168,7 @@ private: HashTable *, uintptr_t, 4> obj_thrd_map; - HashTable mutex_map; + HashTable mutex_map; HashTable cond_map; /** @@ -206,9 +206,9 @@ private: */ CycleGraph * const mo_graph; - Fuzzer * fuzzer; - + Fuzzer * fuzzer; + Thread * action_select_next_thread(const ModelAction *curr) const; }; -#endif /* __EXECUTION_H__ */ +#endif/* __EXECUTION_H__ */ diff --git a/futex.cc b/futex.cc index fa32e9a2..ce130446 100644 --- a/futex.cc +++ b/futex.cc @@ -2,7 +2,7 @@ // 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 #ifdef _GLIBCXX_HAS_GTHREADS @@ -26,19 +26,19 @@ const unsigned futex_wake_op = 1; namespace std _GLIBCXX_VISIBILITY(default) { -_GLIBCXX_BEGIN_NAMESPACE_VERSION + _GLIBCXX_BEGIN_NAMESPACE_VERSION 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; } - // 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; } @@ -64,7 +64,7 @@ _GLIBCXX_BEGIN_NAMESPACE_VERSION 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 550a0a16..d3d9d2c5 100644 --- a/fuzzer.cc +++ b/fuzzer.cc @@ -4,23 +4,23 @@ #include "model.h" int Fuzzer::selectWrite(ModelAction *read, ModelVector * 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) { - 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) { - 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 a6318d04..3a843510 100644 --- a/fuzzer.h +++ b/fuzzer.h @@ -6,11 +6,11 @@ class Fuzzer { public: - Fuzzer() {} - int selectWrite(ModelAction *read, ModelVector* rf_set); - Thread * selectThread(Node *n, int * threadlist, int numthreads); - Thread * selectNotify(action_list_t * waiters); - MEMALLOC + Fuzzer() {} + int selectWrite(ModelAction *read, ModelVector* rf_set); + Thread * selectThread(Node *n, int * threadlist, int numthreads); + Thread * selectNotify(action_list_t * waiters); + MEMALLOC private: }; #endif diff --git a/hashtable.h b/hashtable.h index 2802eabe..22c90221 100644 --- a/hashtable.h +++ b/hashtable.h @@ -45,7 +45,7 @@ struct hashlistnode { */ template class HashTable { - public: +public: /** * @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); - size = 0; // Initial number of elements in the hash + size = 0; // Initial number of elements in the hash } /** @brief Hash table destructor */ @@ -183,7 +183,7 @@ class HashTable { exit(EXIT_FAILURE); } - table = newtable; // Update the global hashtable upon resize() + table = newtable; // Update the global hashtable upon resize() 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]; - for (; bin < lastbin; bin++) { + for (;bin < lastbin;bin++) { _Key key = bin->key; struct hashlistnode<_Key, _Val> *search; @@ -207,10 +207,10 @@ class HashTable { 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; @@ -219,4 +219,4 @@ class HashTable { double loadfactor; }; -#endif /* __HASHTABLE_H__ */ +#endif/* __HASHTABLE_H__ */ diff --git a/impatomic.cc b/impatomic.cc index 4b5d1c28..a2551803 100644 --- 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 -( 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)); @@ -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_wait__( volatile atomic_flag* __a__ ) { +void __atomic_flag_wait__( volatile atomic_flag* __a__ ) { while ( atomic_flag_test_and_set( __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__ )) ; } diff --git a/librace.cc b/librace.cc index b7836278..a9bb7052 100644 --- 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 -// return anything. +// return anything. 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) { - //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)); @@ -115,7 +115,7 @@ void cds_store16(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)); @@ -125,7 +125,7 @@ void cds_store32(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)); diff --git a/main.cc b/main.cc index 1e5ad166..9375ac0d 100644 --- 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( -"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, @@ -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'}, - {0, 0, 0, 0} /* Terminator */ + {0, 0, 0, 0} /* Terminator */ }; 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': - { - ModelVector * analyses = getInstalledTraceAnalysis(); - if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg)) - error = true; - } - break; - default: /* '?' */ + { + ModelVector * analyses = getInstalledTraceAnalysis(); + if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg)) + error = true; + } + break; + default: /* '?' */ error = true; break; } @@ -172,7 +172,7 @@ static void model_main() snapshot_stack_init(); if (!model) - model = new ModelChecker(); + model = new ModelChecker(); model->setParams(params); install_trace_analyses(model->get_execution()); diff --git a/model.cc b/model.cc index f5f20dd7..1d55182d 100644 --- a/model.cc +++ b/model.cc @@ -44,8 +44,8 @@ ModelChecker::~ModelChecker() /** Method to set parameters */ void ModelChecker::setParams(struct model_params params) { - this->params = params; - execution->setParams(¶ms); + this->params = params; + execution->setParams(¶ms); } /** @@ -62,7 +62,7 @@ void ModelChecker::reset_to_initial_state() * 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); @@ -148,9 +148,9 @@ void ModelChecker::print_bugs() const SnapVector *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(); } @@ -198,7 +198,7 @@ void ModelChecker::print_stats() const 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) { @@ -227,8 +227,8 @@ bool ModelChecker::next_execution() 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) { @@ -237,7 +237,7 @@ bool ModelChecker::next_execution() checkDataRaces(); run_trace_analyses(); - } + } record_stats(); /* Output */ @@ -259,7 +259,7 @@ bool ModelChecker::next_execution() /** @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()); } @@ -314,9 +314,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) 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"); @@ -366,9 +366,9 @@ void ModelChecker::run() 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; - 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 { @@ -379,18 +379,18 @@ void ModelChecker::run() * 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()) { - 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 */ - 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)) { @@ -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(); - 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 || \ - 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; - } + } } } /* 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 (!t) + if (!t) 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. */ - for (unsigned int i = 0; i < trace_analyses.size(); i++) + for (unsigned int i = 0;i < trace_analyses.size();i++) trace_analyses[i]->finish(); } diff --git a/model.h b/model.h index 166eb12d..95fc6abe 100644 --- a/model.h +++ b/model.h @@ -21,11 +21,11 @@ typedef SnapList action_list_t; /** @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 */ @@ -60,9 +60,9 @@ public: 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. */ @@ -104,4 +104,4 @@ private: extern ModelChecker *model; -#endif /* __MODEL_H__ */ +#endif/* __MODEL_H__ */ diff --git a/mutex.cc b/mutex.cc index a431321e..44f64ff7 100644 --- 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); } - + 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)); diff --git a/mymemory.cc b/mymemory.cc index e8ec0805..eff66348 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -259,7 +259,7 @@ void operator delete[](void *p, size_t size) 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) @@ -273,4 +273,4 @@ void Thread_free(void *ptr) free(ptr); } -#endif /* !USE_MPROTECT_SNAPSHOT */ +#endif/* !USE_MPROTECT_SNAPSHOT */ diff --git a/mymemory.h b/mymemory.h index a62ab83b..aaf54c39 100644 --- a/mymemory.h +++ b/mymemory.h @@ -24,7 +24,7 @@ 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; \ } @@ -43,7 +43,7 @@ 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; \ } @@ -71,15 +71,15 @@ void Thread_free(void *ptr); */ template class ModelAlloc { - public: +public: // 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 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 @@ -140,14 +140,14 @@ class ModelAlloc { /** Return that all specializations of this allocator are interchangeable. */ template bool operator ==(const ModelAlloc&, - const ModelAlloc&) throw() { + const ModelAlloc&) throw() { return true; } /** Return that all specializations of this allocator are interchangeable. */ template bool operator!= (const ModelAlloc&, - const ModelAlloc&) throw() { + const ModelAlloc&) throw() { return false; } @@ -163,15 +163,15 @@ bool operator!= (const ModelAlloc&, */ template class SnapshotAlloc { - public: +public: // 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 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 @@ -232,36 +232,36 @@ class SnapshotAlloc { /** Return that all specializations of this allocator are interchangeable. */ template bool operator ==(const SnapshotAlloc&, - const SnapshotAlloc&) throw() { + const SnapshotAlloc&) throw() { return true; } /** Return that all specializations of this allocator are interchangeable. */ template bool operator!= (const SnapshotAlloc&, - const SnapshotAlloc&) throw() { + const SnapshotAlloc&) throw() { 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 - extern mspace user_snapshot_space; +extern mspace user_snapshot_space; #endif - extern mspace model_snapshot_space; +extern mspace model_snapshot_space; #ifdef __cplusplus -}; /* end of extern "C" */ +}; /* end of extern "C" */ #endif -#endif /* _MY_MEMORY_H */ +#endif/* _MY_MEMORY_H */ diff --git a/nodestack.cc b/nodestack.cc index b9aaf6fd..c1c3cfc5 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -54,7 +54,7 @@ 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]; } @@ -76,7 +76,7 @@ void NodeStack::print() const { 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(); @@ -97,9 +97,9 @@ ModelAction * NodeStack::explore_action(ModelAction *act) /** 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(); diff --git a/nodestack.h b/nodestack.h index edaf397e..c5e6d415 100644 --- a/nodestack.h +++ b/nodestack.h @@ -1,6 +1,6 @@ /** @file nodestack.h * @brief Stack of operations for use in backtracking. -*/ + */ #ifndef __NODESTACK_H__ #define __NODESTACK_H__ @@ -80,4 +80,4 @@ private: int head_idx; }; -#endif /* __NODESTACK_H__ */ +#endif/* __NODESTACK_H__ */ diff --git a/output.h b/output.h index e390bb61..53afb2c5 100644 --- 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(); -#endif /* ! CONFIG_DEBUG */ +#endif/* ! CONFIG_DEBUG */ -#endif /* __OUTPUT_H__ */ +#endif/* __OUTPUT_H__ */ diff --git a/params.h b/params.h index 4f49d81f..597ce1ca 100644 --- a/params.h +++ b/params.h @@ -19,4 +19,4 @@ struct model_params { char **argv; }; -#endif /* __PARAMS_H__ */ +#endif/* __PARAMS_H__ */ diff --git a/pthread.cc b/pthread.cc index 87dc2065..f0f96848 100644 --- a/pthread.cc +++ b/pthread.cc @@ -15,7 +15,7 @@ #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)¶ms); @@ -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; - } + } 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) { - model = new ModelChecker(); + model = new ModelChecker(); } 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(); - /* 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. */ - if (!execution->getMutexMap()->contains(p_mutex)) { + if (!execution->getMutexMap()->contains(p_mutex)) { 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(); } -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); @@ -99,24 +99,24 @@ int pthread_mutex_unlock(pthread_mutex_t *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 /* - 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; } @@ -150,8 +150,8 @@ int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) { 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(); diff --git a/schedule.cc b/schedule.cc index fff26ce2..f26a1a6a 100644 --- 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; - 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) @@ -206,14 +206,14 @@ Thread * Scheduler::select_next_thread(Node *n) { 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) - 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; @@ -254,7 +254,7 @@ void Scheduler::print() const 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); diff --git a/schedule.h b/schedule.h index 6498789a..16ddb341 100644 --- a/schedule.h +++ b/schedule.h @@ -55,4 +55,4 @@ private: Thread *current; }; -#endif /* __SCHEDULE_H__ */ +#endif/* __SCHEDULE_H__ */ diff --git a/snapshot-interface.cc b/snapshot-interface.cc index 5242d168..bf12fe8a 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -22,12 +22,12 @@ struct snapshot_entry { }; class SnapshotStack { - public: +public: int backTrackBeforeStep(int seq_index); void snapshotStep(int seq_index); MEMALLOC - private: +private: ModelVector stack; }; @@ -73,7 +73,7 @@ static void SnapshotGlobalSegments() 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; @@ -141,7 +141,7 @@ static void SnapshotGlobalSegments() 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 diff --git a/snapshot-interface.h b/snapshot-interface.h index 7f4de211..d926c74e 100644 --- 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, - 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); diff --git a/snapshot.cc b/snapshot.cc index 7deaeff4..826046f0 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -40,8 +40,8 @@ struct BackingPageRecord { /* 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 @@ -57,19 +57,19 @@ struct 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 }; @@ -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", - __FILE__, __LINE__); + __FILE__, __LINE__); // print_trace(); // Trace printing may cause dynamic memory allocation - exit(EXIT_FAILURE); + exit(EXIT_FAILURE); } 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); @@ -132,8 +132,8 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused) } 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; @@ -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); - 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); @@ -191,15 +191,15 @@ static void mprot_add_to_snapshot(void *addr, unsigned int numPages) } 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() { - 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"); @@ -220,7 +220,7 @@ static void mprot_roll_back(snapshot_id theID) { #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; @@ -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; - 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); } } - 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)); @@ -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_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 @@ -289,19 +289,19 @@ struct fork_snapshotter { 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; @@ -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, - void (*func)(void)) + void (*func)(void)) { getcontext(ctxt); ctxt->uc_stack.ss_sp = stack; @@ -361,8 +361,8 @@ mspace create_shared_mspace() } 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(); @@ -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, - 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); @@ -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", - getpid(), forkedID, snapshotid); + getpid(), forkedID, snapshotid); 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; } -#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, - 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); diff --git a/stacktrace.h b/stacktrace.h index a3b03509..6444c418 100644 --- 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. - 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] - for (char *p = symbollist[i]; *p; ++p) { + for (char *p = symbollist[i];*p;++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, - funcname, &funcnamesize, &status); + funcname, &funcnamesize, &status); if (status == 0) { - funcname = ret; // use possibly realloc()-ed string + funcname = ret; // use possibly realloc()-ed string 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", - symbollist[i], begin_name, begin_offset); + symbollist[i], begin_name, begin_offset); } } 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); } -#endif // __STACKTRACE_H__ +#endif// __STACKTRACE_H__ diff --git a/stl-model.h b/stl-model.h index ae6e8b27..9fa7cf9f 100644 --- a/stl-model.h +++ b/stl-model.h @@ -8,7 +8,7 @@ template class ModelList : public std::list<_Tp, ModelAlloc<_Tp> > { - public: +public: typedef std::list< _Tp, ModelAlloc<_Tp> > list; ModelList() : @@ -25,7 +25,7 @@ class ModelList : public std::list<_Tp, ModelAlloc<_Tp> > template class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> > { - public: +public: typedef std::list<_Tp, SnapshotAlloc<_Tp> > list; SnapList() : @@ -42,7 +42,7 @@ class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> > template class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> > { - public: +public: typedef std::vector< _Tp, ModelAlloc<_Tp> > vector; ModelVector() : @@ -59,7 +59,7 @@ class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> > template class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> > { - public: +public: typedef std::vector< _Tp, SnapshotAlloc<_Tp> > vector; SnapVector() : @@ -73,4 +73,4 @@ class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> > SNAPSHOTALLOC }; -#endif /* __STL_MODEL_H__ */ +#endif/* __STL_MODEL_H__ */ diff --git a/threads-model.h b/threads-model.h index c6e3a3af..ad178329 100644 --- a/threads-model.h +++ b/threads-model.h @@ -187,4 +187,4 @@ static inline int id_to_int(thread_id_t id) return id; } -#endif /* __THREADS_MODEL_H__ */ +#endif/* __THREADS_MODEL_H__ */ diff --git a/threads.cc b/threads.cc index d1929cd7..b87ae4e4 100644 --- a/threads.cc +++ b/threads.cc @@ -143,7 +143,7 @@ Thread::Thread(thread_id_t 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) { @@ -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"); - 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; - 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; diff --git a/traceanalysis.h b/traceanalysis.h index d363150a..3f8c7688 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -4,12 +4,12 @@ class TraceAnalysis { - public: +public: /** 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. */ -- 2.34.1