Add a collision list for FuncInsts with the same source line number

diff --git a/execution.cc b/execution.cc
index e285156fd15d1526d2492006354fd7527535df06..e6203cb548861653ed600b83238f112f4e42d667 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -821,8 +821,9 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  *
  * @param curr The current action. Must be a read.
  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
  *
  * @param curr The current action. Must be a read.
  * @param rf The ModelAction or Promise that curr reads from. Must be a write.

- * @param check_only Only check if the current action satisfies read 
- *        modification order or not, without modifiying priorsetand canprune
+ * @param check_only If true, then only check whether the current action satisfies
+ *        read modification order or not, without modifiying priorset and canprune.
+ *        False by default.

  * @return True if modification order edges were added; false otherwise
  */
 
  * @return True if modification order edges were added; false otherwise
  */
 

diff --git a/funcinst.cc b/funcinst.cc
index 44bb167e2193f411fe129a3a51c54e4127124421..df91edc848cb9a0417385bf0e6e78f31bcc321cd 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -3,7 +3,7 @@
 
 FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
        single_location(true),
 
 FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
        single_location(true),

-       execution_number(model->get_execution_number()),
+       execution_number(0),

        action_marker(0)        /* The marker for FuncNode starts from 1 */
 {
        ASSERT(act);
        action_marker(0)        /* The marker for FuncNode starts from 1 */
 {
        ASSERT(act);


@@ -61,7 +61,7 @@ ModelAction * FuncInst::get_associated_act(uint32_t marker)
                return NULL;
 }
 
                return NULL;
 }
 

-/*
+/* Search the FuncInst that has the same type as act in the collision list */

 FuncInst * FuncInst::search_in_collision(ModelAction *act)
 {
        action_type type = act->get_type();
 FuncInst * FuncInst::search_in_collision(ModelAction *act)
 {
        action_type type = act->get_type();


@@ -74,7 +74,11 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
        }
        return NULL;
 }
        }
        return NULL;
 }

-*/
+
+void FuncInst::add_to_collision(FuncInst * inst)
+{
+       collisions.push_back(inst);
+}

 
 /* Note: is_read() is equivalent to ModelAction::is_read() */
 bool FuncInst::is_read() const
 
 /* Note: is_read() is equivalent to ModelAction::is_read() */
 bool FuncInst::is_read() const

diff --git a/funcinst.h b/funcinst.h
index 98af6bcb297a02c15fb1aa88fd3d9343bacb72b6..e96eb19067ba2afb6831810dbece99bdb8f81a7a 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -25,8 +25,8 @@ public:
        bool add_pred(FuncInst * other);
        bool add_succ(FuncInst * other);
 
        bool add_pred(FuncInst * other);
        bool add_succ(FuncInst * other);
 

-       //FuncInst * search_in_collision(ModelAction *act);
-       //func_inst_list_mt * get_collisions() { return &collisions; }
+       FuncInst * search_in_collision(ModelAction *act);
+       void add_to_collision(FuncInst * inst);

 
        func_inst_list_mt * get_preds() { return &predecessors; }
        func_inst_list_mt * get_succs() { return &successors; }
 
        func_inst_list_mt * get_preds() { return &predecessors; }
        func_inst_list_mt * get_succs() { return &successors; }


@@ -67,12 +67,13 @@ private:
        ModelAction * associated_act;
        uint32_t action_marker;
 
        ModelAction * associated_act;
        uint32_t action_marker;
 

-       /* Currently not in use. May remove this field later
-        *
-        * collisions store a list of FuncInsts with the same position
-        * but different action types. For example, CAS is broken down
-        * as three different atomic operations in cmodelint.cc */
-       // func_inst_list_mt collisions;
+       /**
+        * Collisions store a list of FuncInsts with the same position
+        * but different action types. For example,
+        * <code>volatile int x; x++;</code> produces read and write
+        * actions with the same position.
+        */
+       func_inst_list_mt collisions;

 
        func_inst_list_mt predecessors;
        func_inst_list_mt successors;
 
        func_inst_list_mt predecessors;
        func_inst_list_mt successors;

