promise: rename has_sync_thread() -> thread_is_eliminated()
[model-checker.git] / promise.cc
1 #include "promise.h"
2 #include "model.h"
3 #include "schedule.h"
4
5 /**
6  * Eliminate a thread which no longer can satisfy this promise. Once all
7  * enabled threads have been eliminated, this promise is unresolvable.
8  *
9  * @param tid The thread ID of the thread to eliminate
10  * @return True, if this elimination has invalidated the promise; false
11  * otherwise
12  */
13 bool Promise::eliminate_thread(thread_id_t tid)
14 {
15         unsigned int id = id_to_int(tid);
16         if (id >= eliminated_thread.size())
17                 eliminated_thread.resize(id + 1, false);
18         if (eliminated_thread[id])
19                 return false;
20
21         eliminated_thread[id] = true;
22         return has_failed();
23 }
24
25 /**
26  * Check if this promise has failed. A promise can fail when all threads which
27  * could possibly satisfy the promise have been eliminated.
28  *
29  * @return True, if this promise has failed; false otherwise
30  */
31 bool Promise::has_failed() const
32 {
33         unsigned int size = eliminated_thread.size();
34         int promise_tid = id_to_int(read->get_tid());
35         for (unsigned int i = 1; i < model->get_num_threads(); i++) {
36                 if ((i >= size || !eliminated_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) {
37                         return false;
38                 }
39         }
40         return true;
41 }