Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
[c11tester.git] / model.cc
1 #include <stdio.h>
2
3 #include "model.h"
4 #include "action.h"
5 #include "nodestack.h"
6 #include "schedule.h"
7 #include "snapshot-interface.h"
8 #include "common.h"
9 #include "clockvector.h"
10 #include "cyclegraph.h"
11 #include "promise.h"
12 #include "datarace.h"
13
14 #define INITIAL_THREAD_ID       0
15
16 ModelChecker *model;
17
18 /** @brief Constructor */
19 ModelChecker::ModelChecker(struct model_params params) :
20         /* Initialize default scheduler */
21         scheduler(new Scheduler()),
22         /* First thread created will have id INITIAL_THREAD_ID */
23         next_thread_id(INITIAL_THREAD_ID),
24         used_sequence_numbers(0),
25         num_executions(0),
26         params(params),
27         current_action(NULL),
28         diverge(NULL),
29         nextThread(NULL),
30         action_trace(new action_list_t()),
31         thread_map(new HashTable<int, Thread *, int>()),
32         obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
33         obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
34         promises(new std::vector<Promise *>()),
35         lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
36         thrd_last_action(new std::vector<ModelAction *>(1)),
37         node_stack(new NodeStack()),
38         next_backtrack(NULL),
39         mo_graph(new CycleGraph()),
40         failed_promise(false),
41         asserted(false)
42 {
43 }
44
45 /** @brief Destructor */
46 ModelChecker::~ModelChecker()
47 {
48         for (int i = 0; i < get_num_threads(); i++)
49                 delete thread_map->get(i);
50         delete thread_map;
51
52         delete obj_thrd_map;
53         delete obj_map;
54         delete action_trace;
55
56         for (unsigned int i = 0; i < promises->size(); i++)
57                 delete (*promises)[i];
58         delete promises;
59
60         delete lazy_sync_with_release;
61
62         delete thrd_last_action;
63         delete node_stack;
64         delete scheduler;
65         delete mo_graph;
66 }
67
68 /**
69  * Restores user program to initial state and resets all model-checker data
70  * structures.
71  */
72 void ModelChecker::reset_to_initial_state()
73 {
74         DEBUG("+++ Resetting to initial state +++\n");
75         node_stack->reset_execution();
76         current_action = NULL;
77         next_thread_id = INITIAL_THREAD_ID;
78         used_sequence_numbers = 0;
79         nextThread = NULL;
80         next_backtrack = NULL;
81         failed_promise = false;
82         reset_asserted();
83         snapshotObject->backTrackBeforeStep(0);
84 }
85
86 /** @returns a thread ID for a new Thread */
87 thread_id_t ModelChecker::get_next_id()
88 {
89         return next_thread_id++;
90 }
91
92 /** @returns the number of user threads created during this execution */
93 int ModelChecker::get_num_threads()
94 {
95         return next_thread_id;
96 }
97
98 /** @returns a sequence number for a new ModelAction */
99 modelclock_t ModelChecker::get_next_seq_num()
100 {
101         return ++used_sequence_numbers;
102 }
103
104 /**
105  * Choose the next thread in the replay sequence.
106  *
107  * If the replay sequence has reached the 'diverge' point, returns a thread
108  * from the backtracking set. Otherwise, simply returns the next thread in the
109  * sequence that is being replayed.
110  */
111 Thread * ModelChecker::get_next_replay_thread()
112 {
113         thread_id_t tid;
114
115         /* Have we completed exploring the preselected path? */
116         if (diverge == NULL)
117                 return NULL;
118
119         /* Else, we are trying to replay an execution */
120         ModelAction *next = node_stack->get_next()->get_action();
121
122         if (next == diverge) {
123                 Node *nextnode = next->get_node();
124                 /* Reached divergence point */
125                 if (nextnode->increment_promise()) {
126                         /* The next node will try to satisfy a different set of promises. */
127                         tid = next->get_tid();
128                         node_stack->pop_restofstack(2);
129                 } else if (nextnode->increment_read_from()) {
130                         /* The next node will read from a different value. */
131                         tid = next->get_tid();
132                         node_stack->pop_restofstack(2);
133                 } else if (nextnode->increment_future_value()) {
134                         /* The next node will try to read from a different future value. */
135                         tid = next->get_tid();
136                         node_stack->pop_restofstack(2);
137                 } else {
138                         /* Make a different thread execute for next step */
139                         Node *node = nextnode->get_parent();
140                         tid = node->get_next_backtrack();
141                         node_stack->pop_restofstack(1);
142                 }
143                 DEBUG("*** Divergence point ***\n");
144                 diverge = NULL;
145         } else {
146                 tid = next->get_tid();
147         }
148         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
149         ASSERT(tid != THREAD_ID_T_NONE);
150         return thread_map->get(id_to_int(tid));
151 }
152
153 /**
154  * Queries the model-checker for more executions to explore and, if one
155  * exists, resets the model-checker state to execute a new execution.
156  *
157  * @return If there are more executions to explore, return true. Otherwise,
158  * return false.
159  */
160 bool ModelChecker::next_execution()
161 {
162         DBG();
163
164         num_executions++;
165
166         if (isfinalfeasible() || DBG_ENABLED())
167                 print_summary();
168
169         if ((diverge = model->get_next_backtrack()) == NULL)
170                 return false;
171
172         if (DBG_ENABLED()) {
173                 printf("Next execution will diverge at:\n");
174                 diverge->print();
175         }
176
177         model->reset_to_initial_state();
178         return true;
179 }
180
181 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
182 {
183         action_type type = act->get_type();
184
185         switch (type) {
186                 case ATOMIC_READ:
187                 case ATOMIC_WRITE:
188                 case ATOMIC_RMW:
189                         break;
190                 default:
191                         return NULL;
192         }
193         /* linear search: from most recent to oldest */
194         action_list_t *list = obj_map->get_safe_ptr(act->get_location());
195         action_list_t::reverse_iterator rit;
196         for (rit = list->rbegin(); rit != list->rend(); rit++) {
197                 ModelAction *prev = *rit;
198                 if (act->is_synchronizing(prev))
199                         return prev;
200         }
201         return NULL;
202 }
203
204 void ModelChecker::set_backtracking(ModelAction *act)
205 {
206         ModelAction *prev;
207         Node *node;
208         Thread *t = get_thread(act->get_tid());
209
210         prev = get_last_conflict(act);
211         if (prev == NULL)
212                 return;
213
214         node = prev->get_node()->get_parent();
215
216         while (!node->is_enabled(t))
217                 t = t->get_parent();
218
219         /* Check if this has been explored already */
220         if (node->has_been_explored(t->get_id()))
221                 return;
222
223         /* Cache the latest backtracking point */
224         if (!next_backtrack || *prev > *next_backtrack)
225                 next_backtrack = prev;
226
227         /* If this is a new backtracking point, mark the tree */
228         if (!node->set_backtrack(t->get_id()))
229                 return;
230         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
231                         prev->get_tid(), t->get_id());
232         if (DBG_ENABLED()) {
233                 prev->print();
234                 act->print();
235         }
236 }
237
238 /**
239  * Returns last backtracking point. The model checker will explore a different
240  * path for this point in the next execution.
241  * @return The ModelAction at which the next execution should diverge.
242  */
243 ModelAction * ModelChecker::get_next_backtrack()
244 {
245         ModelAction *next = next_backtrack;
246         next_backtrack = NULL;
247         return next;
248 }
249
250 /**
251  * This is the heart of the model checker routine. It performs model-checking
252  * actions corresponding to a given "current action." Among other processes, it
253  * calculates reads-from relationships, updates synchronization clock vectors,
254  * forms a memory_order constraints graph, and handles replay/backtrack
255  * execution when running permutations of previously-observed executions.
256  *
257  * @param curr The current action to process
258  * @return The next Thread that must be executed. May be NULL if ModelChecker
259  * makes no choice (e.g., according to replay execution, combining RMW actions,
260  * etc.)
261  */
262 Thread * ModelChecker::check_current_action(ModelAction *curr)
263 {
264         bool already_added = false;
265
266         ASSERT(curr);
267
268         if (curr->is_rmwc() || curr->is_rmw()) {
269                 ModelAction *tmp = process_rmw(curr);
270                 already_added = true;
271                 delete curr;
272                 curr = tmp;
273         } else {
274                 ModelAction *tmp = node_stack->explore_action(curr);
275                 if (tmp) {
276                         /* Discard duplicate ModelAction; use action from NodeStack */
277                         /* First restore type and order in case of RMW operation */
278                         if (curr->is_rmwr())
279                                 tmp->copy_typeandorder(curr);
280
281                         /* If we have diverged, we need to reset the clock vector. */
282                         if (diverge == NULL)
283                                 tmp->create_cv(get_parent_action(tmp->get_tid()));
284
285                         delete curr;
286                         curr = tmp;
287                 } else {
288                         /*
289                          * Perform one-time actions when pushing new ModelAction onto
290                          * NodeStack
291                          */
292                         curr->create_cv(get_parent_action(curr->get_tid()));
293                         /* Build may_read_from set */
294                         if (curr->is_read())
295                                 build_reads_from_past(curr);
296                         if (curr->is_write())
297                                 compute_promises(curr);
298                 }
299         }
300
301         /* Assign 'creation' parent */
302         if (curr->get_type() == THREAD_CREATE) {
303                 Thread *th = (Thread *)curr->get_location();
304                 th->set_creation(curr);
305         } else if (curr->get_type() == THREAD_JOIN) {
306                 Thread *wait, *join;
307                 wait = get_thread(curr->get_tid());
308                 join = (Thread *)curr->get_location();
309                 if (!join->is_complete())
310                         scheduler->wait(wait, join);
311         } else if (curr->get_type() == THREAD_FINISH) {
312                 Thread *th = get_thread(curr->get_tid());
313                 while (!th->wait_list_empty()) {
314                         Thread *wake = th->pop_wait_list();
315                         scheduler->wake(wake);
316                 }
317                 th->complete();
318         }
319
320         /* Deal with new thread */
321         if (curr->get_type() == THREAD_START)
322                 check_promises(NULL, curr->get_cv());
323
324         /* Assign reads_from values */
325         Thread *th = get_thread(curr->get_tid());
326         uint64_t value = VALUE_NONE;
327         bool updated = false;
328         if (curr->is_read()) {
329                 const ModelAction *reads_from = curr->get_node()->get_read_from();
330                 if (reads_from != NULL) {
331                         value = reads_from->get_value();
332                         /* Assign reads_from, perform release/acquire synchronization */
333                         curr->read_from(reads_from);
334                         if (r_modification_order(curr,reads_from))
335                                 updated = true;
336                 } else {
337                         /* Read from future value */
338                         value = curr->get_node()->get_future_value();
339                         curr->read_from(NULL);
340                         Promise *valuepromise = new Promise(curr, value);
341                         promises->push_back(valuepromise);
342                 }
343         } else if (curr->is_write()) {
344                 if (w_modification_order(curr))
345                         updated = true;
346                 if (resolve_promises(curr))
347                         updated = true;
348         }
349
350         if (updated)
351                 resolve_release_sequences(curr->get_location());
352
353         th->set_return_value(value);
354
355         /* Add action to list.  */
356         if (!already_added)
357                 add_action_to_lists(curr);
358
359         Node *currnode = curr->get_node();
360         Node *parnode = currnode->get_parent();
361
362         if (!parnode->backtrack_empty() || !currnode->read_from_empty() ||
363                   !currnode->future_value_empty() || !currnode->promise_empty())
364                 if (!next_backtrack || *curr > *next_backtrack)
365                         next_backtrack = curr;
366
367         set_backtracking(curr);
368
369         /* Do not split atomic actions. */
370         if (curr->is_rmwr())
371                 return thread_current();
372         else
373                 return get_next_replay_thread();
374 }
375
376 /** @returns whether the current partial trace must be a prefix of a
377  * feasible trace. */
378
379 bool ModelChecker::isfeasibleprefix() {
380         return promises->size()==0;
381 }
382
383 /** @returns whether the current partial trace is feasible. */
384 bool ModelChecker::isfeasible() {
385         return !mo_graph->checkForCycles() && !failed_promise;
386 }
387
388 /** Returns whether the current completed trace is feasible. */
389 bool ModelChecker::isfinalfeasible() {
390         return isfeasible() && promises->size() == 0;
391 }
392
393 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
394 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
395         int tid = id_to_int(act->get_tid());
396         ModelAction *lastread = get_last_action(tid);
397         lastread->process_rmw(act);
398         if (act->is_rmw())
399                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
400         return lastread;
401 }
402
403 /**
404  * Updates the mo_graph with the constraints imposed from the current read.
405  * @param curr The current action. Must be a read.
406  * @param rf The action that curr reads from. Must be a write.
407  * @return True if modification order edges were added; false otherwise
408  */
409 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
410 {
411         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
412         unsigned int i;
413         bool added = false;
414         ASSERT(curr->is_read());
415
416         /* Iterate over all threads */
417         for (i = 0; i < thrd_lists->size(); i++) {
418                 /* Iterate over actions in thread, starting from most recent */
419                 action_list_t *list = &(*thrd_lists)[i];
420                 action_list_t::reverse_iterator rit;
421                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
422                         ModelAction *act = *rit;
423
424                         /* Include at most one act per-thread that "happens before" curr */
425                         if (act->happens_before(curr)) {
426                                 if (act->is_read()) {
427                                         const ModelAction *prevreadfrom = act->get_reads_from();
428                                         if (prevreadfrom != NULL && rf != prevreadfrom) {
429                                                 mo_graph->addEdge(prevreadfrom, rf);
430                                                 added = true;
431                                         }
432                                 } else if (rf != act) {
433                                         mo_graph->addEdge(act, rf);
434                                         added = true;
435                                 }
436                                 break;
437                         }
438                 }
439         }
440
441         return added;
442 }
443
444 /** Updates the mo_graph with the constraints imposed from the current read. */
445 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
446 {
447         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
448         unsigned int i;
449         ASSERT(curr->is_read());
450
451         /* Iterate over all threads */
452         for (i = 0; i < thrd_lists->size(); i++) {
453                 /* Iterate over actions in thread, starting from most recent */
454                 action_list_t *list = &(*thrd_lists)[i];
455                 action_list_t::reverse_iterator rit;
456                 ModelAction *lastact = NULL;
457
458                 /* Find last action that happens after curr */
459                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
460                         ModelAction *act = *rit;
461                         if (curr->happens_before(act)) {
462                                 lastact = act;
463                         } else
464                                 break;
465                 }
466
467                         /* Include at most one act per-thread that "happens before" curr */
468                 if (lastact != NULL) {
469                         if (lastact->is_read()) {
470                                 const ModelAction *postreadfrom = lastact->get_reads_from();
471                                 if (postreadfrom != NULL&&rf != postreadfrom)
472                                         mo_graph->addEdge(rf, postreadfrom);
473                         } else if (rf != lastact) {
474                                 mo_graph->addEdge(rf, lastact);
475                         }
476                         break;
477                 }
478         }
479 }
480
481 /**
482  * Updates the mo_graph with the constraints imposed from the current write.
483  * @param curr The current action. Must be a write.
484  * @return True if modification order edges were added; false otherwise
485  */
486 bool ModelChecker::w_modification_order(ModelAction *curr)
487 {
488         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
489         unsigned int i;
490         bool added = false;
491         ASSERT(curr->is_write());
492
493         if (curr->is_seqcst()) {
494                 /* We have to at least see the last sequentially consistent write,
495                          so we are initialized. */
496                 ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
497                 if (last_seq_cst != NULL) {
498                         mo_graph->addEdge(last_seq_cst, curr);
499                         added = true;
500                 }
501         }
502
503         /* Iterate over all threads */
504         for (i = 0; i < thrd_lists->size(); i++) {
505                 /* Iterate over actions in thread, starting from most recent */
506                 action_list_t *list = &(*thrd_lists)[i];
507                 action_list_t::reverse_iterator rit;
508                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
509                         ModelAction *act = *rit;
510
511                         /* Include at most one act per-thread that "happens before" curr */
512                         if (act->happens_before(curr)) {
513                                 if (act->is_read())
514                                         mo_graph->addEdge(act->get_reads_from(), curr);
515                                 else
516                                         mo_graph->addEdge(act, curr);
517                                 added = true;
518                                 break;
519                         } else if (act->is_read() && !act->is_synchronizing(curr) &&
520                                                      !act->same_thread(curr)) {
521                                 /* We have an action that:
522                                    (1) did not happen before us
523                                    (2) is a read and we are a write
524                                    (3) cannot synchronize with us
525                                    (4) is in a different thread
526                                    =>
527                                    that read could potentially read from our write.
528                                  */
529                                 if (act->get_node()->add_future_value(curr->get_value()) &&
530                                                 (!next_backtrack || *act > *next_backtrack))
531                                         next_backtrack = act;
532                         }
533                 }
534         }
535
536         return added;
537 }
538
539 /**
540  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
541  * The ModelAction under consideration is expected to be taking part in
542  * release/acquire synchronization as an object of the "reads from" relation.
543  * Note that this can only provide release sequence support for RMW chains
544  * which do not read from the future, as those actions cannot be traced until
545  * their "promise" is fulfilled. Similarly, we may not even establish the
546  * presence of a release sequence with certainty, as some modification order
547  * constraints may be decided further in the future. Thus, this function
548  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
549  * and a boolean representing certainty.
550  *
551  * @todo Finish lazy updating, when promises are fulfilled in the future
552  * @param rf The action that might be part of a release sequence. Must be a
553  * write.
554  * @param release_heads A pass-by-reference style return parameter.  After
555  * execution of this function, release_heads will contain the heads of all the
556  * relevant release sequences, if any exists
557  * @return true, if the ModelChecker is certain that release_heads is complete;
558  * false otherwise
559  */
560 bool ModelChecker::release_seq_head(const ModelAction *rf,
561                 std::vector<const ModelAction *> *release_heads) const
562 {
563         ASSERT(rf->is_write());
564         if (!rf) {
565                 /* read from future: need to settle this later */
566                 return false; /* incomplete */
567         }
568         if (rf->is_release())
569                 release_heads->push_back(rf);
570         if (rf->is_rmw()) {
571                 if (rf->is_acquire())
572                         return true; /* complete */
573                 return release_seq_head(rf->get_reads_from(), release_heads);
574         }
575         if (rf->is_release())
576                 return true; /* complete */
577
578         /* else relaxed write; check modification order for contiguous subsequence
579          * -> rf must be same thread as release */
580         int tid = id_to_int(rf->get_tid());
581         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
582         action_list_t *list = &(*thrd_lists)[tid];
583         action_list_t::const_reverse_iterator rit;
584
585         /* Find rf in the thread list */
586         for (rit = list->rbegin(); rit != list->rend(); rit++)
587                 if (*rit == rf)
588                         break;
589
590         /* Find the last write/release */
591         for (; rit != list->rend(); rit++)
592                 if ((*rit)->is_release())
593                         break;
594         if (rit == list->rend()) {
595                 /* No write-release in this thread */
596                 return true; /* complete */
597         }
598         ModelAction *release = *rit;
599
600         ASSERT(rf->same_thread(release));
601
602         bool certain = true;
603         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
604                 if (id_to_int(rf->get_tid()) == (int)i)
605                         continue;
606                 list = &(*thrd_lists)[i];
607                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
608                         const ModelAction *act = *rit;
609                         if (!act->is_write())
610                                 continue;
611                         /* Reach synchronization -> this thread is complete */
612                         if (act->happens_before(release))
613                                 break;
614                         if (rf->happens_before(act))
615                                 continue;
616
617                         /* Check modification order */
618                         if (mo_graph->checkReachable(rf, act))
619                                 /* rf --mo--> act */
620                                 continue;
621                         if (mo_graph->checkReachable(act, release))
622                                 /* act --mo--> release */
623                                 break;
624                         if (mo_graph->checkReachable(release, act) &&
625                                       mo_graph->checkReachable(act, rf)) {
626                                 /* release --mo-> act --mo--> rf */
627                                 return true; /* complete */
628                         }
629                         certain = false;
630                 }
631         }
632
633         if (certain)
634                 release_heads->push_back(release);
635         return certain;
636 }
637
638 /**
639  * A public interface for getting the release sequence head(s) with which a
640  * given ModelAction must synchronize. This function only returns a non-empty
641  * result when it can locate a release sequence head with certainty. Otherwise,
642  * it may mark the internal state of the ModelChecker so that it will handle
643  * the release sequence at a later time, causing @a act to update its
644  * synchronization at some later point in execution.
645  * @param act The 'acquire' action that may read from a release sequence
646  * @param release_heads A pass-by-reference return parameter. Will be filled
647  * with the head(s) of the release sequence(s), if they exists with certainty.
648  * @see ModelChecker::release_seq_head
649  */
650 void ModelChecker::get_release_seq_heads(ModelAction *act,
651                 std::vector<const ModelAction *> *release_heads)
652 {
653         const ModelAction *rf = act->get_reads_from();
654         bool complete;
655         complete = release_seq_head(rf, release_heads);
656         if (!complete) {
657                 /* add act to 'lazy checking' list */
658                 std::list<ModelAction *> *list;
659                 list = lazy_sync_with_release->get_safe_ptr(act->get_location());
660                 list->push_back(act);
661         }
662 }
663
664 /**
665  * Attempt to resolve all stashed operations that might synchronize with a
666  * release sequence for a given location. This implements the "lazy" portion of
667  * determining whether or not a release sequence was contiguous, since not all
668  * modification order information is present at the time an action occurs.
669  *
670  * @param location The location/object that should be checked for release
671  * sequence resolutions
672  * @return True if any updates occurred (new synchronization, new mo_graph edges)
673  */
674 bool ModelChecker::resolve_release_sequences(void *location)
675 {
676         std::list<ModelAction *> *list;
677         list = lazy_sync_with_release->getptr(location);
678         if (!list)
679                 return false;
680
681         bool updated = false;
682         std::list<ModelAction *>::iterator it = list->begin();
683         while (it != list->end()) {
684                 ModelAction *act = *it;
685                 const ModelAction *rf = act->get_reads_from();
686                 std::vector<const ModelAction *> release_heads;
687                 bool complete;
688                 complete = release_seq_head(rf, &release_heads);
689                 for (unsigned int i = 0; i < release_heads.size(); i++) {
690                         if (!act->has_synchronized_with(release_heads[i])) {
691                                 updated = true;
692                                 act->synchronize_with(release_heads[i]);
693                         }
694                 }
695
696                 if (updated) {
697                         /* propagate synchronization to later actions */
698                         action_list_t::reverse_iterator it = action_trace->rbegin();
699                         while ((*it) != act) {
700                                 ModelAction *propagate = *it;
701                                 if (act->happens_before(propagate))
702                                         /** @todo new mo_graph edges along with
703                                          * this synchronization? */
704                                         propagate->synchronize_with(act);
705                         }
706                 }
707                 if (complete)
708                         it = list->erase(it);
709                 else
710                         it++;
711         }
712
713         // If we resolved promises or data races, see if we have realized a data race.
714         if (checkDataRaces()) {
715                 model->set_assert();
716         }
717
718         return updated;
719 }
720
721 /**
722  * Performs various bookkeeping operations for the current ModelAction. For
723  * instance, adds action to the per-object, per-thread action vector and to the
724  * action trace list of all thread actions.
725  *
726  * @param act is the ModelAction to add.
727  */
728 void ModelChecker::add_action_to_lists(ModelAction *act)
729 {
730         int tid = id_to_int(act->get_tid());
731         action_trace->push_back(act);
732
733         obj_map->get_safe_ptr(act->get_location())->push_back(act);
734
735         std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
736         if (tid >= (int)vec->size())
737                 vec->resize(next_thread_id);
738         (*vec)[tid].push_back(act);
739
740         if ((int)thrd_last_action->size() <= tid)
741                 thrd_last_action->resize(get_num_threads());
742         (*thrd_last_action)[tid] = act;
743 }
744
745 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
746 {
747         int nthreads = get_num_threads();
748         if ((int)thrd_last_action->size() < nthreads)
749                 thrd_last_action->resize(nthreads);
750         return (*thrd_last_action)[id_to_int(tid)];
751 }
752
753 /**
754  * Gets the last memory_order_seq_cst action (in the total global sequence)
755  * performed on a particular object (i.e., memory location).
756  * @param location The object location to check
757  * @return The last seq_cst action performed
758  */
759 ModelAction * ModelChecker::get_last_seq_cst(const void *location)
760 {
761         action_list_t *list = obj_map->get_safe_ptr(location);
762         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
763         action_list_t::reverse_iterator rit;
764         for (rit = list->rbegin(); rit != list->rend(); rit++)
765                 if ((*rit)->is_write() && (*rit)->is_seqcst())
766                         return *rit;
767         return NULL;
768 }
769
770 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
771 {
772         ModelAction *parent = get_last_action(tid);
773         if (!parent)
774                 parent = get_thread(tid)->get_creation();
775         return parent;
776 }
777
778 /**
779  * Returns the clock vector for a given thread.
780  * @param tid The thread whose clock vector we want
781  * @return Desired clock vector
782  */
783 ClockVector * ModelChecker::get_cv(thread_id_t tid)
784 {
785         return get_parent_action(tid)->get_cv();
786 }
787
788 /**
789  * Resolve a set of Promises with a current write. The set is provided in the
790  * Node corresponding to @a write.
791  * @param write The ModelAction that is fulfilling Promises
792  * @return True if promises were resolved; false otherwise
793  */
794 bool ModelChecker::resolve_promises(ModelAction *write)
795 {
796         bool resolved = false;
797         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
798                 Promise *promise = (*promises)[promise_index];
799                 if (write->get_node()->get_promise(i)) {
800                         ModelAction *read = promise->get_action();
801                         read->read_from(write);
802                         r_modification_order(read, write);
803                         post_r_modification_order(read, write);
804                         promises->erase(promises->begin() + promise_index);
805                         resolved = true;
806                 } else
807                         promise_index++;
808         }
809
810         return resolved;
811 }
812
813 /**
814  * Compute the set of promises that could potentially be satisfied by this
815  * action. Note that the set computation actually appears in the Node, not in
816  * ModelChecker.
817  * @param curr The ModelAction that may satisfy promises
818  */
819 void ModelChecker::compute_promises(ModelAction *curr)
820 {
821         for (unsigned int i = 0; i < promises->size(); i++) {
822                 Promise *promise = (*promises)[i];
823                 const ModelAction *act = promise->get_action();
824                 if (!act->happens_before(curr) &&
825                                 act->is_read() &&
826                                 !act->is_synchronizing(curr) &&
827                                 !act->same_thread(curr) &&
828                                 promise->get_value() == curr->get_value()) {
829                         curr->get_node()->set_promise(i);
830                 }
831         }
832 }
833
834 /** Checks promises in response to change in ClockVector Threads. */
835 void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
836 {
837         for (unsigned int i = 0; i < promises->size(); i++) {
838                 Promise *promise = (*promises)[i];
839                 const ModelAction *act = promise->get_action();
840                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
841                                 merge_cv->synchronized_since(act)) {
842                         //This thread is no longer able to send values back to satisfy the promise
843                         int num_synchronized_threads = promise->increment_threads();
844                         if (num_synchronized_threads == model->get_num_threads()) {
845                                 //Promise has failed
846                                 failed_promise = true;
847                                 return;
848                         }
849                 }
850         }
851 }
852
853 /**
854  * Build up an initial set of all past writes that this 'read' action may read
855  * from. This set is determined by the clock vector's "happens before"
856  * relationship.
857  * @param curr is the current ModelAction that we are exploring; it must be a
858  * 'read' operation.
859  */
860 void ModelChecker::build_reads_from_past(ModelAction *curr)
861 {
862         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
863         unsigned int i;
864         ASSERT(curr->is_read());
865
866         ModelAction *last_seq_cst = NULL;
867
868         /* Track whether this object has been initialized */
869         bool initialized = false;
870
871         if (curr->is_seqcst()) {
872                 last_seq_cst = get_last_seq_cst(curr->get_location());
873                 /* We have to at least see the last sequentially consistent write,
874                          so we are initialized. */
875                 if (last_seq_cst != NULL)
876                         initialized = true;
877         }
878
879         /* Iterate over all threads */
880         for (i = 0; i < thrd_lists->size(); i++) {
881                 /* Iterate over actions in thread, starting from most recent */
882                 action_list_t *list = &(*thrd_lists)[i];
883                 action_list_t::reverse_iterator rit;
884                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
885                         ModelAction *act = *rit;
886
887                         /* Only consider 'write' actions */
888                         if (!act->is_write())
889                                 continue;
890
891                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
892                         if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
893                                 DEBUG("Adding action to may_read_from:\n");
894                                 if (DBG_ENABLED()) {
895                                         act->print();
896                                         curr->print();
897                                 }
898                                 curr->get_node()->add_read_from(act);
899                         }
900
901                         /* Include at most one act per-thread that "happens before" curr */
902                         if (act->happens_before(curr)) {
903                                 initialized = true;
904                                 break;
905                         }
906                 }
907         }
908
909         if (!initialized) {
910                 /** @todo Need a more informative way of reporting errors. */
911                 printf("ERROR: may read from uninitialized atomic\n");
912         }
913
914         if (DBG_ENABLED() || !initialized) {
915                 printf("Reached read action:\n");
916                 curr->print();
917                 printf("Printing may_read_from\n");
918                 curr->get_node()->print_may_read_from();
919                 printf("End printing may_read_from\n");
920         }
921
922         ASSERT(initialized);
923 }
924
925 static void print_list(action_list_t *list)
926 {
927         action_list_t::iterator it;
928
929         printf("---------------------------------------------------------------------\n");
930         printf("Trace:\n");
931
932         for (it = list->begin(); it != list->end(); it++) {
933                 (*it)->print();
934         }
935         printf("---------------------------------------------------------------------\n");
936 }
937
938 void ModelChecker::print_summary()
939 {
940         printf("\n");
941         printf("Number of executions: %d\n", num_executions);
942         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
943
944         scheduler->print();
945
946         if (!isfinalfeasible())
947                 printf("INFEASIBLE EXECUTION!\n");
948         print_list(action_trace);
949         printf("\n");
950 }
951
952 /**
953  * Add a Thread to the system for the first time. Should only be called once
954  * per thread.
955  * @param t The Thread to add
956  */
957 void ModelChecker::add_thread(Thread *t)
958 {
959         thread_map->put(id_to_int(t->get_id()), t);
960         scheduler->add_thread(t);
961 }
962
963 void ModelChecker::remove_thread(Thread *t)
964 {
965         scheduler->remove_thread(t);
966 }
967
968 /**
969  * Switch from a user-context to the "master thread" context (a.k.a. system
970  * context). This switch is made with the intention of exploring a particular
971  * model-checking action (described by a ModelAction object). Must be called
972  * from a user-thread context.
973  * @param act The current action that will be explored. Must not be NULL.
974  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
975  */
976 int ModelChecker::switch_to_master(ModelAction *act)
977 {
978         DBG();
979         Thread *old = thread_current();
980         set_current_action(act);
981         old->set_state(THREAD_READY);
982         return Thread::swap(old, &system_context);
983 }
984
985 /**
986  * Takes the next step in the execution, if possible.
987  * @return Returns true (success) if a step was taken and false otherwise.
988  */
989 bool ModelChecker::take_step() {
990         Thread *curr, *next;
991
992         if (has_asserted())
993                 return false;
994
995         curr = thread_current();
996         if (curr) {
997                 if (curr->get_state() == THREAD_READY) {
998                         ASSERT(current_action);
999                         nextThread = check_current_action(current_action);
1000                         current_action = NULL;
1001                         if (!curr->is_blocked() && !curr->is_complete())
1002                                 scheduler->add_thread(curr);
1003                 } else {
1004                         ASSERT(false);
1005                 }
1006         }
1007         next = scheduler->next_thread(nextThread);
1008
1009         /* Infeasible -> don't take any more steps */
1010         if (!isfeasible())
1011                 return false;
1012
1013         if (next)
1014                 next->set_state(THREAD_RUNNING);
1015         DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
1016
1017         /* next == NULL -> don't take any more steps */
1018         if (!next)
1019                 return false;
1020         /* Return false only if swap fails with an error */
1021         return (Thread::swap(&system_context, next) == 0);
1022 }
1023
1024 /** Runs the current execution until threre are no more steps to take. */
1025 void ModelChecker::finish_execution() {
1026         DBG();
1027
1028         while (take_step());
1029 }