diff --git a/funcnode.cc b/funcnode.cc
index 2972b86ed0e0ab037ade76d9589eebba2f90b7cb..909d4a8d1e891a72d4c9ae4ea0dc6f6fbd295a40 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -46,9 +46,6 @@ void FuncNode::set_new_exec_flag()
 
 /* Check whether FuncInst with the same type, position, and location
  * as act has been added to func_inst_map or not. If not, add it.
 
 /* Check whether FuncInst with the same type, position, and location
  * as act has been added to func_inst_map or not. If not, add it.

- *
- * Note: currently, actions with the same position are filtered out by process_action,
- * so the collision list of FuncInst is not used. May remove it later. 

  */
 void FuncNode::add_inst(ModelAction *act)
 {
  */
 void FuncNode::add_inst(ModelAction *act)
 {


@@ -61,31 +58,54 @@ void FuncNode::add_inst(ModelAction *act)
        if (position == NULL)
                return;
 
        if (position == NULL)
                return;
 

-       if ( func_inst_map.contains(position) ) {
-               FuncInst * inst = func_inst_map.get(position);
+       FuncInst * func_inst = func_inst_map.get(position);

 
 

-               /* TODO: The assertion fails when encountering volatile variables that use ++ or -- syntax, i.e. read and write have the same position */
-               ASSERT(inst->get_type() == act->get_type());
-               int curr_execution_number = model->get_execution_number();
+       /* This position has not been inserted into hashtable before */
+       if (func_inst == NULL) {
+               func_inst = create_new_inst(act);
+               func_inst_map.put(position, func_inst);
+               return;
+       }

 
 

-               /* Reset locations when new executions start */
-               if (inst->get_execution_number() != curr_execution_number) {
-                       inst->set_location(act->get_location());
-                       inst->set_execution_number(curr_execution_number);
+       /* Volatile variables that use ++ or -- syntax may result in read and write actions with the same position */
+       if (func_inst->get_type() != act->get_type()) {
+               FuncInst * collision_inst = func_inst->search_in_collision(act);
+
+               if (collision_inst == NULL) {
+                       collision_inst = create_new_inst(act);
+                       func_inst->add_to_collision(collision_inst);
+                       return;
+               } else {
+                       func_inst = collision_inst;

                }
                }

+       }

 
 

-               if (inst->get_location() != act->get_location())
-                       inst->not_single_location();
+       ASSERT(func_inst->get_type() == act->get_type());
+       int curr_execution_number = model->get_execution_number();

 
 

-               return;
+       /* Reset locations when new executions start */
+       if (func_inst->get_execution_number() != curr_execution_number) {
+               func_inst->set_location(act->get_location());
+               func_inst->set_execution_number(curr_execution_number);

        }
 
        }
 

+       /* Mark the memory location of such inst as not unique */
+       if (func_inst->get_location() != act->get_location())
+               func_inst->not_single_location();
+}
+
+FuncInst * FuncNode::create_new_inst(ModelAction * act)
+{

        FuncInst * func_inst = new FuncInst(act, this);
        FuncInst * func_inst = new FuncInst(act, this);

+       int exec_num = model->get_execution_number();
+       func_inst->set_execution_number(exec_num);

 
 

-       func_inst_map.put(position, func_inst);

        inst_list.push_back(func_inst);
        inst_list.push_back(func_inst);

+
+       return func_inst;

 }
 
 }
 

+

 /* Get the FuncInst with the same type, position, and location
  * as act
  *
 /* Get the FuncInst with the same type, position, and location
  * as act
  *


@@ -108,14 +128,18 @@ FuncInst * FuncNode::get_inst(ModelAction *act)
        action_type inst_type = inst->get_type();
        action_type act_type = act->get_type();
 
        action_type inst_type = inst->get_type();
        action_type act_type = act->get_type();
 

-       // else if branch: an RMWRCAS action is converted to a RMW or READ action
-       if (inst_type == act_type)
+       if (inst_type == act_type) {

                return inst;
                return inst;

+       }
+       /* RMWRCAS actions are converted to RMW or READ actions */

        else if (inst_type == ATOMIC_RMWRCAS &&
        else if (inst_type == ATOMIC_RMWRCAS &&

-                       (act_type == ATOMIC_RMW || act_type == ATOMIC_READ))
+                       (act_type == ATOMIC_RMW || act_type == ATOMIC_READ)) {

                return inst;
                return inst;

-
-       return NULL;
+       }
+       /* Return the FuncInst in the collision list */
+       else {
+               return inst->search_in_collision(act);
+       }

 }
 
 
 }
 
 

diff --git a/funcnode.h b/funcnode.h
index fab4db50903af3bd5e4146b18b42ce5ce135c01c..ea591a2e05ba5426c0e553b11cacfa609c0df078 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -25,6 +25,7 @@ public:
        void set_new_exec_flag();
 
        void add_inst(ModelAction *act);
        void set_new_exec_flag();
 
        void add_inst(ModelAction *act);

+       FuncInst * create_new_inst(ModelAction *act);

        FuncInst * get_inst(ModelAction *act);
 
        HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncInstMap() { return &func_inst_map; }
        FuncInst * get_inst(ModelAction *act);
 
        HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncInstMap() { return &func_inst_map; }