Improve the algorithm that marks which actions are needed by FuncNode

diff --git a/action.cc b/action.cc
index 85a2a766b3583eabb2504bdc5537348520a840b9..df73d2099cc7641be668e03878bfc29f61e190fc 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -45,6 +45,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        value(value),
        type(type),
        original_type(ATOMIC_NOP),
+       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -77,9 +78,11 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value,
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
+       func_act_ref(NULL),
        value(value),
        type(type),
        original_type(ATOMIC_NOP),
+       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -111,9 +114,11 @@ 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),
+       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -149,9 +154,11 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
+       func_act_ref(NULL),
        value(value),
        type(type),
        original_type(ATOMIC_NOP),
+       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -188,9 +195,11 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
+       func_act_ref(NULL),
        value(value),
        type(type),
        original_type(ATOMIC_NOP),
+       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -614,7 +623,7 @@ uint64_t ModelAction::get_reads_from_value() const
  */
 uint64_t ModelAction::get_write_value() const
 {
-       ASSERT(is_write());
+       ASSERT(is_write() || is_free());
        return value;
 }
 
@@ -785,4 +794,9 @@ void ModelAction::use_original_type()
        action_type_t tmp = type;
        type = original_type;
        original_type = tmp;
+
+       if (swap_flag)
+               swap_flag = false;
+       else
+               swap_flag = true;
 }

diff --git a/action.h b/action.h
index e830a74e6093ab58ccbf35bc4718537d70ed9440..67c1ae81e8dccacaaad1a80393d0257e20dc53dc 100644 (file)
--- a/action.h
+++ b/action.h
@@ -34,7 +34,7 @@ using std::memory_order_seq_cst;
  * iteself does not indicate no value.
  */
 #define VALUE_NONE 0xdeadbeef
-#define HAS_REFERENCE ((void *)0x1)
+#define WRITE_REFERENCED ((void *)0x1)
 
 /**
  * @brief The "location" at which a fence occurs
@@ -104,7 +104,7 @@ 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; }
+       action_type get_original_type() const { return original_type; }
        void set_original_type(action_type _type) { original_type = _type; }
        void set_free() { type = READY_FREE; }
        memory_order get_mo() const { return order; }
@@ -120,6 +120,7 @@ public:
        ModelAction * get_reads_from() const { return reads_from; }
        uint64_t get_time() const {return time;}
        cdsc::mutex * get_mutex() const;
+       bool get_swap_flag() const { return swap_flag; }
 
        void set_read_from(ModelAction *act);
 
@@ -254,6 +255,10 @@ private:
         * set as READY_FREE or weaken from a RMW to a write */
        action_type original_type;
 
+       /** @brief Indicate whether the action type and the original action type 
+        *  has been swapped. */
+       bool swap_flag;
+
        /** @brief The memory order for this operation. */
        memory_order order;
 

diff --git a/execution.cc b/execution.cc
index 47edb31a3bc270db9a82521984aafcd18baa1f9b..796e9b74840ccb52233a55b16abacc843f408fba 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1755,11 +1755,25 @@ 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);
+                       // For read or rmw actions being used by ModelHistory, mark the reads_from as being used. 
+                       if (act->is_read()) {
+                               if (act->is_rmw()) {
+                                       void * func_act_ref = act->getFuncActRef();
+                                       if (func_act_ref == WRITE_REFERENCED) {
+                                               // Only the write part of this rmw is referenced, do nothing
+                                       } else if (func_act_ref != NULL) {
+                                               // The read part of rmw is potentially referenced
+                                               ModelAction * reads_from = act->get_reads_from();
+                                               if (reads_from->getFuncActRef() == NULL)
+                                                       reads_from->setFuncActRef(WRITE_REFERENCED);
+                                       }
+                               } else {
+                                       if (act->getFuncActRef() != NULL) {
+                                               ModelAction * reads_from = act->get_reads_from();
+                                               if (reads_from->getFuncActRef() == NULL)
+                                                       reads_from->setFuncActRef(WRITE_REFERENCED);
+                                       }
+                               }
                        }
 
                        ModelAction * write;
@@ -1781,10 +1795,8 @@ 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());
-                                                       }
+                                                       // Save the original action type
+                                                       prevact->set_original_type(prevact->get_type());
                                                        prevact->set_free();
                                                        queue->push_back(prevnode);
                                                }
