X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=promise.cc;h=62e2c9d24d67dbd2509faba6736bec62ea410f84;hb=6d07b6dd2442d2af16d3411cbbdcfd5519853ca4;hp=90591eb60249693d773c534dfbaedf96c4117521;hpb=92db01802459e4913d32683c27e8b5cea2d9c2b2;p=model-checker.git diff --git a/promise.cc b/promise.cc index 90591eb..62e2c9d 100644 --- a/promise.cc +++ b/promise.cc @@ -2,28 +2,29 @@ #include "model.h" #include "schedule.h" -bool Promise::increment_threads(thread_id_t tid) { - unsigned int id=id_to_int(tid); - if ( id >= synced_thread.size() ) { - synced_thread.resize(id+1, false); - } +bool Promise::increment_threads(thread_id_t tid) +{ + unsigned int id = id_to_int(tid); + if (id >= synced_thread.size()) + synced_thread.resize(id + 1, false); if (synced_thread[id]) return false; - - synced_thread[id]=true; - unsigned int sync_size=synced_thread.size(); - int promise_tid=id_to_int(read->get_tid()); - for(unsigned int i=1;iget_num_threads();i++) { - if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && model->is_enabled(int_to_id(i))) { + + synced_thread[id] = true; + unsigned int sync_size = synced_thread.size(); + int promise_tid = id_to_int(read->get_tid()); + for (unsigned int i = 1; i < model->get_num_threads(); i++) { + if ((i >= sync_size || !synced_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) { return false; } } return true; } -bool Promise::check_promise() { - unsigned int sync_size=synced_thread.size(); - for(unsigned int i=1;iget_num_threads();i++) { +bool Promise::check_promise() const +{ + unsigned int sync_size = synced_thread.size(); + for (unsigned int i = 1; i < model->get_num_threads(); i++) { if ((i >= sync_size || !synced_thread[i]) && model->is_enabled(int_to_id(i))) { return false; }