remove some datarace code

diff --git a/cmodelint.cc b/cmodelint.cc
index d3b64b156c79b72a27662e2fd6ab92ca3e1a01fc..92eea8514c53dcf8184beaa96f3832f8f36e6d5f 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -95,10 +95,10 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position)
 
 // cds volatile loads
 #define VOLATILELOAD(size) \
-  uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \
-    ensureModel();                                                     \
-    return (uint ## size ## _t) model->switch_to_master(new ModelAction(ATOMIC_READ, position, memory_order_relaxed, obj)); \
-  }
+       uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \
+               ensureModel();                                                      \
+               return (uint ## size ## _t)model->switch_to_master(new ModelAction(ATOMIC_READ, position, memory_order_relaxed, obj)); \
+       }
 
 VOLATILELOAD(8)
 VOLATILELOAD(16)
@@ -107,10 +107,10 @@ VOLATILELOAD(64)
 
 // cds volatile stores
 #define VOLATILESTORE(size) \
-  void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) {        \
-    ensureModel();                                                     \
-    model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, memory_order_relaxed, obj, (uint64_t) val)); \
-}
+       void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \
+               ensureModel();                                                      \
+               model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, memory_order_relaxed, obj, (uint64_t) val)); \
+       }
 
 VOLATILESTORE(8)
 VOLATILESTORE(16)

