more implementation of scanalysis...
[model-checker.git] / promise.cc
1 #define __STDC_FORMAT_MACROS
2 #include <inttypes.h>
3
4 #include "promise.h"
5 #include "model.h"
6 #include "schedule.h"
7 #include "action.h"
8 #include "threads-model.h"
9
10 /**
11  * @brief Promise constructor
12  * @param read The read which reads from a promised future value
13  * @param fv The future value that is promised
14  */
15 Promise::Promise(ModelAction *read, struct future_value fv) :
16         num_available_threads(0),
17         fv(fv),
18         readers(1, read),
19         write(NULL)
20 {
21         add_thread(fv.tid);
22         eliminate_thread(read->get_tid());
23 }
24
25 /**
26  * Add a reader that reads from this Promise. Must be added in an order
27  * consistent with execution order.
28  *
29  * @param reader The ModelAction that reads from this promise. Must be a read.
30  * @return True if this new reader has invalidated the promise; false otherwise
31  */
32 bool Promise::add_reader(ModelAction *reader)
33 {
34         readers.push_back(reader);
35         return eliminate_thread(reader->get_tid());
36 }
37
38 /**
39  * Access a reader that read from this Promise. Readers must be inserted in
40  * order by execution order, so they can be returned in this order.
41  *
42  * @param i The index of the reader to return
43  * @return The i'th reader of this Promise
44  */
45 ModelAction * Promise::get_reader(unsigned int i) const
46 {
47         return i < readers.size() ? readers[i] : NULL;
48 }
49
50 /**
51  * Eliminate a thread which no longer can satisfy this promise. Once all
52  * enabled threads have been eliminated, this promise is unresolvable.
53  *
54  * @param tid The thread ID of the thread to eliminate
55  * @return True, if this elimination has invalidated the promise; false
56  * otherwise
57  */
58 bool Promise::eliminate_thread(thread_id_t tid)
59 {
60         unsigned int id = id_to_int(tid);
61         if (!thread_is_available(tid))
62                 return false;
63
64         available_thread[id] = false;
65         num_available_threads--;
66         return has_failed();
67 }
68
69 /**
70  * Add a thread which may resolve this promise
71  *
72  * @param tid The thread ID
73  */
74 void Promise::add_thread(thread_id_t tid)
75 {
76         unsigned int id = id_to_int(tid);
77         if (id >= available_thread.size())
78                 available_thread.resize(id + 1, false);
79         if (!available_thread[id]) {
80                 available_thread[id] = true;
81                 num_available_threads++;
82         }
83 }
84
85 /**
86  * Check if a thread is available for resolving this promise. That is, the
87  * thread must have been previously marked for resolving this promise, and it
88  * cannot have been eliminated due to synchronization, etc.
89  *
90  * @param tid Thread ID of the thread to check
91  * @return True if the thread is available; false otherwise
92  */
93 bool Promise::thread_is_available(thread_id_t tid) const
94 {
95         unsigned int id = id_to_int(tid);
96         if (id >= available_thread.size())
97                 return false;
98         return available_thread[id];
99 }
100
101 /** @brief Print debug info about the Promise */
102 void Promise::print() const
103 {
104         model_print("Promised value %#" PRIx64 ", first read from thread %d, available threads to resolve: ",
105                         fv.value, id_to_int(get_reader(0)->get_tid()));
106         bool failed = true;
107         for (unsigned int i = 0; i < available_thread.size(); i++)
108                 if (available_thread[i]) {
109                         model_print("[%d]", i);
110                         failed = false;
111                 }
112         if (failed)
113                 model_print("(none)");
114         model_print("\n");
115 }
116
117 /**
118  * Check if this promise has failed. A promise can fail when all threads which
119  * could possibly satisfy the promise have been eliminated.
120  *
121  * @return True, if this promise has failed; false otherwise
122  */
123 bool Promise::has_failed() const
124 {
125         return num_available_threads == 0;
126 }
127
128 /**
129  * @brief Check if an action's thread and location are compatible for resolving
130  * this promise
131  * @param act The action to check against
132  * @return True if we are compatible; false otherwise
133  */
134 bool Promise::is_compatible(const ModelAction *act) const
135 {
136         return thread_is_available(act->get_tid()) && get_reader(0)->same_var(act);
137 }
138
139 /**
140  * @brief Check if an action's thread and location are compatible for resolving
141  * this promise, and that the promise is thread-exclusive
142  * @param act The action to check against
143  * @return True if we are compatible and exclusive; false otherwise
144  */
145 bool Promise::is_compatible_exclusive(const ModelAction *act) const
146 {
147         return get_num_available_threads() == 1 && is_compatible(act);
148 }
149
150 /**
151  * @brief Check if a store's value matches this Promise
152  * @param write The store to check
153  * @return True if the store's written value matches this Promise
154  */
155 bool Promise::same_value(const ModelAction *write) const
156 {
157         return get_value() == write->get_write_value();
158 }
159
160 /**
161  * @brief Check if a ModelAction's location matches this Promise
162  * @param act The ModelAction to check
163  * @return True if the action's location matches this Promise
164  */
165 bool Promise::same_location(const ModelAction *act) const
166 {
167         return get_reader(0)->same_var(act);
168 }