Do not allow a thread to stash the next pending action if its last action was a SLEEP...

[c11tester.git] / funcnode.cc

diff --git a/funcnode.cc b/funcnode.cc
index d6672cb8901c4dbdb72d1db84c3f6cd1e401a53d..909d4a8d1e891a72d4c9ae4ea0dc6f6fbd295a40 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -22,11 +22,11 @@ FuncNode::FuncNode(ModelHistory * history) :
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
        predicate_tree_exit = new Predicate(NULL, false, true);
 
-       // Memories that are reclaimed after each execution
+       /* Snapshot data structures below */
        action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
-       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
+       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
 
        //values_may_read_from = new value_set_t();
@@ -38,7 +38,7 @@ void FuncNode::set_new_exec_flag()
        action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
-       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
+       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
 
        //values_may_read_from = new value_set_t();
@@ -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.
- *
- * 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)
 {
@@ -61,30 +58,54 @@ void FuncNode::add_inst(ModelAction *act)
        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);
 
-               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);
+       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);
+
+       return func_inst;
 }
 
+
 /* Get the FuncInst with the same type, position, and location
  * as act
  *
@@ -107,14 +128,18 @@ FuncInst * FuncNode::get_inst(ModelAction *act)
        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;
+       }
+       /* RMWRCAS actions are converted to RMW or READ actions */
        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 NULL;
+       }
+       /* Return the FuncInst in the collision list */
+       else {
+               return inst->search_in_collision(act);
+       }
 }
 
 
@@ -306,7 +331,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                        inst_id_map.put(next_inst, inst_counter++);
 
                it = it->getNext();
-               curr_pred->incr_count();
+               curr_pred->incr_expl_count();
        }
 
        curr_pred->set_exit(predicate_tree_exit);