ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
{
- void *loc = act->get_location();
action_type type = act->get_type();
- thread_id_t id = act->get_tid();
switch (type) {
case THREAD_CREATE:
action_list_t::reverse_iterator rit;
for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
ModelAction *prev = *rit;
- if (prev->get_location() != loc)
- continue;
- if (type == ATOMIC_READ && prev->get_type() != ATOMIC_WRITE)
- continue;
- /* Conflict from the same thread is not really a conflict */
- if (id == prev->get_tid())
- continue;
- return prev;
+ if (act->is_dependent(prev))
+ return prev;
}
return NULL;
}
act->value = value;
}
+bool ModelAction::is_read()
+{
+ return type == ATOMIC_READ;
+}
+
+bool ModelAction::is_write()
+{
+ return type == ATOMIC_WRITE;
+}
+
+bool ModelAction::same_var(ModelAction *act)
+{
+ return location == act->location;
+}
+
+bool ModelAction::same_thread(ModelAction *act)
+{
+ return tid == act->tid;
+}
+
+bool ModelAction::is_dependent(ModelAction *act)
+{
+ if (!is_read() && !is_write())
+ return false;
+ if (!act->is_read() && !act->is_write())
+ return false;
+ if (same_var(act) && !same_thread(act) &&
+ (is_write() || act->is_write()))
+ return true;
+ return false;
+}
+
void ModelAction::print(void)
{
const char *type_str;
TreeNode * get_node() { return node; }
void set_node(TreeNode *n) { node = n; }
+
+ bool is_read();
+ bool is_write();
+ bool same_var(ModelAction *act);
+ bool same_thread(ModelAction *act);
+ bool is_dependent(ModelAction *act);
private:
action_type type;
memory_order order;