7 #define INITIAL_THREAD_ID 0
11 ModelChecker::ModelChecker()
13 /* First thread created will have id (INITIAL_THREAD_ID + 1) */
14 this->used_thread_id = INITIAL_THREAD_ID;
15 /* Initialize default scheduler */
16 this->scheduler = new Scheduler();
19 this->current_action = NULL;
20 this->exploring = NULL;
21 this->nextThread = THREAD_ID_T_NONE;
23 rootNode = new TreeNode(NULL);
24 currentNode = rootNode;
25 action_trace = new action_list_t();
28 ModelChecker::~ModelChecker()
31 delete this->scheduler;
35 void ModelChecker::reset_to_initial_state()
37 DEBUG("+++ Resetting to initial state +++\n");
38 std::map<thread_id_t, class Thread *>::iterator it;
39 for (it = thread_map.begin(); it != thread_map.end(); it++) {
43 action_trace = new action_list_t();
44 currentNode = rootNode;
45 current_action = NULL;
46 used_thread_id = INITIAL_THREAD_ID;
47 /* scheduler reset ? */
50 int ModelChecker::get_next_id()
52 return ++used_thread_id;
55 Thread * ModelChecker::schedule_next_thread()
58 if (nextThread == THREAD_ID_T_NONE)
60 t = thread_map[nextThread];
62 DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
67 * get_next_replay_thread() - Choose the next thread in the replay sequence
69 * If we've reached the 'diverge' point, then we pick a thread from the
71 * Otherwise, we simply return the next thread in the sequence.
73 thread_id_t ModelChecker::get_next_replay_thread()
78 next = exploring->get_state();
80 if (next == exploring->get_diverge()) {
81 TreeNode *node = next->get_node();
83 /* Reached divergence point; discard our current 'exploring' */
84 DEBUG("*** Discard 'Backtrack' object ***\n");
85 tid = node->getNextBacktrack();
89 tid = next->get_tid();
91 DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
95 thread_id_t ModelChecker::advance_backtracking_state()
97 /* Have we completed exploring the preselected path? */
98 if (exploring == NULL)
99 return THREAD_ID_T_NONE;
101 /* Else, we are trying to replay an execution */
102 exploring->advance_state();
103 if (exploring->get_state() == NULL)
104 DEBUG("*** error: reached end of backtrack trace\n");
106 return get_next_replay_thread();
109 bool ModelChecker::next_execution()
113 if ((exploring = model->get_next_backtrack()) == NULL)
115 model->reset_to_initial_state();
116 nextThread = get_next_replay_thread();
120 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
122 action_type type = act->get_type();
134 /* linear search: from most recent to oldest */
135 action_list_t::reverse_iterator rit;
136 for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
137 ModelAction *prev = *rit;
138 if (act->is_dependent(prev))
144 void ModelChecker::set_backtracking(ModelAction *act)
149 prev = get_last_conflict(act);
153 node = prev->get_node();
155 /* Check if this has been explored already */
156 if (node->hasBeenExplored(act->get_tid()))
158 /* If this is a new backtracking point, mark the tree */
159 if (node->setBacktrack(act->get_tid()) != 0)
162 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
163 prev->get_tid(), act->get_tid());
169 Backtrack *back = new Backtrack(prev, action_trace);
170 backtrack_list.push_back(back);
173 Backtrack * ModelChecker::get_next_backtrack()
176 if (backtrack_list.empty())
178 next = backtrack_list.back();
179 backtrack_list.pop_back();
183 void ModelChecker::check_current_action(void)
185 ModelAction *next = this->current_action;
188 DEBUG("trying to push NULL action...\n");
191 current_action = NULL;
192 nextThread = advance_backtracking_state();
193 next->set_node(currentNode);
194 set_backtracking(next);
195 currentNode = currentNode->exploreChild(next->get_tid());
196 this->action_trace->push_back(next);
199 void ModelChecker::print_summary(void)
201 action_list_t::iterator it;
204 printf("---------------------------------------------------------------------\n");
205 printf("Number of executions: %d\n", num_executions);
206 printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes());
210 printf("Trace:\n\n");
212 for (it = action_trace->begin(); it != action_trace->end(); it++) {
216 printf("---------------------------------------------------------------------\n");
219 int ModelChecker::add_thread(Thread *t)
221 thread_map[t->get_id()] = t;
222 scheduler->add_thread(t);
226 void ModelChecker::remove_thread(Thread *t)
228 scheduler->remove_thread(t);
231 int ModelChecker::switch_to_master(ModelAction *act)
236 old = thread_current();
237 set_current_action(act);
238 old->set_state(THREAD_READY);
239 return Thread::swap(old, get_system_context());
242 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
244 Thread *t = thread_current();
245 ModelAction *act = this;
250 act->tid = t->get_id();
254 bool ModelAction::is_read()
256 return type == ATOMIC_READ;
259 bool ModelAction::is_write()
261 return type == ATOMIC_WRITE;
264 bool ModelAction::same_var(ModelAction *act)
266 return location == act->location;
269 bool ModelAction::same_thread(ModelAction *act)
271 return tid == act->tid;
274 bool ModelAction::is_dependent(ModelAction *act)
276 if (!is_read() && !is_write())
278 if (!act->is_read() && !act->is_write())
280 if (same_var(act) && !same_thread(act) &&
281 (is_write() || act->is_write()))
286 void ModelAction::print(void)
288 const char *type_str;
289 switch (this->type) {
291 type_str = "thread create";
294 type_str = "thread yield";
297 type_str = "thread join";
300 type_str = "atomic read";
303 type_str = "atomic write";
306 type_str = "unknown type";
309 printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);