X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=mutex.cc;h=91b0b9a33f8a4109d82e9334f127534b1d6ec137;hb=d2cbbe4ce6d8f6e1aa23b8fe639ed58edf1789b7;hp=b31b20a8ed2f02446fd1c4fbea5965c65b2b6979;hpb=16ef61e0af2f98a34acaa919077def37ece3b5bd;p=model-checker.git diff --git a/mutex.cc b/mutex.cc index b31b20a..91b0b9a 100644 --- a/mutex.cc +++ b/mutex.cc @@ -1,12 +1,15 @@ -#include "mutex.h" -#include "model.h" +#include +#include "model.h" +#include "threads-model.h" +#include "clockvector.h" namespace std { -mutex::mutex() : - owner(0), islocked(false) -{ - +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() {