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