From 85fac9c01a7269fe0a879f97155f9c5976672606 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 19 Sep 2012 16:38:33 -0700 Subject: [PATCH] more mutex changes --- model.cc | 4 ++++ mutex.cc | 4 +++- mutex.h | 3 +++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 651d32d..6732c26 100644 --- a/model.cc +++ b/model.cc @@ -337,6 +337,10 @@ void ModelChecker::process_mutex(ModelAction *curr) { } //otherwise fall into the lock case case ATOMIC_LOCK: { + if (curr->get_cv()->getClock(state->alloc_tid)<=state->alloc_clock) { + printf("Lock access before initialization\n"); + set_assert(); + } state->islocked=true; ModelAction *unlock=get_last_unlock(curr); //synchronize with the previous unlock statement diff --git a/mutex.cc b/mutex.cc index 2cf6828..51315d9 100644 --- a/mutex.cc +++ b/mutex.cc @@ -1,10 +1,12 @@ #include "mutex.h" #include "model.h" - namespace std { mutex::mutex() { state.islocked=false; + thread_id_t tid=thread_current()->get_id(); + state.alloc_tid=tid; + state.alloc_clock=model->get_cv(tid)->getClock(tid); } void mutex::lock() { diff --git a/mutex.h b/mutex.h index a65250b..828aae5 100644 --- a/mutex.h +++ b/mutex.h @@ -1,10 +1,13 @@ #ifndef MUTEX_H #define MUTEX_H #include "threads.h" +#include "clockvector.h" namespace std { struct mutex_state { bool islocked; + thread_id_t alloc_tid; + modelclock_t alloc_clock; }; class mutex { -- 2.34.1