From fd0026445b71eb29e0beedd32ba061fbc43d0c27 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 15 Nov 2012 12:21:45 -0800 Subject: [PATCH] model: add 'const' --- model.cc | 15 ++++++++++----- model.h | 10 +++++----- 2 files changed, 15 insertions(+), 10 deletions(-) diff --git a/model.cc b/model.cc index 33fc4c3c..1264f683 100644 --- a/model.cc +++ b/model.cc @@ -1038,7 +1038,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { } } -bool ModelChecker::promises_expired() { +bool ModelChecker::promises_expired() const +{ for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) { Promise *promise = (*promises)[promise_index]; if (promise->get_expiration()used_sequence_numbers) { @@ -1050,12 +1051,14 @@ bool ModelChecker::promises_expired() { /** @return whether the current partial trace must be a prefix of a * feasible trace. */ -bool ModelChecker::isfeasibleprefix() { +bool ModelChecker::isfeasibleprefix() const +{ return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); } /** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() { +bool ModelChecker::isfeasible() const +{ if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) DEBUG("Infeasible: RMW violation\n"); @@ -1064,7 +1067,8 @@ bool ModelChecker::isfeasible() { /** @return whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ -bool ModelChecker::isfeasibleotherthanRMW() { +bool ModelChecker::isfeasibleotherthanRMW() const +{ if (DBG_ENABLED()) { if (mo_graph->checkForCycles()) DEBUG("Infeasible: modification order cycles\n"); @@ -1081,7 +1085,8 @@ bool ModelChecker::isfeasibleotherthanRMW() { } /** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() { +bool ModelChecker::isfinalfeasible() const +{ if (DBG_ENABLED() && promises->size() != 0) DEBUG("Infeasible: unrevolved promises\n"); diff --git a/model.h b/model.h index ee8026d0..baec467b 100644 --- a/model.h +++ b/model.h @@ -98,15 +98,15 @@ public: ClockVector * get_cv(thread_id_t tid); ModelAction * get_parent_action(thread_id_t tid); bool next_execution(); - bool isfeasible(); - bool isfeasibleotherthanRMW(); - bool isfinalfeasible(); + bool isfeasible() const; + bool isfeasibleotherthanRMW() const; + bool isfinalfeasible() const; void check_promises_thread_disabled(); void mo_check_promises(thread_id_t tid, const ModelAction *write); void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv); void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads); void finish_execution(); - bool isfeasibleprefix(); + bool isfeasibleprefix() const; void set_assert() {asserted=true;} bool is_deadlocked() const; bool is_complete_execution() const; @@ -130,7 +130,7 @@ private: void reset_asserted() {asserted=false;} int num_executions; int num_feasible_executions; - bool promises_expired(); + bool promises_expired() const; void execute_sleep_set(); void wake_up_sleeping_actions(ModelAction * curr); modelclock_t get_next_seq_num(); -- 2.34.1