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();
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();
/* 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)
{
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
*
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);
+ }
}
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);