spacing

diff --git a/action.cc b/action.cc
index a313b70fbe970810c96fe16bc1d7a0a27108508b..e88fceef66a8d173e851f4439afd55f1d96564f4 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -264,7 +264,7 @@ void ModelAction::process_rmw(ModelAction * act) {
  */
 bool ModelAction::could_synchronize_with(const ModelAction *act) const
 {
-       //Same thread can't be reordered
+       // Same thread can't be reordered
        if (same_thread(act))
                return false;
 
@@ -283,15 +283,15 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const
                        (act->could_be_write() || act->is_fence()))
                return true;
 
-       //lock just released...we can grab lock
+       // lock just released...we can grab lock
        if ((is_lock() ||is_trylock()) && (act->is_unlock()||act->is_wait()))
                return true;
 
-       //lock just acquired...we can fail to grab lock
+       // lock just acquired...we can fail to grab lock
        if (is_trylock() && act->is_success_lock())
                return true;
 
-       //other thread stalling on lock...we can release lock
+       // other thread stalling on lock...we can release lock
        if (is_unlock() && (act->is_trylock()||act->is_lock()))
                return true;
 
@@ -310,19 +310,19 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const
 
 bool ModelAction::is_conflicting_lock(const ModelAction *act) const
 {
-       //Must be different threads to reorder
+       // Must be different threads to reorder
        if (same_thread(act))
                return false;
        
-       //Try to reorder a lock past a successful lock
+       // Try to reorder a lock past a successful lock
        if (act->is_success_lock())
                return true;
        
-       //Try to push a successful trylock past an unlock
+       // Try to push a successful trylock past an unlock
        if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
                return true;
 
-       //Try to push a successful trylock past a wait
+       // Try to push a successful trylock past a wait
        if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS)
                return true;
 

diff --git a/action.h b/action.h
index a246123c259d002d04eb14b1b0a4d63048e12fb6..5ec109883118af17cc3abf860594d58383ab0909 100644 (file)
--- a/action.h
+++ b/action.h
@@ -24,12 +24,10 @@ using std::memory_order_acq_rel;
 using std::memory_order_seq_cst;
 
 /** Note that this value can be legitimately used by a program, and
-               hence by iteself does not indicate no value. */
-
+ *  hence by iteself does not indicate no value. */
 #define VALUE_NONE 0xdeadbeef
 
 /** A special value to represent a successful trylock */
-
 #define VALUE_TRYSUCCESS 1
 
 /** A special value to represent a failed trylock */

diff --git a/model.cc b/model.cc
index c38c79caa24b81f04e67d3069de2f32351aa0aac..e4b6431336050c89043f45851214c632b2e943ce 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -129,19 +129,21 @@ ModelChecker::~ModelChecker()
        delete priv;
 }
 
