common: improve backtrace function
[c11tester.git] / model.cc
1 #include <stdio.h>
2 #include <algorithm>
3
4 #include "model.h"
5 #include "action.h"
6 #include "nodestack.h"
7 #include "schedule.h"
8 #include "snapshot-interface.h"
9 #include "common.h"
10 #include "clockvector.h"
11 #include "cyclegraph.h"
12 #include "promise.h"
13 #include "datarace.h"
14 #include "mutex.h"
15 #include "threads.h"
16
17 #define INITIAL_THREAD_ID       0
18
19 ModelChecker *model;
20
21 /** @brief Constructor */
22 ModelChecker::ModelChecker(struct model_params params) :
23         /* Initialize default scheduler */
24         params(params),
25         scheduler(new Scheduler()),
26         num_executions(0),
27         num_feasible_executions(0),
28         diverge(NULL),
29         earliest_diverge(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         lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
34         obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
35         promises(new std::vector<Promise *>()),
36         futurevalues(new std::vector<struct PendingFutureValue>()),
37         pending_rel_seqs(new std::vector<struct release_seq *>()),
38         thrd_last_action(new std::vector<ModelAction *>(1)),
39         node_stack(new NodeStack()),
40         mo_graph(new CycleGraph()),
41         failed_promise(false),
42         too_many_reads(false),
43         asserted(false),
44         bad_synchronization(false)
45 {
46         /* Allocate this "size" on the snapshotting heap */
47         priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
48         /* First thread created will have id INITIAL_THREAD_ID */
49         priv->next_thread_id = INITIAL_THREAD_ID;
50 }
51
52 /** @brief Destructor */
53 ModelChecker::~ModelChecker()
54 {
55         for (unsigned int i = 0; i < get_num_threads(); i++)
56                 delete thread_map->get(i);
57         delete thread_map;
58
59         delete obj_thrd_map;
60         delete obj_map;
61         delete lock_waiters_map;
62         delete action_trace;
63
64         for (unsigned int i = 0; i < promises->size(); i++)
65                 delete (*promises)[i];
66         delete promises;
67
68         delete pending_rel_seqs;
69
70         delete thrd_last_action;
71         delete node_stack;
72         delete scheduler;
73         delete mo_graph;
74 }
75
76 /**
77  * Restores user program to initial state and resets all model-checker data
78  * structures.
79  */
80 void ModelChecker::reset_to_initial_state()
81 {
82         DEBUG("+++ Resetting to initial state +++\n");
83         node_stack->reset_execution();
84         failed_promise = false;
85         too_many_reads = false;
86         bad_synchronization = false;
87         reset_asserted();
88         snapshotObject->backTrackBeforeStep(0);
89 }
90
91 /** @return a thread ID for a new Thread */
92 thread_id_t ModelChecker::get_next_id()
93 {
94         return priv->next_thread_id++;
95 }
96
97 /** @return the number of user threads created during this execution */
98 unsigned int ModelChecker::get_num_threads()
99 {
100         return priv->next_thread_id;
101 }
102
103 /** @return The currently executing Thread. */
104 Thread * ModelChecker::get_current_thread()
105 {
106         return scheduler->get_current_thread();
107 }
108
109 /** @return a sequence number for a new ModelAction */
110 modelclock_t ModelChecker::get_next_seq_num()
111 {
112         return ++priv->used_sequence_numbers;
113 }
114
115 /**
116  * @brief Choose the next thread to execute.
117  *
118  * This function chooses the next thread that should execute. It can force the
119  * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
120  * followed by a THREAD_START, or it can enforce execution replay/backtracking.
121  * The model-checker may have no preference regarding the next thread (i.e.,
122  * when exploring a new execution ordering), in which case this will return
123  * NULL.
124  * @param curr The current ModelAction. This action might guide the choice of
125  * next thread.
126  * @return The next thread to run. If the model-checker has no preference, NULL.
127  */
128 Thread * ModelChecker::get_next_thread(ModelAction *curr)
129 {
130         thread_id_t tid;
131
132         if (curr!=NULL) {
133                 /* Do not split atomic actions. */
134                 if (curr->is_rmwr())
135                         return thread_current();
136                 /* The THREAD_CREATE action points to the created Thread */
137                 else if (curr->get_type() == THREAD_CREATE)
138                         return (Thread *)curr->get_location();
139         }
140
141         /* Have we completed exploring the preselected path? */
142         if (diverge == NULL)
143                 return NULL;
144
145         /* Else, we are trying to replay an execution */
146         ModelAction *next = node_stack->get_next()->get_action();
147
148         if (next == diverge) {
149                 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
150                         earliest_diverge=diverge;
151
152                 Node *nextnode = next->get_node();
153                 /* Reached divergence point */
154                 if (nextnode->increment_promise()) {
155                         /* The next node will try to satisfy a different set of promises. */
156                         tid = next->get_tid();
157                         node_stack->pop_restofstack(2);
158                 } else if (nextnode->increment_read_from()) {
159                         /* The next node will read from a different value. */
160                         tid = next->get_tid();
161                         node_stack->pop_restofstack(2);
162                 } else if (nextnode->increment_future_value()) {
163                         /* The next node will try to read from a different future value. */
164                         tid = next->get_tid();
165                         node_stack->pop_restofstack(2);
166                 } else {
167                         /* Make a different thread execute for next step */
168                         Node *node = nextnode->get_parent();
169                         tid = node->get_next_backtrack();
170                         node_stack->pop_restofstack(1);
171                         if (diverge==earliest_diverge) {
172                                 earliest_diverge=node->get_action();
173                         }
174                 }
175                 DEBUG("*** Divergence point ***\n");
176
177                 diverge = NULL;
178         } else {
179                 tid = next->get_tid();
180         }
181         DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
182         ASSERT(tid != THREAD_ID_T_NONE);
183         return thread_map->get(id_to_int(tid));
184 }
185
186 /**
187  * Queries the model-checker for more executions to explore and, if one
188  * exists, resets the model-checker state to execute a new execution.
189  *
190  * @return If there are more executions to explore, return true. Otherwise,
191  * return false.
192  */
193 bool ModelChecker::next_execution()
194 {
195         DBG();
196
197         num_executions++;
198
199         if (isfinalfeasible()) {
200                 printf("Earliest divergence point since last feasible execution:\n");
201                 if (earliest_diverge)
202                         earliest_diverge->print();
203                 else
204                         printf("(Not set)\n");
205
206                 earliest_diverge = NULL;
207                 num_feasible_executions++;
208         }
209
210         DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
211                         pending_rel_seqs->size());
212
213         if (isfinalfeasible() || DBG_ENABLED())
214                 print_summary();
215
216         if ((diverge = get_next_backtrack()) == NULL)
217                 return false;
218
219         if (DBG_ENABLED()) {
220                 printf("Next execution will diverge at:\n");
221                 diverge->print();
222         }
223
224         reset_to_initial_state();
225         return true;
226 }
227
228 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
229 {
230         switch (act->get_type()) {
231         case ATOMIC_READ:
232         case ATOMIC_WRITE:
233         case ATOMIC_RMW: {
234                 /* linear search: from most recent to oldest */
235                 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
236                 action_list_t::reverse_iterator rit;
237                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
238                         ModelAction *prev = *rit;
239                         if (prev->could_synchronize_with(act))
240                                 return prev;
241                 }
242                 break;
243         }
244         case ATOMIC_LOCK:
245         case ATOMIC_TRYLOCK: {
246                 /* linear search: from most recent to oldest */
247                 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
248                 action_list_t::reverse_iterator rit;
249                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
250                         ModelAction *prev = *rit;
251                         if (act->is_conflicting_lock(prev))
252                                 return prev;
253                 }
254                 break;
255         }
256         case ATOMIC_UNLOCK: {
257                 /* linear search: from most recent to oldest */
258                 action_list_t *list = obj_map->get_safe_ptr(act->get_location());
259                 action_list_t::reverse_iterator rit;
260                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
261                         ModelAction *prev = *rit;
262                         if (!act->same_thread(prev)&&prev->is_failed_trylock())
263                                 return prev;
264                 }
265                 break;
266         }
267         default:
268                 break;
269         }
270         return NULL;
271 }
272
273 /** This method find backtracking points where we should try to
274  * reorder the parameter ModelAction against.
275  *
276  * @param the ModelAction to find backtracking points for.
277  */
278 void ModelChecker::set_backtracking(ModelAction *act)
279 {
280         Thread *t = get_thread(act);
281         ModelAction * prev = get_last_conflict(act);
282         if (prev == NULL)
283                 return;
284
285         Node * node = prev->get_node()->get_parent();
286
287         int low_tid, high_tid;
288         if (node->is_enabled(t)) {
289                 low_tid = id_to_int(act->get_tid());
290                 high_tid = low_tid+1;
291         } else {
292                 low_tid = 0;
293                 high_tid = get_num_threads();
294         }
295
296         for(int i = low_tid; i < high_tid; i++) {
297                 thread_id_t tid = int_to_id(i);
298                 if (!node->is_enabled(tid))
299                         continue;
300
301                 /* Check if this has been explored already */
302                 if (node->has_been_explored(tid))
303                         continue;
304
305                 /* See if fairness allows */
306                 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
307                         bool unfair=false;
308                         for(int t=0;t<node->get_num_threads();t++) {
309                                 thread_id_t tother=int_to_id(t);
310                                 if (node->is_enabled(tother) && node->has_priority(tother)) {
311                                         unfair=true;
312                                         break;
313                                 }
314                         }
315                         if (unfair)
316                                 continue;
317                 }
318
319                 /* Cache the latest backtracking point */
320                 if (!priv->next_backtrack || *prev > *priv->next_backtrack)
321                         priv->next_backtrack = prev;
322
323                 /* If this is a new backtracking point, mark the tree */
324                 if (!node->set_backtrack(tid))
325                         continue;
326                 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
327                                         id_to_int(prev->get_tid()),
328                                         id_to_int(t->get_id()));
329                 if (DBG_ENABLED()) {
330                         prev->print();
331                         act->print();
332                 }
333         }
334 }
335
336 /**
337  * Returns last backtracking point. The model checker will explore a different
338  * path for this point in the next execution.
339  * @return The ModelAction at which the next execution should diverge.
340  */
341 ModelAction * ModelChecker::get_next_backtrack()
342 {
343         ModelAction *next = priv->next_backtrack;
344         priv->next_backtrack = NULL;
345         return next;
346 }
347
348 /**
349  * Processes a read or rmw model action.
350  * @param curr is the read model action to process.
351  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
352  * @return True if processing this read updates the mo_graph.
353  */
354 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
355 {
356         uint64_t value;
357         bool updated = false;
358         while (true) {
359                 const ModelAction *reads_from = curr->get_node()->get_read_from();
360                 if (reads_from != NULL) {
361                         mo_graph->startChanges();
362
363                         value = reads_from->get_value();
364                         bool r_status = false;
365
366                         if (!second_part_of_rmw) {
367                                 check_recency(curr, reads_from);
368                                 r_status = r_modification_order(curr, reads_from);
369                         }
370
371
372                         if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
373                                 mo_graph->rollbackChanges();
374                                 too_many_reads = false;
375                                 continue;
376                         }
377
378                         curr->read_from(reads_from);
379                         mo_graph->commitChanges();
380                         mo_check_promises(curr->get_tid(), reads_from);
381
382                         updated |= r_status;
383                 } else if (!second_part_of_rmw) {
384                         /* Read from future value */
385                         value = curr->get_node()->get_future_value();
386                         modelclock_t expiration = curr->get_node()->get_future_value_expiration();
387                         curr->read_from(NULL);
388                         Promise *valuepromise = new Promise(curr, value, expiration);
389                         promises->push_back(valuepromise);
390                 }
391                 get_thread(curr)->set_return_value(value);
392                 return updated;
393         }
394 }
395
396 /**
397  * Processes a lock, trylock, or unlock model action.  @param curr is
398  * the read model action to process.
399  *
400  * The try lock operation checks whether the lock is taken.  If not,
401  * it falls to the normal lock operation case.  If so, it returns
402  * fail.
403  *
404  * The lock operation has already been checked that it is enabled, so
405  * it just grabs the lock and synchronizes with the previous unlock.
406  *
407  * The unlock operation has to re-enable all of the threads that are
408  * waiting on the lock.
409  *
410  * @return True if synchronization was updated; false otherwise
411  */
412 bool ModelChecker::process_mutex(ModelAction *curr) {
413         std::mutex *mutex = (std::mutex *)curr->get_location();
414         struct std::mutex_state *state = mutex->get_state();
415         switch (curr->get_type()) {
416         case ATOMIC_TRYLOCK: {
417                 bool success = !state->islocked;
418                 curr->set_try_lock(success);
419                 if (!success) {
420                         get_thread(curr)->set_return_value(0);
421                         break;
422                 }
423                 get_thread(curr)->set_return_value(1);
424         }
425                 //otherwise fall into the lock case
426         case ATOMIC_LOCK: {
427                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
428                         printf("Lock access before initialization\n");
429                         set_assert();
430                 }
431                 state->islocked = true;
432                 ModelAction *unlock = get_last_unlock(curr);
433                 //synchronize with the previous unlock statement
434                 if (unlock != NULL) {
435                         curr->synchronize_with(unlock);
436                         return true;
437                 }
438                 break;
439         }
440         case ATOMIC_UNLOCK: {
441                 //unlock the lock
442                 state->islocked = false;
443                 //wake up the other threads
444                 action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
445                 //activate all the waiting threads
446                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
447                         scheduler->wake(get_thread(*rit));
448                 }
449                 waiters->clear();
450                 break;
451         }
452         default:
453                 ASSERT(0);
454         }
455         return false;
456 }
457
458 /**
459  * Process a write ModelAction
460  * @param curr The ModelAction to process
461  * @return True if the mo_graph was updated or promises were resolved
462  */
463 bool ModelChecker::process_write(ModelAction *curr)
464 {
465         bool updated_mod_order = w_modification_order(curr);
466         bool updated_promises = resolve_promises(curr);
467
468         if (promises->size() == 0) {
469                 for (unsigned int i = 0; i < futurevalues->size(); i++) {
470                         struct PendingFutureValue pfv = (*futurevalues)[i];
471                         if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
472                                         (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
473                                 priv->next_backtrack = pfv.act;
474                 }
475                 futurevalues->resize(0);
476         }
477
478         mo_graph->commitChanges();
479         mo_check_promises(curr->get_tid(), curr);
480
481         get_thread(curr)->set_return_value(VALUE_NONE);
482         return updated_mod_order || updated_promises;
483 }
484
485 /**
486  * @brief Process the current action for thread-related activity
487  *
488  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
489  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
490  * synchronization, etc.  This function is a no-op for non-THREAD actions
491  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
492  *
493  * @param curr The current action
494  * @return True if synchronization was updated or a thread completed
495  */
496 bool ModelChecker::process_thread_action(ModelAction *curr)
497 {
498         bool updated = false;
499
500         switch (curr->get_type()) {
501         case THREAD_CREATE: {
502                 Thread *th = (Thread *)curr->get_location();
503                 th->set_creation(curr);
504                 break;
505         }
506         case THREAD_JOIN: {
507                 Thread *waiting, *blocking;
508                 waiting = get_thread(curr);
509                 blocking = (Thread *)curr->get_location();
510                 if (!blocking->is_complete()) {
511                         blocking->push_wait_list(curr);
512                         scheduler->sleep(waiting);
513                 } else {
514                         do_complete_join(curr);
515                         updated = true; /* trigger rel-seq checks */
516                 }
517                 break;
518         }
519         case THREAD_FINISH: {
520                 Thread *th = get_thread(curr);
521                 while (!th->wait_list_empty()) {
522                         ModelAction *act = th->pop_wait_list();
523                         Thread *wake = get_thread(act);
524                         scheduler->wake(wake);
525                         do_complete_join(act);
526                         updated = true; /* trigger rel-seq checks */
527                 }
528                 th->complete();
529                 updated = true; /* trigger rel-seq checks */
530                 break;
531         }
532         case THREAD_START: {
533                 check_promises(curr->get_tid(), NULL, curr->get_cv());
534                 break;
535         }
536         default:
537                 break;
538         }
539
540         return updated;
541 }
542
543 /**
544  * Initialize the current action by performing one or more of the following
545  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
546  * in the NodeStack, manipulating backtracking sets, allocating and
547  * initializing clock vectors, and computing the promises to fulfill.
548  *
549  * @param curr The current action, as passed from the user context; may be
550  * freed/invalidated after the execution of this function
551  * @return The current action, as processed by the ModelChecker. Is only the
552  * same as the parameter @a curr if this is a newly-explored action.
553  */
554 ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
555 {
556         ModelAction *newcurr;
557
558         if (curr->is_rmwc() || curr->is_rmw()) {
559                 newcurr = process_rmw(curr);
560                 delete curr;
561
562                 if (newcurr->is_rmw())
563                         compute_promises(newcurr);
564                 return newcurr;
565         }
566
567         curr->set_seq_number(get_next_seq_num());
568
569         newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
570         if (newcurr) {
571                 /* First restore type and order in case of RMW operation */
572                 if (curr->is_rmwr())
573                         newcurr->copy_typeandorder(curr);
574
575                 ASSERT(curr->get_location() == newcurr->get_location());
576                 newcurr->copy_from_new(curr);
577
578                 /* Discard duplicate ModelAction; use action from NodeStack */
579                 delete curr;
580
581                 /* Always compute new clock vector */
582                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
583         } else {
584                 newcurr = curr;
585
586                 /* Always compute new clock vector */
587                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
588                 /*
589                  * Perform one-time actions when pushing new ModelAction onto
590                  * NodeStack
591                  */
592                 if (newcurr->is_write())
593                         compute_promises(newcurr);
594         }
595         return newcurr;
596 }
597
598 /**
599  * This method checks whether a model action is enabled at the given point.
600  * At this point, it checks whether a lock operation would be successful at this point.
601  * If not, it puts the thread in a waiter list.
602  * @param curr is the ModelAction to check whether it is enabled.
603  * @return a bool that indicates whether the action is enabled.
604  */
605 bool ModelChecker::check_action_enabled(ModelAction *curr) {
606         if (curr->is_lock()) {
607                 std::mutex * lock = (std::mutex *)curr->get_location();
608                 struct std::mutex_state * state = lock->get_state();
609                 if (state->islocked) {
610                         //Stick the action in the appropriate waiting queue
611                         lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
612                         return false;
613                 }
614         }
615
616         return true;
617 }
618
619 /**
620  * This is the heart of the model checker routine. It performs model-checking
621  * actions corresponding to a given "current action." Among other processes, it
622  * calculates reads-from relationships, updates synchronization clock vectors,
623  * forms a memory_order constraints graph, and handles replay/backtrack
624  * execution when running permutations of previously-observed executions.
625  *
626  * @param curr The current action to process
627  * @return The next Thread that must be executed. May be NULL if ModelChecker
628  * makes no choice (e.g., according to replay execution, combining RMW actions,
629  * etc.)
630  */
631 Thread * ModelChecker::check_current_action(ModelAction *curr)
632 {
633         ASSERT(curr);
634
635         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
636
637         if (!check_action_enabled(curr)) {
638                 /* Make the execution look like we chose to run this action
639                  * much later, when a lock is actually available to release */
640                 get_current_thread()->set_pending(curr);
641                 scheduler->sleep(get_current_thread());
642                 return get_next_thread(NULL);
643         }
644
645         ModelAction *newcurr = initialize_curr_action(curr);
646
647         /* Add the action to lists before any other model-checking tasks */
648         if (!second_part_of_rmw)
649                 add_action_to_lists(newcurr);
650
651         /* Build may_read_from set for newly-created actions */
652         if (curr == newcurr && curr->is_read())
653                 build_reads_from_past(curr);
654         curr = newcurr;
655
656         /* Initialize work_queue with the "current action" work */
657         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
658
659         while (!work_queue.empty()) {
660                 WorkQueueEntry work = work_queue.front();
661                 work_queue.pop_front();
662
663                 switch (work.type) {
664                 case WORK_CHECK_CURR_ACTION: {
665                         ModelAction *act = work.action;
666                         bool update = false; /* update this location's release seq's */
667                         bool update_all = false; /* update all release seq's */
668
669                         if (process_thread_action(curr))
670                                 update_all = true;
671
672                         if (act->is_read() && process_read(act, second_part_of_rmw))
673                                 update = true;
674
675                         if (act->is_write() && process_write(act))
676                                 update = true;
677
678                         if (act->is_mutex_op() && process_mutex(act))
679                                 update_all = true;
680
681                         if (update_all)
682                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
683                         else if (update)
684                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
685                         break;
686                 }
687                 case WORK_CHECK_RELEASE_SEQ:
688                         resolve_release_sequences(work.location, &work_queue);
689                         break;
690                 case WORK_CHECK_MO_EDGES: {
691                         /** @todo Complete verification of work_queue */
692                         ModelAction *act = work.action;
693                         bool updated = false;
694
695                         if (act->is_read()) {
696                                 const ModelAction *rf = act->get_reads_from();
697                                 if (rf != NULL && r_modification_order(act, rf))
698                                         updated = true;
699                         }
700                         if (act->is_write()) {
701                                 if (w_modification_order(act))
702                                         updated = true;
703                         }
704                         mo_graph->commitChanges();
705
706                         if (updated)
707                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
708                         break;
709                 }
710                 default:
711                         ASSERT(false);
712                         break;
713                 }
714         }
715
716         check_curr_backtracking(curr);
717
718         set_backtracking(curr);
719
720         return get_next_thread(curr);
721 }
722
723 /**
724  * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
725  * operation from the Thread it is joining with. Must be called after the
726  * completion of the Thread in question.
727  * @param join The THREAD_JOIN action
728  */
729 void ModelChecker::do_complete_join(ModelAction *join)
730 {
731         Thread *blocking = (Thread *)join->get_location();
732         ModelAction *act = get_last_action(blocking->get_id());
733         join->synchronize_with(act);
734 }
735
736 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
737         Node *currnode = curr->get_node();
738         Node *parnode = currnode->get_parent();
739
740         if ((!parnode->backtrack_empty() ||
741                          !currnode->read_from_empty() ||
742                          !currnode->future_value_empty() ||
743                          !currnode->promise_empty())
744                         && (!priv->next_backtrack ||
745                                         *curr > *priv->next_backtrack)) {
746                 priv->next_backtrack = curr;
747         }
748 }
749
750 bool ModelChecker::promises_expired() {
751         for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
752                 Promise *promise = (*promises)[promise_index];
753                 if (promise->get_expiration()<priv->used_sequence_numbers) {
754                         return true;
755                 }
756         }
757         return false;
758 }
759
760 /** @return whether the current partial trace must be a prefix of a
761  * feasible trace. */
762 bool ModelChecker::isfeasibleprefix() {
763         return promises->size() == 0 && pending_rel_seqs->size() == 0;
764 }
765
766 /** @return whether the current partial trace is feasible. */
767 bool ModelChecker::isfeasible() {
768         if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
769                 DEBUG("Infeasible: RMW violation\n");
770
771         return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
772 }
773
774 /** @return whether the current partial trace is feasible other than
775  * multiple RMW reading from the same store. */
776 bool ModelChecker::isfeasibleotherthanRMW() {
777         if (DBG_ENABLED()) {
778                 if (mo_graph->checkForCycles())
779                         DEBUG("Infeasible: modification order cycles\n");
780                 if (failed_promise)
781                         DEBUG("Infeasible: failed promise\n");
782                 if (too_many_reads)
783                         DEBUG("Infeasible: too many reads\n");
784                 if (bad_synchronization)
785                         DEBUG("Infeasible: bad synchronization ordering\n");
786                 if (promises_expired())
787                         DEBUG("Infeasible: promises expired\n");
788         }
789         return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
790 }
791
792 /** Returns whether the current completed trace is feasible. */
793 bool ModelChecker::isfinalfeasible() {
794         if (DBG_ENABLED() && promises->size() != 0)
795                 DEBUG("Infeasible: unrevolved promises\n");
796
797         return isfeasible() && promises->size() == 0;
798 }
799
800 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
801 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
802         ModelAction *lastread = get_last_action(act->get_tid());
803         lastread->process_rmw(act);
804         if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
805                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
806                 mo_graph->commitChanges();
807         }
808         return lastread;
809 }
810
811 /**
812  * Checks whether a thread has read from the same write for too many times
813  * without seeing the effects of a later write.
814  *
815  * Basic idea:
816  * 1) there must a different write that we could read from that would satisfy the modification order,
817  * 2) we must have read from the same value in excess of maxreads times, and
818  * 3) that other write must have been in the reads_from set for maxreads times.
819  *
820  * If so, we decide that the execution is no longer feasible.
821  */
822 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
823         if (params.maxreads != 0) {
824
825                 if (curr->get_node()->get_read_from_size() <= 1)
826                         return;
827                 //Must make sure that execution is currently feasible...  We could
828                 //accidentally clear by rolling back
829                 if (!isfeasible())
830                         return;
831                 std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
832                 int tid = id_to_int(curr->get_tid());
833
834                 /* Skip checks */
835                 if ((int)thrd_lists->size() <= tid)
836                         return;
837                 action_list_t *list = &(*thrd_lists)[tid];
838
839                 action_list_t::reverse_iterator rit = list->rbegin();
840                 /* Skip past curr */
841                 for (; (*rit) != curr; rit++)
842                         ;
843                 /* go past curr now */
844                 rit++;
845
846                 action_list_t::reverse_iterator ritcopy = rit;
847                 //See if we have enough reads from the same value
848                 int count = 0;
849                 for (; count < params.maxreads; rit++,count++) {
850                         if (rit==list->rend())
851                                 return;
852                         ModelAction *act = *rit;
853                         if (!act->is_read())
854                                 return;
855                         
856                         if (act->get_reads_from() != rf)
857                                 return;
858                         if (act->get_node()->get_read_from_size() <= 1)
859                                 return;
860                 }
861                 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
862                         //Get write
863                         const ModelAction * write = curr->get_node()->get_read_from_at(i);
864
865                         //Need a different write
866                         if (write==rf)
867                                 continue;
868
869                         /* Test to see whether this is a feasible write to read from*/
870                         mo_graph->startChanges();
871                         r_modification_order(curr, write);
872                         bool feasiblereadfrom = isfeasible();
873                         mo_graph->rollbackChanges();
874
875                         if (!feasiblereadfrom)
876                                 continue;
877                         rit = ritcopy;
878
879                         bool feasiblewrite = true;
880                         //new we need to see if this write works for everyone
881
882                         for (int loop = count; loop>0; loop--,rit++) {
883                                 ModelAction *act=*rit;
884                                 bool foundvalue = false;
885                                 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
886                                         if (act->get_node()->get_read_from_at(i)==write) {
887                                                 foundvalue = true;
888                                                 break;
889                                         }
890                                 }
891                                 if (!foundvalue) {
892                                         feasiblewrite = false;
893                                         break;
894                                 }
895                         }
896                         if (feasiblewrite) {
897                                 too_many_reads = true;
898                                 return;
899                         }
900                 }
901         }
902 }
903
904 /**
905  * Updates the mo_graph with the constraints imposed from the current
906  * read.
907  *
908  * Basic idea is the following: Go through each other thread and find
909  * the lastest action that happened before our read.  Two cases:
910  *
911  * (1) The action is a write => that write must either occur before
912  * the write we read from or be the write we read from.
913  *
914  * (2) The action is a read => the write that that action read from
915  * must occur before the write we read from or be the same write.
916  *
917  * @param curr The current action. Must be a read.
918  * @param rf The action that curr reads from. Must be a write.
919  * @return True if modification order edges were added; false otherwise
920  */
921 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
922 {
923         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
924         unsigned int i;
925         bool added = false;
926         ASSERT(curr->is_read());
927
928         /* Iterate over all threads */
929         for (i = 0; i < thrd_lists->size(); i++) {
930                 /* Iterate over actions in thread, starting from most recent */
931                 action_list_t *list = &(*thrd_lists)[i];
932                 action_list_t::reverse_iterator rit;
933                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
934                         ModelAction *act = *rit;
935
936                         /*
937                          * Include at most one act per-thread that "happens
938                          * before" curr. Don't consider reflexively.
939                          */
940                         if (act->happens_before(curr) && act != curr) {
941                                 if (act->is_write()) {
942                                         if (rf != act) {
943                                                 mo_graph->addEdge(act, rf);
944                                                 added = true;
945                                         }
946                                 } else {
947                                         const ModelAction *prevreadfrom = act->get_reads_from();
948                                         //if the previous read is unresolved, keep going...
949                                         if (prevreadfrom == NULL)
950                                                 continue;
951
952                                         if (rf != prevreadfrom) {
953                                                 mo_graph->addEdge(prevreadfrom, rf);
954                                                 added = true;
955                                         }
956                                 }
957                                 break;
958                         }
959                 }
960         }
961
962         return added;
963 }
964
965 /** This method fixes up the modification order when we resolve a
966  *  promises.  The basic problem is that actions that occur after the
967  *  read curr could not property add items to the modification order
968  *  for our read.
969  *
970  *  So for each thread, we find the earliest item that happens after
971  *  the read curr.  This is the item we have to fix up with additional
972  *  constraints.  If that action is write, we add a MO edge between
973  *  the Action rf and that action.  If the action is a read, we add a
974  *  MO edge between the Action rf, and whatever the read accessed.
975  *
976  * @param curr is the read ModelAction that we are fixing up MO edges for.
977  * @param rf is the write ModelAction that curr reads from.
978  *
979  */
980 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
981 {
982         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
983         unsigned int i;
984         ASSERT(curr->is_read());
985
986         /* Iterate over all threads */
987         for (i = 0; i < thrd_lists->size(); i++) {
988                 /* Iterate over actions in thread, starting from most recent */
989                 action_list_t *list = &(*thrd_lists)[i];
990                 action_list_t::reverse_iterator rit;
991                 ModelAction *lastact = NULL;
992
993                 /* Find last action that happens after curr that is either not curr or a rmw */
994                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
995                         ModelAction *act = *rit;
996                         if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
997                                 lastact = act;
998                         } else
999                                 break;
1000                 }
1001
1002                         /* Include at most one act per-thread that "happens before" curr */
1003                 if (lastact != NULL) {
1004                         if (lastact==curr) {
1005                                 //Case 1: The resolved read is a RMW, and we need to make sure
1006                                 //that the write portion of the RMW mod order after rf
1007
1008                                 mo_graph->addEdge(rf, lastact);
1009                         } else if (lastact->is_read()) {
1010                                 //Case 2: The resolved read is a normal read and the next
1011                                 //operation is a read, and we need to make sure the value read
1012                                 //is mod ordered after rf
1013
1014                                 const ModelAction *postreadfrom = lastact->get_reads_from();
1015                                 if (postreadfrom != NULL&&rf != postreadfrom)
1016                                         mo_graph->addEdge(rf, postreadfrom);
1017                         } else {
1018                                 //Case 3: The resolved read is a normal read and the next
1019                                 //operation is a write, and we need to make sure that the
1020                                 //write is mod ordered after rf
1021                                 if (lastact!=rf)
1022                                         mo_graph->addEdge(rf, lastact);
1023                         }
1024                         break;
1025                 }
1026         }
1027 }
1028
1029 /**
1030  * Updates the mo_graph with the constraints imposed from the current write.
1031  *
1032  * Basic idea is the following: Go through each other thread and find
1033  * the lastest action that happened before our write.  Two cases:
1034  *
1035  * (1) The action is a write => that write must occur before
1036  * the current write
1037  *
1038  * (2) The action is a read => the write that that action read from
1039  * must occur before the current write.
1040  *
1041  * This method also handles two other issues:
1042  *
1043  * (I) Sequential Consistency: Making sure that if the current write is
1044  * seq_cst, that it occurs after the previous seq_cst write.
1045  *
1046  * (II) Sending the write back to non-synchronizing reads.
1047  *
1048  * @param curr The current action. Must be a write.
1049  * @return True if modification order edges were added; false otherwise
1050  */
1051 bool ModelChecker::w_modification_order(ModelAction *curr)
1052 {
1053         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1054         unsigned int i;
1055         bool added = false;
1056         ASSERT(curr->is_write());
1057
1058         if (curr->is_seqcst()) {
1059                 /* We have to at least see the last sequentially consistent write,
1060                          so we are initialized. */
1061                 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1062                 if (last_seq_cst != NULL) {
1063                         mo_graph->addEdge(last_seq_cst, curr);
1064                         added = true;
1065                 }
1066         }
1067
1068         /* Iterate over all threads */
1069         for (i = 0; i < thrd_lists->size(); i++) {
1070                 /* Iterate over actions in thread, starting from most recent */
1071                 action_list_t *list = &(*thrd_lists)[i];
1072                 action_list_t::reverse_iterator rit;
1073                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1074                         ModelAction *act = *rit;
1075                         if (act == curr) {
1076                                 /*
1077                                  * 1) If RMW and it actually read from something, then we
1078                                  * already have all relevant edges, so just skip to next
1079                                  * thread.
1080                                  * 
1081                                  * 2) If RMW and it didn't read from anything, we should
1082                                  * whatever edge we can get to speed up convergence.
1083                                  *
1084                                  * 3) If normal write, we need to look at earlier actions, so
1085                                  * continue processing list.
1086                                  */
1087                                 if (curr->is_rmw()) {
1088                                         if (curr->get_reads_from()!=NULL)
1089                                                 break;
1090                                         else 
1091                                                 continue;
1092                                 } else
1093                                         continue;
1094                         }
1095
1096                         /*
1097                          * Include at most one act per-thread that "happens
1098                          * before" curr
1099                          */
1100                         if (act->happens_before(curr)) {
1101                                 /*
1102                                  * Note: if act is RMW, just add edge:
1103                                  *   act --mo--> curr
1104                                  * The following edge should be handled elsewhere:
1105                                  *   readfrom(act) --mo--> act
1106                                  */
1107                                 if (act->is_write())
1108                                         mo_graph->addEdge(act, curr);
1109                                 else if (act->is_read()) { 
1110                                         //if previous read accessed a null, just keep going
1111                                         if (act->get_reads_from() == NULL)
1112                                                 continue;
1113                                         mo_graph->addEdge(act->get_reads_from(), curr);
1114                                 }
1115                                 added = true;
1116                                 break;
1117                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1118                                                      !act->same_thread(curr)) {
1119                                 /* We have an action that:
1120                                    (1) did not happen before us
1121                                    (2) is a read and we are a write
1122                                    (3) cannot synchronize with us
1123                                    (4) is in a different thread
1124                                    =>
1125                                    that read could potentially read from our write.
1126                                  */
1127                                 if (thin_air_constraint_may_allow(curr, act)) {
1128                                         if (isfeasible() ||
1129                                                         (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1130                                                 struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act};
1131                                                 futurevalues->push_back(pfv);
1132                                         }
1133                                 }
1134                         }
1135                 }
1136         }
1137
1138         return added;
1139 }
1140
1141 /** Arbitrary reads from the future are not allowed.  Section 29.3
1142  * part 9 places some constraints.  This method checks one result of constraint
1143  * constraint.  Others require compiler support. */
1144 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1145         if (!writer->is_rmw())
1146                 return true;
1147
1148         if (!reader->is_rmw())
1149                 return true;
1150
1151         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1152                 if (search == reader)
1153                         return false;
1154                 if (search->get_tid() == reader->get_tid() &&
1155                                 search->happens_before(reader))
1156                         break;
1157         }
1158
1159         return true;
1160 }
1161
1162 /**
1163  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1164  * The ModelAction under consideration is expected to be taking part in
1165  * release/acquire synchronization as an object of the "reads from" relation.
1166  * Note that this can only provide release sequence support for RMW chains
1167  * which do not read from the future, as those actions cannot be traced until
1168  * their "promise" is fulfilled. Similarly, we may not even establish the
1169  * presence of a release sequence with certainty, as some modification order
1170  * constraints may be decided further in the future. Thus, this function
1171  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1172  * and a boolean representing certainty.
1173  *
1174  * @todo Finish lazy updating, when promises are fulfilled in the future
1175  * @param rf The action that might be part of a release sequence. Must be a
1176  * write.
1177  * @param release_heads A pass-by-reference style return parameter. After
1178  * execution of this function, release_heads will contain the heads of all the
1179  * relevant release sequences, if any exists with certainty
1180  * @param pending A pass-by-reference style return parameter which is only used
1181  * when returning false (i.e., uncertain). Returns most information regarding
1182  * an uncertain release sequence, including any write operations that might
1183  * break the sequence.
1184  * @return true, if the ModelChecker is certain that release_heads is complete;
1185  * false otherwise
1186  */
1187 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1188                 rel_heads_list_t *release_heads,
1189                 struct release_seq *pending) const
1190 {
1191         /* Only check for release sequences if there are no cycles */
1192         if (mo_graph->checkForCycles())
1193                 return false;
1194
1195         while (rf) {
1196                 ASSERT(rf->is_write());
1197
1198                 if (rf->is_release())
1199                         release_heads->push_back(rf);
1200                 if (!rf->is_rmw())
1201                         break; /* End of RMW chain */
1202
1203                 /** @todo Need to be smarter here...  In the linux lock
1204                  * example, this will run to the beginning of the program for
1205                  * every acquire. */
1206                 /** @todo The way to be smarter here is to keep going until 1
1207                  * thread has a release preceded by an acquire and you've seen
1208                  *       both. */
1209
1210                 /* acq_rel RMW is a sufficient stopping condition */
1211                 if (rf->is_acquire() && rf->is_release())
1212                         return true; /* complete */
1213
1214                 rf = rf->get_reads_from();
1215         };
1216         if (!rf) {
1217                 /* read from future: need to settle this later */
1218                 pending->rf = NULL;
1219                 return false; /* incomplete */
1220         }
1221
1222         if (rf->is_release())
1223                 return true; /* complete */
1224
1225         /* else relaxed write; check modification order for contiguous subsequence
1226          * -> rf must be same thread as release */
1227         int tid = id_to_int(rf->get_tid());
1228         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
1229         action_list_t *list = &(*thrd_lists)[tid];
1230         action_list_t::const_reverse_iterator rit;
1231
1232         /* Find rf in the thread list */
1233         rit = std::find(list->rbegin(), list->rend(), rf);
1234         ASSERT(rit != list->rend());
1235
1236         /* Find the last write/release */
1237         for (; rit != list->rend(); rit++)
1238                 if ((*rit)->is_release())
1239                         break;
1240         if (rit == list->rend()) {
1241                 /* No write-release in this thread */
1242                 return true; /* complete */
1243         }
1244         ModelAction *release = *rit;
1245
1246         ASSERT(rf->same_thread(release));
1247
1248         pending->writes.clear();
1249
1250         bool certain = true;
1251         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1252                 if (id_to_int(rf->get_tid()) == (int)i)
1253                         continue;
1254                 list = &(*thrd_lists)[i];
1255
1256                 /* Can we ensure no future writes from this thread may break
1257                  * the release seq? */
1258                 bool future_ordered = false;
1259
1260                 ModelAction *last = get_last_action(int_to_id(i));
1261                 Thread *th = get_thread(int_to_id(i));
1262                 if ((last && rf->happens_before(last)) ||
1263                                 !scheduler->is_enabled(th) ||
1264                                 th->is_complete())
1265                         future_ordered = true;
1266
1267                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1268                         const ModelAction *act = *rit;
1269                         /* Reach synchronization -> this thread is complete */
1270                         if (act->happens_before(release))
1271                                 break;
1272                         if (rf->happens_before(act)) {
1273                                 future_ordered = true;
1274                                 continue;
1275                         }
1276
1277                         /* Only writes can break release sequences */
1278                         if (!act->is_write())
1279                                 continue;
1280
1281                         /* Check modification order */
1282                         if (mo_graph->checkReachable(rf, act)) {
1283                                 /* rf --mo--> act */
1284                                 future_ordered = true;
1285                                 continue;
1286                         }
1287                         if (mo_graph->checkReachable(act, release))
1288                                 /* act --mo--> release */
1289                                 break;
1290                         if (mo_graph->checkReachable(release, act) &&
1291                                       mo_graph->checkReachable(act, rf)) {
1292                                 /* release --mo-> act --mo--> rf */
1293                                 return true; /* complete */
1294                         }
1295                         /* act may break release sequence */
1296                         pending->writes.push_back(act);
1297                         certain = false;
1298                 }
1299                 if (!future_ordered)
1300                         certain = false; /* This thread is uncertain */
1301         }
1302
1303         if (certain) {
1304                 release_heads->push_back(release);
1305                 pending->writes.clear();
1306         } else {
1307                 pending->release = release;
1308                 pending->rf = rf;
1309         }
1310         return certain;
1311 }
1312
1313 /**
1314  * A public interface for getting the release sequence head(s) with which a
1315  * given ModelAction must synchronize. This function only returns a non-empty
1316  * result when it can locate a release sequence head with certainty. Otherwise,
1317  * it may mark the internal state of the ModelChecker so that it will handle
1318  * the release sequence at a later time, causing @a act to update its
1319  * synchronization at some later point in execution.
1320  * @param act The 'acquire' action that may read from a release sequence
1321  * @param release_heads A pass-by-reference return parameter. Will be filled
1322  * with the head(s) of the release sequence(s), if they exists with certainty.
1323  * @see ModelChecker::release_seq_heads
1324  */
1325 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1326 {
1327         const ModelAction *rf = act->get_reads_from();
1328         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1329         sequence->acquire = act;
1330
1331         if (!release_seq_heads(rf, release_heads, sequence)) {
1332                 /* add act to 'lazy checking' list */
1333                 pending_rel_seqs->push_back(sequence);
1334         } else {
1335                 snapshot_free(sequence);
1336         }
1337 }
1338
1339 /**
1340  * Attempt to resolve all stashed operations that might synchronize with a
1341  * release sequence for a given location. This implements the "lazy" portion of
1342  * determining whether or not a release sequence was contiguous, since not all
1343  * modification order information is present at the time an action occurs.
1344  *
1345  * @param location The location/object that should be checked for release
1346  * sequence resolutions. A NULL value means to check all locations.
1347  * @param work_queue The work queue to which to add work items as they are
1348  * generated
1349  * @return True if any updates occurred (new synchronization, new mo_graph
1350  * edges)
1351  */
1352 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1353 {
1354         bool updated = false;
1355         std::vector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
1356         while (it != pending_rel_seqs->end()) {
1357                 struct release_seq *pending = *it;
1358                 ModelAction *act = pending->acquire;
1359
1360                 /* Only resolve sequences on the given location, if provided */
1361                 if (location && act->get_location() != location) {
1362                         it++;
1363                         continue;
1364                 }
1365
1366                 const ModelAction *rf = act->get_reads_from();
1367                 rel_heads_list_t release_heads;
1368                 bool complete;
1369                 complete = release_seq_heads(rf, &release_heads, pending);
1370                 for (unsigned int i = 0; i < release_heads.size(); i++) {
1371                         if (!act->has_synchronized_with(release_heads[i])) {
1372                                 if (act->synchronize_with(release_heads[i]))
1373                                         updated = true;
1374                                 else
1375                                         set_bad_synchronization();
1376                         }
1377                 }
1378
1379                 if (updated) {
1380                         /* Re-check all pending release sequences */
1381                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1382                         /* Re-check act for mo_graph edges */
1383                         work_queue->push_back(MOEdgeWorkEntry(act));
1384
1385                         /* propagate synchronization to later actions */
1386                         action_list_t::reverse_iterator rit = action_trace->rbegin();
1387                         for (; (*rit) != act; rit++) {
1388                                 ModelAction *propagate = *rit;
1389                                 if (act->happens_before(propagate)) {
1390                                         propagate->synchronize_with(act);
1391                                         /* Re-check 'propagate' for mo_graph edges */
1392                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
1393                                 }
1394                         }
1395                 }
1396                 if (complete) {
1397                         it = pending_rel_seqs->erase(it);
1398                         snapshot_free(pending);
1399                 } else {
1400                         it++;
1401                 }
1402         }
1403
1404         // If we resolved promises or data races, see if we have realized a data race.
1405         if (checkDataRaces()) {
1406                 set_assert();
1407         }
1408
1409         return updated;
1410 }
1411
1412 /**
1413  * Performs various bookkeeping operations for the current ModelAction. For
1414  * instance, adds action to the per-object, per-thread action vector and to the
1415  * action trace list of all thread actions.
1416  *
1417  * @param act is the ModelAction to add.
1418  */
1419 void ModelChecker::add_action_to_lists(ModelAction *act)
1420 {
1421         int tid = id_to_int(act->get_tid());
1422         action_trace->push_back(act);
1423
1424         obj_map->get_safe_ptr(act->get_location())->push_back(act);
1425
1426         std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
1427         if (tid >= (int)vec->size())
1428                 vec->resize(priv->next_thread_id);
1429         (*vec)[tid].push_back(act);
1430
1431         if ((int)thrd_last_action->size() <= tid)
1432                 thrd_last_action->resize(get_num_threads());
1433         (*thrd_last_action)[tid] = act;
1434 }
1435
1436 /**
1437  * @brief Get the last action performed by a particular Thread
1438  * @param tid The thread ID of the Thread in question
1439  * @return The last action in the thread
1440  */
1441 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1442 {
1443         int threadid = id_to_int(tid);
1444         if (threadid < (int)thrd_last_action->size())
1445                 return (*thrd_last_action)[id_to_int(tid)];
1446         else
1447                 return NULL;
1448 }
1449
1450 /**
1451  * Gets the last memory_order_seq_cst write (in the total global sequence)
1452  * performed on a particular object (i.e., memory location), not including the
1453  * current action.
1454  * @param curr The current ModelAction; also denotes the object location to
1455  * check
1456  * @return The last seq_cst write
1457  */
1458 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1459 {
1460         void *location = curr->get_location();
1461         action_list_t *list = obj_map->get_safe_ptr(location);
1462         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1463         action_list_t::reverse_iterator rit;
1464         for (rit = list->rbegin(); rit != list->rend(); rit++)
1465                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1466                         return *rit;
1467         return NULL;
1468 }
1469
1470 /**
1471  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1472  * location). This function identifies the mutex according to the current
1473  * action, which is presumed to perform on the same mutex.
1474  * @param curr The current ModelAction; also denotes the object location to
1475  * check
1476  * @return The last unlock operation
1477  */
1478 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1479 {
1480         void *location = curr->get_location();
1481         action_list_t *list = obj_map->get_safe_ptr(location);
1482         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1483         action_list_t::reverse_iterator rit;
1484         for (rit = list->rbegin(); rit != list->rend(); rit++)
1485                 if ((*rit)->is_unlock())
1486                         return *rit;
1487         return NULL;
1488 }
1489
1490 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1491 {
1492         ModelAction *parent = get_last_action(tid);
1493         if (!parent)
1494                 parent = get_thread(tid)->get_creation();
1495         return parent;
1496 }
1497
1498 /**
1499  * Returns the clock vector for a given thread.
1500  * @param tid The thread whose clock vector we want
1501  * @return Desired clock vector
1502  */
1503 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1504 {
1505         return get_parent_action(tid)->get_cv();
1506 }
1507
1508 /**
1509  * Resolve a set of Promises with a current write. The set is provided in the
1510  * Node corresponding to @a write.
1511  * @param write The ModelAction that is fulfilling Promises
1512  * @return True if promises were resolved; false otherwise
1513  */
1514 bool ModelChecker::resolve_promises(ModelAction *write)
1515 {
1516         bool resolved = false;
1517   std::vector<thread_id_t> threads_to_check;
1518
1519         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
1520                 Promise *promise = (*promises)[promise_index];
1521                 if (write->get_node()->get_promise(i)) {
1522                         ModelAction *read = promise->get_action();
1523                         if (read->is_rmw()) {
1524                                 mo_graph->addRMWEdge(write, read);
1525                         }
1526                         read->read_from(write);
1527                         //First fix up the modification order for actions that happened
1528                         //before the read
1529                         r_modification_order(read, write);
1530                         //Next fix up the modification order for actions that happened
1531                         //after the read.
1532                         post_r_modification_order(read, write);
1533                         //Make sure the promise's value matches the write's value
1534                         ASSERT(promise->get_value() == write->get_value());
1535                         delete(promise);
1536                         
1537                         promises->erase(promises->begin() + promise_index);
1538                         threads_to_check.push_back(read->get_tid());
1539
1540                         resolved = true;
1541                 } else
1542                         promise_index++;
1543         }
1544
1545         //Check whether reading these writes has made threads unable to
1546         //resolve promises
1547
1548         for(unsigned int i=0;i<threads_to_check.size();i++)
1549                 mo_check_promises(threads_to_check[i], write);
1550
1551         return resolved;
1552 }
1553
1554 /**
1555  * Compute the set of promises that could potentially be satisfied by this
1556  * action. Note that the set computation actually appears in the Node, not in
1557  * ModelChecker.
1558  * @param curr The ModelAction that may satisfy promises
1559  */
1560 void ModelChecker::compute_promises(ModelAction *curr)
1561 {
1562         for (unsigned int i = 0; i < promises->size(); i++) {
1563                 Promise *promise = (*promises)[i];
1564                 const ModelAction *act = promise->get_action();
1565                 if (!act->happens_before(curr) &&
1566                                 act->is_read() &&
1567                                 !act->could_synchronize_with(curr) &&
1568                                 !act->same_thread(curr) &&
1569                                 promise->get_value() == curr->get_value()) {
1570                         curr->get_node()->set_promise(i);
1571                 }
1572         }
1573 }
1574
1575 /** Checks promises in response to change in ClockVector Threads. */
1576 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
1577 {
1578         for (unsigned int i = 0; i < promises->size(); i++) {
1579                 Promise *promise = (*promises)[i];
1580                 const ModelAction *act = promise->get_action();
1581                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
1582                                 merge_cv->synchronized_since(act)) {
1583                         if (promise->increment_threads(tid)) {
1584                                 //Promise has failed
1585                                 failed_promise = true;
1586                                 return;
1587                         }
1588                 }
1589         }
1590 }
1591
1592 /** Checks promises in response to addition to modification order for threads.
1593  * Definitions:
1594  * pthread is the thread that performed the read that created the promise
1595  * 
1596  * pread is the read that created the promise
1597  *
1598  * pwrite is either the first write to same location as pread by
1599  * pthread that is sequenced after pread or the value read by the
1600  * first read to the same lcoation as pread by pthread that is
1601  * sequenced after pread..
1602  *
1603  *      1. If tid=pthread, then we check what other threads are reachable
1604  * through the mode order starting with pwrite.  Those threads cannot
1605  * perform a write that will resolve the promise due to modification
1606  * order constraints.
1607  *
1608  * 2. If the tid is not pthread, we check whether pwrite can reach the
1609  * action write through the modification order.  If so, that thread
1610  * cannot perform a future write that will resolve the promise due to
1611  * modificatin order constraints.
1612  *
1613  *      @parem tid The thread that either read from the model action
1614  *      write, or actually did the model action write.
1615  *
1616  *      @parem write The ModelAction representing the relevant write.
1617  */
1618
1619 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
1620         void * location = write->get_location();
1621         for (unsigned int i = 0; i < promises->size(); i++) {
1622                 Promise *promise = (*promises)[i];
1623                 const ModelAction *act = promise->get_action();
1624                 
1625                 //Is this promise on the same location?
1626                 if ( act->get_location() != location )
1627                         continue;
1628
1629                 //same thread as the promise
1630                 if ( act->get_tid()==tid ) {
1631
1632                         //do we have a pwrite for the promise, if not, set it
1633                         if (promise->get_write() == NULL ) {
1634                                 promise->set_write(write);
1635                         }
1636                         if (mo_graph->checkPromise(write, promise)) {
1637                                 failed_promise = true;
1638                                 return;
1639                         }
1640                 }
1641                 
1642                 //Don't do any lookups twice for the same thread
1643                 if (promise->has_sync_thread(tid))
1644                         continue;
1645                 
1646                 if (mo_graph->checkReachable(promise->get_write(), write)) {
1647                         if (promise->increment_threads(tid)) {
1648                                 failed_promise = true;
1649                                 return;
1650                         }
1651                 }
1652         }
1653 }
1654
1655 /**
1656  * Build up an initial set of all past writes that this 'read' action may read
1657  * from. This set is determined by the clock vector's "happens before"
1658  * relationship.
1659  * @param curr is the current ModelAction that we are exploring; it must be a
1660  * 'read' operation.
1661  */
1662 void ModelChecker::build_reads_from_past(ModelAction *curr)
1663 {
1664         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
1665         unsigned int i;
1666         ASSERT(curr->is_read());
1667
1668         ModelAction *last_seq_cst = NULL;
1669
1670         /* Track whether this object has been initialized */
1671         bool initialized = false;
1672
1673         if (curr->is_seqcst()) {
1674                 last_seq_cst = get_last_seq_cst(curr);
1675                 /* We have to at least see the last sequentially consistent write,
1676                          so we are initialized. */
1677                 if (last_seq_cst != NULL)
1678                         initialized = true;
1679         }
1680
1681         /* Iterate over all threads */
1682         for (i = 0; i < thrd_lists->size(); i++) {
1683                 /* Iterate over actions in thread, starting from most recent */
1684                 action_list_t *list = &(*thrd_lists)[i];
1685                 action_list_t::reverse_iterator rit;
1686                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1687                         ModelAction *act = *rit;
1688
1689                         /* Only consider 'write' actions */
1690                         if (!act->is_write() || act == curr)
1691                                 continue;
1692
1693                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1694                         if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
1695                                 DEBUG("Adding action to may_read_from:\n");
1696                                 if (DBG_ENABLED()) {
1697                                         act->print();
1698                                         curr->print();
1699                                 }
1700                                 curr->get_node()->add_read_from(act);
1701                         }
1702
1703                         /* Include at most one act per-thread that "happens before" curr */
1704                         if (act->happens_before(curr)) {
1705                                 initialized = true;
1706                                 break;
1707                         }
1708                 }
1709         }
1710
1711         if (!initialized) {
1712                 /** @todo Need a more informative way of reporting errors. */
1713                 printf("ERROR: may read from uninitialized atomic\n");
1714         }
1715
1716         if (DBG_ENABLED() || !initialized) {
1717                 printf("Reached read action:\n");
1718                 curr->print();
1719                 printf("Printing may_read_from\n");
1720                 curr->get_node()->print_may_read_from();
1721                 printf("End printing may_read_from\n");
1722         }
1723
1724         ASSERT(initialized);
1725 }
1726
1727 static void print_list(action_list_t *list)
1728 {
1729         action_list_t::iterator it;
1730
1731         printf("---------------------------------------------------------------------\n");
1732         printf("Trace:\n");
1733
1734         for (it = list->begin(); it != list->end(); it++) {
1735                 (*it)->print();
1736         }
1737         printf("---------------------------------------------------------------------\n");
1738 }
1739
1740 #if SUPPORT_MOD_ORDER_DUMP
1741 void ModelChecker::dumpGraph(char *filename) {
1742         char buffer[200];
1743   sprintf(buffer, "%s.dot",filename);
1744   FILE *file=fopen(buffer, "w");
1745   fprintf(file, "digraph %s {\n",filename);
1746         mo_graph->dumpNodes(file);
1747         ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
1748         
1749         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
1750                 ModelAction *action=*it;
1751                 if (action->is_read()) {
1752                         fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
1753                         if (action->get_reads_from()!=NULL)
1754                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
1755                 }
1756                 if (thread_array[action->get_tid()] != NULL) {
1757                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
1758                 }
1759                 
1760                 thread_array[action->get_tid()]=action;
1761         }
1762   fprintf(file,"}\n");
1763         model_free(thread_array);
1764   fclose(file); 
1765 }
1766 #endif
1767
1768 void ModelChecker::print_summary()
1769 {
1770         printf("\n");
1771         printf("Number of executions: %d\n", num_executions);
1772         printf("Number of feasible executions: %d\n", num_feasible_executions);
1773         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
1774
1775 #if SUPPORT_MOD_ORDER_DUMP
1776         scheduler->print();
1777         char buffername[100];
1778         sprintf(buffername, "exec%04u", num_executions);
1779         mo_graph->dumpGraphToFile(buffername);
1780         sprintf(buffername, "graph%04u", num_executions);
1781   dumpGraph(buffername);
1782 #endif
1783
1784         if (!isfinalfeasible())
1785                 printf("INFEASIBLE EXECUTION!\n");
1786         print_list(action_trace);
1787         printf("\n");
1788 }
1789
1790 /**
1791  * Add a Thread to the system for the first time. Should only be called once
1792  * per thread.
1793  * @param t The Thread to add
1794  */
1795 void ModelChecker::add_thread(Thread *t)
1796 {
1797         thread_map->put(id_to_int(t->get_id()), t);
1798         scheduler->add_thread(t);
1799 }
1800
1801 /**
1802  * Removes a thread from the scheduler. 
1803  * @param the thread to remove.
1804  */
1805 void ModelChecker::remove_thread(Thread *t)
1806 {
1807         scheduler->remove_thread(t);
1808 }
1809
1810 /**
1811  * @brief Get a Thread reference by its ID
1812  * @param tid The Thread's ID
1813  * @return A Thread reference
1814  */
1815 Thread * ModelChecker::get_thread(thread_id_t tid) const
1816 {
1817         return thread_map->get(id_to_int(tid));
1818 }
1819
1820 /**
1821  * @brief Get a reference to the Thread in which a ModelAction was executed
1822  * @param act The ModelAction
1823  * @return A Thread reference
1824  */
1825 Thread * ModelChecker::get_thread(ModelAction *act) const
1826 {
1827         return get_thread(act->get_tid());
1828 }
1829
1830 /**
1831  * Switch from a user-context to the "master thread" context (a.k.a. system
1832  * context). This switch is made with the intention of exploring a particular
1833  * model-checking action (described by a ModelAction object). Must be called
1834  * from a user-thread context.
1835  *
1836  * @param act The current action that will be explored. May be NULL only if
1837  * trace is exiting via an assertion (see ModelChecker::set_assert and
1838  * ModelChecker::has_asserted).
1839  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
1840  */
1841 int ModelChecker::switch_to_master(ModelAction *act)
1842 {
1843         DBG();
1844         Thread *old = thread_current();
1845         set_current_action(act);
1846         old->set_state(THREAD_READY);
1847         return Thread::swap(old, &system_context);
1848 }
1849
1850 /**
1851  * Takes the next step in the execution, if possible.
1852  * @return Returns true (success) if a step was taken and false otherwise.
1853  */
1854 bool ModelChecker::take_step() {
1855         if (has_asserted())
1856                 return false;
1857
1858         Thread *curr = thread_current();
1859         if (curr) {
1860                 if (curr->get_state() == THREAD_READY) {
1861                         ASSERT(priv->current_action);
1862
1863                         priv->nextThread = check_current_action(priv->current_action);
1864                         priv->current_action = NULL;
1865
1866                         if (curr->is_blocked() || curr->is_complete())
1867                                 scheduler->remove_thread(curr);
1868                 } else {
1869                         ASSERT(false);
1870                 }
1871         }
1872         Thread *next = scheduler->next_thread(priv->nextThread);
1873
1874         /* Infeasible -> don't take any more steps */
1875         if (!isfeasible())
1876                 return false;
1877
1878         DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
1879                         next ? id_to_int(next->get_id()) : -1);
1880
1881         /* next == NULL -> don't take any more steps */
1882         if (!next)
1883                 return false;
1884
1885         next->set_state(THREAD_RUNNING);
1886
1887         if (next->get_pending() != NULL) {
1888                 /* restart a pending action */
1889                 set_current_action(next->get_pending());
1890                 next->set_pending(NULL);
1891                 next->set_state(THREAD_READY);
1892                 return true;
1893         }
1894
1895         /* Return false only if swap fails with an error */
1896         return (Thread::swap(&system_context, next) == 0);
1897 }
1898
1899 /** Runs the current execution until threre are no more steps to take. */
1900 void ModelChecker::finish_execution() {
1901         DBG();
1902
1903         while (take_step());
1904 }