From: weiyu Date: Thu, 16 Jan 2020 02:04:37 +0000 (-0800) Subject: Toward transferring the removal of some actions from ModelExecution to FuncNode or... X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=df55261fc251d7b6f15086393911530af340eaf4 Toward transferring the removal of some actions from ModelExecution to FuncNode or ModelHistory --- diff --git a/action.cc b/action.cc index d6569544..85a2a766 100644 --- a/action.cc +++ b/action.cc @@ -41,8 +41,10 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, trace_ref(NULL), thrdmap_ref(NULL), action_ref(NULL), + func_act_ref(NULL), value(value), type(type), + original_type(ATOMIC_NOP), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -77,6 +79,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, action_ref(NULL), value(value), type(type), + original_type(ATOMIC_NOP), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -110,6 +113,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, action_ref(NULL), value(value), type(type), + original_type(ATOMIC_NOP), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -147,6 +151,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order action_ref(NULL), value(value), type(type), + original_type(ATOMIC_NOP), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -185,6 +190,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order action_ref(NULL), value(value), type(type), + original_type(ATOMIC_NOP), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -772,3 +778,11 @@ cdsc::mutex * ModelAction::get_mutex() const else return NULL; } + +/** @brief Swap type with original type */ +void ModelAction::use_original_type() +{ + action_type_t tmp = type; + type = original_type; + original_type = tmp; +} diff --git a/action.h b/action.h index 66e11906..e830a74e 100644 --- a/action.h +++ b/action.h @@ -34,6 +34,7 @@ using std::memory_order_seq_cst; * iteself does not indicate no value. */ #define VALUE_NONE 0xdeadbeef +#define HAS_REFERENCE ((void *)0x1) /** * @brief The "location" at which a fence occurs @@ -103,6 +104,8 @@ public: thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } void set_type(action_type _type) { type = _type; } + action_type get_original_type() const { return type; } + void set_original_type(action_type _type) { original_type = _type; } void set_free() { type = READY_FREE; } memory_order get_mo() const { return order; } memory_order get_original_mo() const { return original_order; } @@ -188,15 +191,20 @@ public: bool equals(const ModelAction *x) const { return this == x; } void set_value(uint64_t val) { value = val; } + void use_original_type(); + /* to accomodate pthread create and join */ Thread * thread_operand; void set_thread_operand(Thread *th) { thread_operand = th; } void setTraceRef(sllnode *ref) { trace_ref = ref; } void setThrdMapRef(sllnode *ref) { thrdmap_ref = ref; } void setActionRef(sllnode *ref) { action_ref = ref; } + void setFuncActRef(void *ref) { func_act_ref = ref; } sllnode * getTraceRef() { return trace_ref; } sllnode * getThrdMapRef() { return thrdmap_ref; } sllnode * getActionRef() { return action_ref; } + void * getFuncActRef() { return func_act_ref; } + SNAPSHOTALLOC private: const char * get_type_str() const; @@ -234,7 +242,7 @@ private: sllnode * trace_ref; sllnode * thrdmap_ref; sllnode * action_ref; - + void * func_act_ref; /** @brief The value written (for write or RMW; undefined for read) */ uint64_t value; @@ -242,6 +250,10 @@ private: /** @brief Type of action (read, write, RMW, fence, thread create, etc.) */ action_type type; + /** @brief The original type of action (read, write, RMW) before it was + * set as READY_FREE or weaken from a RMW to a write */ + action_type original_type; + /** @brief The memory order for this operation. */ memory_order order; diff --git a/execution.cc b/execution.cc index 8057aa99..47edb31a 100644 --- a/execution.cc +++ b/execution.cc @@ -58,7 +58,10 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : obj_map(), condvar_waiters_map(), obj_thrd_map(), + obj_wr_thrd_map(), + obj_last_sc_map(), mutex_map(), + cond_map(), thrd_last_action(1), thrd_last_fence_release(), priv(new struct model_snapshot_members ()), @@ -1612,7 +1615,7 @@ bool ModelExecution::is_enabled(thread_id_t tid) const Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const { /* Do not split atomic RMW */ - if (curr->is_rmwr() && !paused_by_fuzzer(curr)) + if (curr->is_rmwr()) return get_thread(curr); /* Follow CREATE with the created thread */ /* which is not needed, because model.cc takes care of this */ @@ -1624,15 +1627,6 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons return NULL; } -/** @param act A read atomic action */ -bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const -{ - ASSERT(act->is_read()); - - // Actions paused by fuzzer have their sequence number reset to 0 - return act->get_seq_number() == 0; -} - /** * Takes the next step in the execution, if possible. * @param curr The current step to take @@ -1735,6 +1729,9 @@ void ModelExecution::fixupLastAct(ModelAction *act) { /** Compute which actions to free. */ void ModelExecution::collectActions() { + if (priv->used_sequence_numbers < params->traceminsize) + return; + //Compute minimal clock vector for all live threads ClockVector *cvmin = computeMinimalCV(); SnapVector * queue = new SnapVector(); @@ -1758,6 +1755,13 @@ void ModelExecution::collectActions() { //Free if it is invisible or we have set a flag to remove visible actions. if (actseq <= tid_clock || params->removevisible) { + // For read actions being used by ModelHistory, mark the reads_from as being used. + if (act->is_read() && act->getFuncActRef() != NULL) { + ModelAction * reads_from = act->get_reads_from(); + if (reads_from->getFuncActRef() == NULL) + reads_from->setFuncActRef(HAS_REFERENCE); + } + ModelAction * write; if (act->is_write()) { write = act; @@ -1777,6 +1781,10 @@ void ModelExecution::collectActions() { CycleNode * prevnode = node->getInEdge(i); ModelAction * prevact = prevnode->getAction(); if (prevact->get_type() != READY_FREE) { + if (prevact->getFuncActRef() != NULL) { + // Copy the original type if being used by ModelHistory + prevact->set_original_type(prevact->get_type()); + } prevact->set_free(); queue->push_back(prevnode); } @@ -1800,8 +1808,19 @@ void ModelExecution::collectActions() { } if (act->is_read()) { + // For read actions being used by ModelHistory, mark the reads_from as being used. + if (act->getFuncActRef() != NULL) { + ModelAction * reads_from = act->get_reads_from(); + if (reads_from->getFuncActRef() == NULL) + reads_from->setFuncActRef(HAS_REFERENCE); + } + if (act->get_reads_from()->is_free()) { if (act->is_rmw()) { + if (act->getFuncActRef() != NULL) { + // Copy the original type if being used by ModelHistory + act->set_original_type(act->get_type()); + } //Weaken a RMW from a freed store to a write act->set_type(ATOMIC_WRITE); } else { @@ -1809,8 +1828,13 @@ void ModelExecution::collectActions() { if (islastact) { fixupLastAct(act); } - delete act; - continue; + + //Only delete this action if not being using by ModelHistory. + //Otherwise, the deletion of action is deferred. + if (act->getFuncActRef() == NULL) { + delete act; + continue; + } } } } @@ -1841,14 +1865,20 @@ void ModelExecution::collectActions() { if (act->is_read()) { if (act->get_reads_from()->is_free()) { if (act->is_rmw()) { + if (act->getFuncActRef() != NULL) { + // Copy the original type if being used by ModelHistory + act->set_original_type(act->get_type()); + } act->set_type(ATOMIC_WRITE); } else { removeAction(act); if (islastact) { fixupLastAct(act); } - delete act; - continue; + if (act->getFuncActRef() == NULL) { + delete act; + continue; + } } } } else if (act->is_free()) { @@ -1856,8 +1886,10 @@ void ModelExecution::collectActions() { if (islastact) { fixupLastAct(act); } - delete act; - continue; + if (act->getFuncActRef() == NULL) { + delete act; + continue; + } } else if (act->is_write()) { //Do nothing with write that hasn't been marked to be freed } else if (islastact) { diff --git a/execution.h b/execution.h index 008e1e11..6cdaeaf1 100644 --- a/execution.h +++ b/execution.h @@ -202,7 +202,6 @@ private: Fuzzer * fuzzer; Thread * action_select_next_thread(const ModelAction *curr) const; - bool paused_by_fuzzer(const ModelAction * act) const; bool isfinished; }; diff --git a/funcnode.cc b/funcnode.cc index dc903ef8..69d8b80e 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -184,6 +184,7 @@ void FuncNode::update_tree(action_list_t * act_list) for (sllnode * it = act_list->begin();it != NULL;it = it->getNext()) { ModelAction * act = it->getVal(); + act->setFuncActRef(NULL); // Remove func_act_ref so that this action can be removed FuncInst * func_inst = get_inst(act); void * loc = act->get_location(); diff --git a/history.cc b/history.cc index c15bb26f..32aacf70 100644 --- a/history.cc +++ b/history.cc @@ -79,7 +79,7 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) } /* Monitor the statuses of threads waiting for tid */ - monitor_waiting_thread(func_id, tid); + // monitor_waiting_thread(func_id, tid); } /* @param func_id a non-zero value */ @@ -146,7 +146,7 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) return; /* Monitor the statuses of threads waiting for tid */ - monitor_waiting_thread_counter(tid); + // monitor_waiting_thread_counter(tid); /* Every write action should be processed, including * nonatomic writes (which have no position) */ @@ -181,7 +181,7 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) return; /* Add to curr_inst_list */ - curr_act_list->push_back(act); + act->setFuncActRef(curr_act_list->add_back(act)); FuncNode * func_node = func_nodes[func_id]; func_node->add_inst(act);