From 509ea2631fffda65d966c4ddd1e18a5c2eda89c0 Mon Sep 17 00:00:00 2001 From: weiyu Date: Fri, 10 Jul 2020 15:45:18 -0700 Subject: [PATCH] Add macro for recording atomic statics and report data races --- config.h | 3 ++ datarace.cc | 4 +++ datarace.h | 4 +++ execution.cc | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++-- execution.h | 4 +++ 5 files changed, 90 insertions(+), 3 deletions(-) diff --git a/config.h b/config.h index f86275a7..1d0f59f6 100644 --- 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 f988596f..544fced0 100644 --- 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 c36af066..34bfd406 100644 --- 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 04314d19..05c5842f 100644 --- 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 * get_safe_ptr_vect_action(HashTable * vec) +static void fixup_action_list(SnapVector * 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 * 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 5cd54469..5158b2a6 100644 --- 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: -- 2.34.1