-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
-       action_list_t * tmp=hash->get(ptr);
-       if (tmp==NULL) {
-               tmp=new action_list_t();
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
+{
+       action_list_t *tmp = hash->get(ptr);
+       if (tmp == NULL) {
+               tmp = new action_list_t();
                hash->put(ptr, tmp);
        }
        return tmp;
 }
 
-static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr) {
-       std::vector<action_list_t> * tmp=hash->get(ptr);
-       if (tmp==NULL) {
-               tmp=new std::vector<action_list_t>();
+static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+{
+       std::vector<action_list_t> *tmp = hash->get(ptr);
+       if (tmp == NULL) {
+               tmp = new std::vector<action_list_t>();
                hash->put(ptr, tmp);
        }
        return tmp;
@@ -208,7 +210,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 {
        thread_id_t tid;
 
-       if (curr!=NULL) {
+       if (curr != NULL) {
                /* Do not split atomic actions. */
                if (curr->is_rmwr())
                        return thread_current();
@@ -283,10 +285,11 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
  * the corresponding thread object's pending action.
  */
 
-void ModelChecker::execute_sleep_set() {
-       for(unsigned int i=0;i<get_num_threads();i++) {
-               thread_id_t tid=int_to_id(i);
-               Thread *thr=get_thread(tid);
+void ModelChecker::execute_sleep_set()
+{
+       for (unsigned int i = 0; i < get_num_threads(); i++) {
+               thread_id_t tid = int_to_id(i);
+               Thread *thr = get_thread(tid);
                if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
                        thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
@@ -602,11 +605,11 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 void ModelChecker::set_backtracking(ModelAction *act)
 {
        Thread *t = get_thread(act);
-       ModelAction * prev = get_last_conflict(act);
+       ModelAction *prev = get_last_conflict(act);
        if (prev == NULL)
                return;
 
-       Node * node = prev->get_node()->get_parent();
+       Node *node = prev->get_node()->get_parent();
 
        int low_tid, high_tid;
        if (node->is_enabled(t)) {
@@ -1136,8 +1139,8 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
  */
 bool ModelChecker::check_action_enabled(ModelAction *curr) {
        if (curr->is_lock()) {
-               std::mutex * lock = (std::mutex *)curr->get_location();
-               struct std::mutex_state * state = lock->get_state();
+               std::mutex *lock = (std::mutex *)curr->get_location();
+               struct std::mutex_state *state = lock->get_state();
                if (state->islocked) {
                        //Stick the action in the appropriate waiting queue
                        get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
@@ -1271,7 +1274,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
-void ModelChecker::check_curr_backtracking(ModelAction * curr) {
+void ModelChecker::check_curr_backtracking(ModelAction *curr)
+{
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
 
@@ -1383,9 +1387,9 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  *
  * If so, we decide that the execution is no longer feasible.
  */
-void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
+void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
+{
        if (params.maxreads != 0) {
-
                if (curr->get_node()->get_read_from_size() <= 1)
                        return;
                //Must make sure that execution is currently feasible...  We could
@@ -1411,7 +1415,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                //See if we have enough reads from the same value
                int count = 0;
                for (; count < params.maxreads; rit++,count++) {
-                       if (rit==list->rend())
+                       if (rit == list->rend())
                                return;
                        ModelAction *act = *rit;
                        if (!act->is_read())
@@ -1422,12 +1426,12 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                        if (act->get_node()->get_read_from_size() <= 1)
                                return;
                }
-               for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
-                       //Get write
-                       const ModelAction * write = curr->get_node()->get_read_from_at(i);
+               for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
+                       /* Get write */
+                       const ModelAction *write = curr->get_node()->get_read_from_at(i);
 
-                       //Need a different write
-                       if (write==rf)
+                       /* Need a different write */
+                       if (write == rf)
                                continue;
 
                        /* Test to see whether this is a feasible write to read from*/
@@ -1444,7 +1448,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                        //new we need to see if this write works for everyone
 
                        for (int loop = count; loop>0; loop--,rit++) {
-                               ModelAction *act=*rit;
+                               ModelAction *act = *rit;
                                bool foundvalue = false;
                                for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
                                        if (act->get_node()->get_read_from_at(j)==write) {
@@ -1762,7 +1766,8 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 /** Arbitrary reads from the future are not allowed.  Section 29.3
  * part 9 places some constraints.  This method checks one result of constraint
  * constraint.  Others require compiler support. */
-bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
        if (!writer->is_rmw())
                return true;
 
@@ -2377,14 +2382,14 @@ void ModelChecker::check_promises_thread_disabled() {
  * cannot perform a future write that will resolve the promise due to
  * modificatin order constraints.
  *
- *     @parem tid The thread that either read from the model action
+ *     @param tid The thread that either read from the model action
  *     write, or actually did the model action write.
  *
- *     @parem write The ModelAction representing the relevant write.
+ *     @param write The ModelAction representing the relevant write.
  */
-
-void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
-       void * location = write->get_location();
+void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
+{
+       void *location = write->get_location();
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
                const ModelAction *act = promise->get_action();
@@ -2509,20 +2514,21 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        }
 }
 
-bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
+bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
+{
        while (true) {
                /* UNINIT actions don't have a Node, and they never sleep */
                if (write->is_uninitialized())
                        return true;
-               Node *prevnode=write->get_node()->get_parent();
+               Node *prevnode = write->get_node()->get_parent();
 
-               bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
-               if (write->is_release()&&thread_sleep)
+               bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
+               if (write->is_release() && thread_sleep)
                        return true;
                if (!write->is_rmw()) {
                        return false;
                }
-               if (write->get_reads_from()==NULL)
+               if (write->get_reads_from() == NULL)
                        return true;
                write=write->get_reads_from();
        }

diff --git a/model.h b/model.h
index af6802a0216612dab30b412d2955fbd1d85f25c3..4f139878ce00300f4252c1705537deabd7643a5f 100644 (file)
--- a/model.h
+++ b/model.h
@@ -121,7 +121,7 @@ public:
        ModelAction * get_parent_action(thread_id_t tid) const;
        void check_promises_thread_disabled();
        void mo_check_promises(thread_id_t tid, const ModelAction *write);
-       void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
+       void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
        bool isfeasibleprefix() const;
 
        bool assert_bug(const char *msg);
@@ -135,15 +135,15 @@ private:
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler *scheduler;
 
-       bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
-       bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
-       bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
+       bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
+       bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader);
+       bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
        bool has_asserted() const;
        void set_assert();
        void set_bad_synchronization();
        bool promises_expired() const;
        void execute_sleep_set();
-       void wake_up_sleeping_actions(ModelAction * curr);
+       void wake_up_sleeping_actions(ModelAction *curr);
        modelclock_t get_next_seq_num();
 
        bool next_execution();
@@ -171,7 +171,7 @@ private:
        void compute_promises(ModelAction *curr);
        void compute_relseq_breakwrites(ModelAction *curr);
 
-       void check_curr_backtracking(ModelAction * curr);
+       void check_curr_backtracking(ModelAction *curr);
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid) const;
        ModelAction * get_last_fence_release(thread_id_t tid) const;