From 98d08ddaa7c248c7c968c1158eb691dc029a1f81 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Mon, 6 Jan 2020 16:04:49 -0800 Subject: [PATCH] My configuration --- cmodelint.cc | 8 ++++++-- config.h | 10 ++++++++++ execution.cc | 9 ++++++++- 3 files changed, 24 insertions(+), 3 deletions(-) diff --git a/cmodelint.cc b/cmodelint.cc index ea34324b..d3fcbb46 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -97,7 +97,7 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) #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)); \ + return (uint ## size ## _t)model->switch_to_master(new ModelAction(ATOMIC_READ, position, memory_order_volatile_load, obj)); \ } VOLATILELOAD(8) @@ -109,7 +109,7 @@ VOLATILELOAD(64) #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)); \ + model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, memory_order_volatile_store, obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ thread_id_t tid = thread_current()->get_id(); \ for(int i=0;i < size / 8;i++) { \ @@ -340,6 +340,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { */ void cds_func_entry(const char * funcName) { +#ifdef NEWFUZZER ensureModel(); Thread * th = thread_current(); uint32_t func_id; @@ -362,9 +363,11 @@ void cds_func_entry(const char * funcName) { } history->enter_function(func_id, th->get_id()); +#endif } void cds_func_exit(const char * funcName) { +#ifdef NEWFUZZER ensureModel(); Thread * th = thread_current(); @@ -382,4 +385,5 @@ void cds_func_exit(const char * funcName) { return; history->exit_function(func_id, th->get_id()); +#endif } diff --git a/config.h b/config.h index 7ed00f09..f86275a7 100644 --- a/config.h +++ b/config.h @@ -53,4 +53,14 @@ /** Enable mitigations against fork handlers that call into locks... */ #define FORK_HANDLER_HACK +/** Enable smart fuzzer */ +//#define NEWFUZZER + +/** Define semantics of volatile memory operations. */ +#define memory_order_volatile_load memory_order_acquire +#define memory_order_volatile_store memory_order_release + +//#define memory_order_volatile_load memory_order_relaxed +//#define memory_order_volatile_store memory_order_relaxed + #endif diff --git a/execution.cc b/execution.cc index a76a3e18..8853bfee 100644 --- a/execution.cc +++ b/execution.cc @@ -63,7 +63,11 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : thrd_last_fence_release(), priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), +#ifdef NEWFUZZER + fuzzer(new NewFuzzer()), +#else fuzzer(new Fuzzer()), +#endif isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ @@ -275,7 +279,9 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { add_normal_write_to_lists(act); add_write_to_lists(act); w_modification_order(act); +#ifdef NEWFUZZER model->get_history()->process_action(act, act->get_tid()); +#endif return act; } @@ -1643,8 +1649,9 @@ Thread * ModelExecution::take_step(ModelAction *curr) ASSERT(curr); /* Process this action in ModelHistory for records */ +#ifdef NEWFUZZER model->get_history()->process_action( curr, curr->get_tid() ); - +#endif if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd); -- 2.34.1