From c01b2b7892814b73cb379b22cd7891d778ece391 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 19 Apr 2012 11:06:30 -0700 Subject: [PATCH] model: implement get_last_conflict() This performs a non-optimized check; that is, it uses a simple O(n) linear search, when it could utilize O(1) lookups instead... but this isn't even the full memory model yet, so I'm not working for perfection! --- model.cc | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/model.cc b/model.cc index 37baf9b..404e14c 100644 --- a/model.cc +++ b/model.cc @@ -35,6 +35,37 @@ void ModelChecker::add_system_thread(Thread *t) this->system_thread = t; } +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: + case THREAD_YIELD: + case THREAD_JOIN: + return NULL; + case ATOMIC_READ: + case ATOMIC_WRITE: + default: + break; + } + std::list::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()) + return NULL; + return prev; + } + return NULL; +} + void ModelChecker::set_backtracking(ModelAction *act) { ModelAction *prev; -- 2.34.1