@@ -1808,19 +1820,29 @@ 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);
+                       // For read or rmw actions being used by ModelHistory, mark the reads_from as being used. 
+                       if (act->is_rmw()) {
+                               void * func_act_ref = act->getFuncActRef();
+                               if (func_act_ref == WRITE_REFERENCED) {
+                                       // Only the write part of this rmw is referenced, do nothing
+                               } else if (func_act_ref != NULL) {
+                                       // The read part of rmw is potentially referenced
+                                       ModelAction * reads_from = act->get_reads_from();
+                                       if (reads_from->getFuncActRef() == NULL)
+                                               reads_from->setFuncActRef(WRITE_REFERENCED);
+                               }
+                       } else {
+                               if (act->getFuncActRef() != NULL) {
+                                       ModelAction * reads_from = act->get_reads_from();
+                                       if (reads_from->getFuncActRef() == NULL)
+                                               reads_from->setFuncActRef(WRITE_REFERENCED);
+                               }
                        }
 
                        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());
-                                       }
+                                       // Save the original action type
+                                       act->set_original_type(act->get_type());
                                        //Weaken a RMW from a freed store to a write
                                        act->set_type(ATOMIC_WRITE);
                                } else {
@@ -1829,8 +1851,8 @@ void ModelExecution::collectActions() {
                                                fixupLastAct(act);
                                        }
 
-                                       //Only delete this action if not being using by ModelHistory.
-                                       //Otherwise, the deletion of action is deferred. 
+                                       // Only delete this action if not being using by ModelHistory.
+                                       // Otherwise, the deletion of action is deferred.
                                        if (act->getFuncActRef() == NULL) {
                                                delete act;
                                                continue;
@@ -1865,10 +1887,8 @@ 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());
-                                       }
+                                       // Save the original action type
+                                       act->set_original_type(act->get_type());
                                        act->set_type(ATOMIC_WRITE);
                                } else {
                                        removeAction(act);

diff --git a/funcnode.cc b/funcnode.cc
index 69d8b80e4694fd54804d3070da62eae14ca6cbf2..63dd382be236d40ec8e74be45186c0acb81947bb 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -184,7 +184,22 @@ void FuncNode::update_tree(action_list_t * act_list)
 
        for (sllnode<ModelAction *> * 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
+
+               // Only ATOMIC_RMW or ATOMIC_WRITE may be swapped with their original types,
+               // which are later added to rw_act_list. Therefore, it is safe to only revert
+               // back action types for actions in rw_act_list whose types have been swapped.
+               if (act->get_original_type() != ATOMIC_NOP && act->get_swap_flag() == false)
+                       act->use_original_type();
+
+               // Remove func_act_ref so that actions can be deleted by Execution::collectActions
+               act->setFuncActRef(NULL);
+               if (act->is_read()) {
+                       // For every read or rmw actions in this list, the reads_from is not deleted.
+                       // So it is safe to call get_reads_from
+                       ModelAction * rf = act->get_reads_from();
+                       rf->setFuncActRef(NULL);
+               }
+
                FuncInst * func_inst = get_inst(act);
                void * loc = act->get_location();
 
@@ -223,12 +238,39 @@ void FuncNode::update_tree(action_list_t * act_list)
                }
        }
 
-//     model_print("function %s\n", func_name);
-//     print_val_loc_map();
-
        update_inst_tree(&inst_list);
        update_predicate_tree(&rw_act_list);
 
+       // Revert back action types and free
+       for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
+               ModelAction * act = it->getVal();
+
+               // Revert back action types for actions whose types have been changed. 
+               if (act->get_swap_flag() == true)
+                       act->use_original_type();
+
+               /**  Free actions
+                * case 1. READY_FREE -> delete
+                * case 2. Read action whose read from is READY_FREE -> delete both actions
+                * In both cases, the actions have already been removed from core model
+                * action lists.
+                */
+
+               /* Problematic: could double free actions
+               if (act->is_free()) {
+                       model_print("delete free act %d\n", act->get_seq_number());
+                       delete act;
+               } else if (act->is_read()) {
+                       ModelAction * rf = act->get_reads_from();
+                       if (rf->is_free()) {
+                               model_print("delete act %d\n", act->get_seq_number());
+                               model_print("delete act %d\n", rf->get_seq_number());
+                               delete rf;
+                               delete act;
+                       }
+               }*/
+       }
+
 //     print_predicate_tree();
 }
 

diff --git a/predicate.cc b/predicate.cc
index f6454dbce37d3efe8b62dd920429a230d1e32070..22fb0c7e8f8172d8cbf4963970c4edd7b5d85d3c 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -87,7 +87,8 @@ void Predicate::copy_predicate_expr(Predicate * other)
  */
 Predicate * Predicate::follow_write_child(FuncInst * inst)
 {
-       ASSERT(inst->get_type() == ATOMIC_WRITE);
+       action_type type = inst->get_type();
+       ASSERT(type == ATOMIC_WRITE || type == ATOMIC_INIT);
 
        for (uint i = 0;i < children.size();i++) {
                Predicate * child = children[i];