diff --git a/execution.cc b/execution.cc
index 323c83d36fe4273ddf0d08508af7653abadf3b91..33a608d6fa18f55b869045b67d6485b6332bb1d6 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -27,7 +27,6 @@ struct model_snapshot_members {
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
                bugs(),
-               dataraces(),
                bad_synchronization(false),
                asserted(false)
        { }
@@ -35,16 +34,12 @@ struct model_snapshot_members {
        ~model_snapshot_members() {
                for (unsigned int i = 0;i < bugs.size();i++)
                        delete bugs[i];
-               for (unsigned int i = 0;i < dataraces.size(); i++) 
-                       delete dataraces[i];
                bugs.clear();
-               dataraces.clear();
        }
 
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        SnapVector<bug_message *> bugs;
-       SnapVector<bug_message *> dataraces;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
        bool asserted;
@@ -190,22 +185,6 @@ bool ModelExecution::assert_bug(const char *msg)
        return false;
 }
 
-/* @brief Put data races in a different list from other bugs. The purpose
- *  is to continue the program untill the number of data races exceeds a 
- *  threshold */
-
-/* TODO: check whether set_assert should be called */
-bool ModelExecution::assert_race(const char *msg)
-{
-       priv->dataraces.push_back(new bug_message(msg));
-
-       if (isfeasibleprefix()) {
-               set_assert();
-               return true;
-       }
-       return false;
-}
-
 /** @return True, if any bugs have been reported for this execution */
 bool ModelExecution::have_bug_reports() const
 {
@@ -213,13 +192,13 @@ bool ModelExecution::have_bug_reports() const
 }
 
 /** @return True, if any fatal bugs have been reported for this execution.
- *  Any bug other than a data race is considered a fatal bug. Data races 
+ *  Any bug other than a data race is considered a fatal bug. Data races
  *  are not considered fatal unless the number of races is exceeds
- *  a threshold (temporarily set as 15). 
+ *  a threshold (temporarily set as 15).
  */
 bool ModelExecution::have_fatal_bug_reports() const
 {
-       return priv->bugs.size() != 0 || priv->dataraces.size() >= 15;
+       return priv->bugs.size() != 0;
 }
 
 SnapVector<bug_message *> * ModelExecution::get_bugs() const
@@ -310,8 +289,8 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
        if (hasnonatomicstore) {
-         ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
-         rf_set->push_back(nonatomicstore);
+               ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
+               rf_set->push_back(nonatomicstore);
        }
 
        while(true) {
@@ -1209,7 +1188,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
        insertIntoActionListAndSetCV(&action_trace, act);
-       
+
        action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
        insertIntoActionList(list, act);
 

diff --git a/execution.h b/execution.h
index 74496c67d9eae8538d4ad9eaaf3c1d4345598b8e..f1d3dc56f0085408fc3ffb2c49f55dad2d26e38c 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -68,7 +68,6 @@ public:
        bool check_action_enabled(ModelAction *curr);
 
        bool assert_bug(const char *msg);
-       bool assert_race(const char *msg);
 
        bool have_bug_reports() const;
        bool have_fatal_bug_reports() const;

diff --git a/funcnode.cc b/funcnode.cc
index e07ab9e22b13c9775e591e35ca81eba44fc43252..27a9abd74b8bd653fdb7e97d3aa562683efac8ac 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -40,7 +40,7 @@ FuncInst * FuncNode::get_or_add_action(ModelAction *act)
 
                        func_inst = new FuncInst(act, this);
                        inst->get_collisions()->push_back(func_inst);
-                       inst_list.push_back(func_inst);         // delete?
+                       inst_list.push_back(func_inst); // delete?
 
                        return func_inst;
                }
@@ -126,7 +126,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
        /* Store the memory locations where atomic reads happen */
        bool push_loc = true;
        ModelList<void *>::iterator it;
-       for (it = read_locations.begin(); it != read_locations.end(); it++) {
+       for (it = read_locations.begin();it != read_locations.end();it++) {
                if (location == *it) {
                        push_loc = false;
                        break;
@@ -172,7 +172,7 @@ void FuncNode::print_last_read(uint32_t tid)
        read_map_t * read_map = thrd_read_map[tid];
 
        ModelList<void *>::iterator it;
-       for (it = read_locations.begin(); it != read_locations.end(); it++) {
+       for (it = read_locations.begin();it != read_locations.end();it++) {
                if ( !read_map->contains(*it) )
                        break;
 

diff --git a/history.cc b/history.cc
index 352a9a4cc479065062d684bfc56fe16fbfa88dd7..6b263ad2df01afec5a1e47862d384679e50c442f 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -10,7 +10,7 @@
 
 /** @brief Constructor */
 ModelHistory::ModelHistory() :
-       func_counter(1), /* function id starts with 1 */
+       func_counter(1),        /* function id starts with 1 */
        func_map(),
        func_map_rev(),
        func_nodes()
@@ -136,7 +136,7 @@ FuncNode * ModelHistory::get_func_node(uint32_t func_id)
 void ModelHistory::print()
 {
        /* function id starts with 1 */
-       for (uint32_t i = 1; i < func_nodes.size(); i++) {
+       for (uint32_t i = 1;i < func_nodes.size();i++) {
                FuncNode * func_node = func_nodes[i];
 
                func_inst_list_mt * entry_insts = func_node->get_entry_insts();

diff --git a/model.cc b/model.cc
index cfbc3b8606243e1cf558a1e7a2a48d0bd3c70967..45fa1b20ff11462c7999090a34e34f31212b049d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -139,28 +139,6 @@ bool ModelChecker::assert_bug(const char *msg, ...)
        return execution->assert_bug(str);
 }
 
-/**
- * @brief Assert a data race in the executing program.
- *
- * Different from assert_bug, the program will not be aborted immediately
- * upon calling this function, unless the number of data races exceeds
- * a threshold.
- *
- * @param msg Descriptive message for the bug (do not include newline char)
- * @return True if bug is immediately-feasible
- */
-bool ModelChecker::assert_race(const char *msg, ...)
-{
-       char str[800];
-
-       va_list ap;
-       va_start(ap, msg);
-       vsnprintf(str, sizeof(str), msg, ap);
-       va_end(ap);
-
-       return execution->assert_race(str);
-}
-
 /**
  * @brief Assert a bug in the executing program, asserted by a user thread
  * @see ModelChecker::assert_bug

diff --git a/model.h b/model.h
index a37bd49d5e0deb818cdfa833336140554fa984a8..9fb94228a3a9f6460a17dbe6f74754062a5934f8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -59,7 +59,6 @@ public:
        uint64_t switch_to_master(ModelAction *act);
 
        bool assert_bug(const char *msg, ...);
-       bool assert_race(const char *msg, ...);
 
        void assert_user_bug(const char *msg);