Add macro for recording atomic statics and report data races

diff --git a/config.h b/config.h
index f86275a725a15344507dfbc46598e28fc95ba339..1d0f59f6581b7f255dbccb1b45a34b90e19760ce 100644 (file)
--- a/config.h
+++ b/config.h
@@ -63,4 +63,7 @@
 //#define memory_order_volatile_load memory_order_relaxed
 //#define memory_order_volatile_store memory_order_relaxed
 
+//#define COLLECT_STAT
+#define REPORT_DATA_RACES
+
 #endif

diff --git a/datarace.cc b/datarace.cc
index f988596f492343f7db2519cf5a83af3bce41821e..544fced0485690e67aabee2d56f8fcbf47d16b1c 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -16,6 +16,7 @@ static void *memory_base;
 static void *memory_top;
 static RaceSet * raceset;
 
+#ifdef COLLECT_STAT
 static unsigned int store8_count = 0;
 static unsigned int store16_count = 0;
 static unsigned int store32_count = 0;
@@ -25,6 +26,7 @@ static unsigned int load8_count = 0;
 static unsigned int load16_count = 0;
 static unsigned int load32_count = 0;
 static unsigned int load64_count = 0;
+#endif
 
 static const ModelExecution * get_execution()
 {
@@ -1212,6 +1214,7 @@ void raceCheckWrite8(thread_id_t thread, const void *location)
        raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
 }
 
+#ifdef COLLECT_STAT
 void print_normal_accesses()
 {
        model_print("store 8  count: %u\n", store8_count);
@@ -1224,3 +1227,4 @@ void print_normal_accesses()
        model_print("load  32 count: %u\n", load32_count);
        model_print("load  64 count: %u\n", load64_count);
 }
+#endif

diff --git a/datarace.h b/datarace.h
index c36af066deceec59e6e2d14e9f0c1ada872dcdc0..34bfd4067dc99ad591a21d1ca621ca5498f0ff67 100644 (file)
--- a/datarace.h
+++ b/datarace.h
@@ -65,6 +65,10 @@ void raceCheckWrite16(thread_id_t thread, const void *location);
 void raceCheckWrite32(thread_id_t thread, const void *location);
 void raceCheckWrite64(thread_id_t thread, const void *location);
 
+#ifdef COLLECT_STAT
+void print_normal_accesses();
+#endif
+
 /**
  * @brief A record of information for detecting data races
  */

diff --git a/execution.cc b/execution.cc
index 04314d194c17058713d1107911b7377b692c5a25..05c5842faf486d6bde5162a76c708397423b6aeb 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -19,6 +19,20 @@
 
 #define INITIAL_THREAD_ID       0
 
+#ifdef COLLECT_STAT
+static unsigned int atomic_load_count = 0;
+static unsigned int atomic_store_count = 0;
+static unsigned int atomic_rmw_count = 0;
+
+static unsigned int atomic_fence_count = 0;
+static unsigned int atomic_lock_count = 0;
+static unsigned int atomic_trylock_count = 0;
+static unsigned int atomic_unlock_count = 0;
+static unsigned int atomic_notify_count = 0;
+static unsigned int atomic_wait_count = 0;
+static unsigned int atomic_timedwait_count = 0;
+#endif
+
 /**
  * Structure for holding small ModelChecker members that should be snapshotted
  */
@@ -133,7 +147,7 @@ static SnapVector<simple_action_list_t> * get_safe_ptr_vect_action(HashTable<con
  * action lists may change. Hence we need to fix the parent pointer of the children
  * of root.
  */
-static void fixup_action_list (SnapVector<action_list_t> * vec)
+static void fixup_action_list(SnapVector<action_list_t> * vec)
 {
        for (uint i = 0; i < vec->size(); i++) {
                action_list_t * list = &(*vec)[i];
@@ -142,6 +156,60 @@ static void fixup_action_list (SnapVector<action_list_t> * vec)
        }
 }
 
+#ifdef COLLECT_STAT
+static inline void record_atomic_stats(ModelAction * act)
+{
+       switch (act->get_type()) {
+               case ATOMIC_WRITE:
+                       atomic_store_count++;
+                       break;
+               case ATOMIC_RMW:
+                       atomic_load_count++;
+                       break;
+               case ATOMIC_READ:
+                       atomic_rmw_count++;
+                       break;
+               case ATOMIC_FENCE:
+                       atomic_fence_count++;
+                       break;
+               case ATOMIC_LOCK:
+                       atomic_lock_count++;
+                       break;
+               case ATOMIC_TRYLOCK:
+                       atomic_trylock_count++;
+                       break;
+               case ATOMIC_UNLOCK:
+                       atomic_unlock_count++;
+                       break;
+               case ATOMIC_NOTIFY_ONE:
+               case ATOMIC_NOTIFY_ALL:
+                       atomic_notify_count++;
+                       break;
+               case ATOMIC_WAIT:
+                       atomic_wait_count++;
+                       break;
+               case ATOMIC_TIMEDWAIT:
+                       atomic_timedwait_count++;
+               default:
+                       return;
+       }
+}
+
+void print_atomic_accesses()
+{
+       model_print("atomic store  count: %u\n", atomic_store_count);
+       model_print("atomic load   count: %u\n", atomic_load_count);
+       model_print("atomic rmw    count: %u\n", atomic_rmw_count);
+
+       model_print("atomic fence  count: %u\n", atomic_fence_count);
+       model_print("atomic lock   count: %u\n", atomic_lock_count);
+       model_print("atomic trylock count: %u\n", atomic_trylock_count);
+       model_print("atomic unlock count: %u\n", atomic_unlock_count);
+       model_print("atomic notify count: %u\n", atomic_notify_count);
+       model_print("atomic wait   count: %u\n", atomic_wait_count);
+       model_print("atomic timedwait count: %u\n", atomic_timedwait_count);
+}
+#endif
 /** @return a thread ID for a new Thread */
 thread_id_t ModelExecution::get_next_id()
 {
@@ -572,7 +640,7 @@ void ModelExecution::process_thread_action(ModelAction *curr)
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
-               break;  // WL: to be add (modified)
+               break;
        }
 
        case THREADONLY_FINISH:
@@ -761,8 +829,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                ASSERT(rf_set == NULL);
 
        /* Add the action to lists */
-       if (!second_part_of_rmw)
+       if (!second_part_of_rmw) {
+#ifdef COLLECT_STAT
+               record_atomic_stats(curr);
+#endif
                add_action_to_lists(curr, canprune);
+       }
 
        if (curr->is_write())
                add_write_to_lists(curr);

diff --git a/execution.h b/execution.h
index 5cd54469c6d3c920b1fda9ab7cecc54ca2de4f29..5158b2a677e9df79e41bd050e045cc0ec15c48ce 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -27,6 +27,10 @@ struct PendingFutureValue {
        ModelAction *reader;
 };
 
+#ifdef COLLECT_STAT
+void print_atomic_accesses();
+#endif
+
 /** @brief The central structure for model-checking */
 class ModelExecution {
 public: