bfa3e02997ee42ed860fcf872d297906a6ac38b5
[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
13 #define INITIAL_THREAD_ID       0
14
15 ModelChecker *model;
16
17 /** @brief Constructor */
18 ModelChecker::ModelChecker()
19         :
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
26         num_executions(0),
27         current_action(NULL),
28         diverge(NULL),
29         nextThread(THREAD_ID_T_NONE),
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 *>(1)),
35         thrd_last_action(new std::vector<ModelAction *>(1)),
36         node_stack(new NodeStack()),
37         next_backtrack(NULL),
38         cyclegraph(new CycleGraph())
39 {
40 }
41
42 /** @brief Destructor */
43 ModelChecker::~ModelChecker()
44 {
45         /*      std::map<int, Thread *>::iterator it;
46         for (it = thread_map->begin(); it != thread_map->end(); it++)
47         delete (*it).second;*/
48         delete thread_map;
49
50         delete obj_thrd_map;
51         delete obj_map;
52         delete action_trace;
53         delete thrd_last_action;
54         delete node_stack;
55         delete scheduler;
56         delete cyclegraph;
57 }
58
59 /**
60  * Restores user program to initial state and resets all model-checker data
61  * structures.
62  */
63 void ModelChecker::reset_to_initial_state()
64 {
65         DEBUG("+++ Resetting to initial state +++\n");
66         node_stack->reset_execution();
67         current_action = NULL;
68         next_thread_id = INITIAL_THREAD_ID;
69         used_sequence_numbers = 0;
70         nextThread = 0;
71         next_backtrack = NULL;
72         snapshotObject->backTrackBeforeStep(0);
73 }
74
75 /** @returns a thread ID for a new Thread */
76 thread_id_t ModelChecker::get_next_id()
77 {
78         return next_thread_id++;
79 }
80
81 /** @returns the number of user threads created during this execution */
82 int ModelChecker::get_num_threads()
83 {
84         return next_thread_id;
85 }
86
87 /** @returns a sequence number for a new ModelAction */
88 modelclock_t ModelChecker::get_next_seq_num()
89 {
90         return ++used_sequence_numbers;
91 }
92
93 /**
94  * Performs the "scheduling" for the model-checker. That is, it checks if the
95  * model-checker has selected a "next thread to run" and returns it, if
96  * available. This function should be called from the Scheduler routine, where
97  * the Scheduler falls back to a default scheduling routine if needed.
98  *
99  * @return The next thread chosen by the model-checker. If the model-checker
100  * makes no selection, retuns NULL.
101  */
102 Thread * ModelChecker::schedule_next_thread()
103 {
104         Thread *t;
105         if (nextThread == THREAD_ID_T_NONE)
106                 return NULL;
107         t = thread_map->get(id_to_int(nextThread));
108
109         ASSERT(t != NULL);
110
111         return t;
112 }
113
114 /**
115  * Choose the next thread in the replay sequence.
116  *
117  * If the replay sequence has reached the 'diverge' point, returns a thread
118  * from the backtracking set. Otherwise, simply returns the next thread in the
119  * sequence that is being replayed.
120  */
121 thread_id_t ModelChecker::get_next_replay_thread()
122 {
123         thread_id_t tid;
124
125         /* Have we completed exploring the preselected path? */
126         if (diverge == NULL)
127                 return THREAD_ID_T_NONE;
128
129         /* Else, we are trying to replay an execution */
130         ModelAction * next = node_stack->get_next()->get_action();
131
132         if (next == diverge) {
133                 Node *nextnode = next->get_node();
134                 /* Reached divergence point */
135                 if (nextnode->increment_read_from()) {
136                         /* The next node will read from a different value */
137                         tid = next->get_tid();
138                         node_stack->pop_restofstack(2);
139                 } else {
140                         /* Make a different thread execute for next step */
141                         Node *node = nextnode->get_parent();
142                         tid = node->get_next_backtrack();
143                         node_stack->pop_restofstack(1);
144                 }
145                 DEBUG("*** Divergence point ***\n");
146                 diverge = NULL;
147         } else {
148                 tid = next->get_tid();
149         }
150         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
151         return tid;
152 }
153
154 /**
155  * Queries the model-checker for more executions to explore and, if one
156  * exists, resets the model-checker state to execute a new execution.
157  *
158  * @return If there are more executions to explore, return true. Otherwise,
159  * return false.
160  */
161 bool ModelChecker::next_execution()
162 {
163         DBG();
164
165         num_executions++;
166
167         if (isfeasible() || DBG_ENABLED())
168                 print_summary();
169
170         if ((diverge = model->get_next_backtrack()) == NULL)
171                 return false;
172
173         if (DBG_ENABLED()) {
174                 printf("Next execution will diverge at:\n");
175                 diverge->print();
176         }
177
178         model->reset_to_initial_state();
179         return true;
180 }
181
182 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
183 {
184         action_type type = act->get_type();
185
186         switch (type) {
187                 case ATOMIC_READ:
188                 case ATOMIC_WRITE:
189                 case ATOMIC_RMW:
190                         break;
191                 default:
192                         return NULL;
193         }
194         /* linear search: from most recent to oldest */
195         action_list_t *list = obj_map->ensureptr(act->get_location());
196         action_list_t::reverse_iterator rit;
197         for (rit = list->rbegin(); rit != list->rend(); rit++) {
198                 ModelAction *prev = *rit;
199                 if (act->is_synchronizing(prev))
200                         return prev;
201         }
202         return NULL;
203 }
204
205 void ModelChecker::set_backtracking(ModelAction *act)
206 {
207         ModelAction *prev;
208         Node *node;
209         Thread *t = get_thread(act->get_tid());
210
211         prev = get_last_conflict(act);
212         if (prev == NULL)
213                 return;
214
215         node = prev->get_node()->get_parent();
216
217         while (!node->is_enabled(t))
218                 t = t->get_parent();
219
220         /* Check if this has been explored already */
221         if (node->has_been_explored(t->get_id()))
222                 return;
223
224         /* Cache the latest backtracking point */
225         if (!next_backtrack || *prev > *next_backtrack)
226                 next_backtrack = prev;
227
228         /* If this is a new backtracking point, mark the tree */
229         if (!node->set_backtrack(t->get_id()))
230                 return;
231         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
232                         prev->get_tid(), t->get_id());
233         if (DBG_ENABLED()) {
234                 prev->print();
235                 act->print();
236         }
237 }
238
239 /**
240  * Returns last backtracking point. The model checker will explore a different
241  * path for this point in the next execution.
242  * @return The ModelAction at which the next execution should diverge.
243  */
244 ModelAction * ModelChecker::get_next_backtrack()
245 {
246         ModelAction *next = next_backtrack;
247         next_backtrack = NULL;
248         return next;
249 }
250
251 void ModelChecker::check_current_action(void)
252 {
253         ModelAction *curr = this->current_action;
254         bool already_added = false;
255         this->current_action = NULL;
256         if (!curr) {
257                 DEBUG("trying to push NULL action...\n");
258                 return;
259         }
260
261         if (curr->is_rmwc()||curr->is_rmw()) {
262                 ModelAction *tmp=process_rmw(curr);
263                 already_added = true;
264                 delete curr;
265                 curr=tmp;
266         } else {
267                 ModelAction * tmp = node_stack->explore_action(curr);
268                 if (tmp) {
269                         /* Discard duplicate ModelAction; use action from NodeStack */
270                         /* First restore type and order in case of RMW operation */
271                         if (curr->is_rmwr())
272                                 tmp->copy_typeandorder(curr);
273                         delete curr;
274                         curr = tmp;
275                 } else {
276                         /*
277                          * Perform one-time actions when pushing new ModelAction onto
278                          * NodeStack
279                          */
280                         curr->create_cv(get_parent_action(curr->get_tid()));
281                         /* Build may_read_from set */
282                         if (curr->is_read())
283                                 build_reads_from_past(curr);
284                 }
285         }
286
287         /* Assign 'creation' parent */
288         if (curr->get_type() == THREAD_CREATE) {
289                 Thread *th = (Thread *)curr->get_location();
290                 th->set_creation(curr);
291         }
292
293         /* Assign reads_from values */
294         Thread *th = get_thread(curr->get_tid());
295         uint64_t value = VALUE_NONE;
296         if (curr->is_read()) {
297                 const ModelAction *reads_from = curr->get_node()->get_read_from();
298                 value = reads_from->get_value();
299                 /* Assign reads_from, perform release/acquire synchronization */
300                 curr->read_from(reads_from);
301                 r_modification_order(curr,reads_from);
302         } else if (curr->is_write()) {
303                 w_modification_order(curr);
304         }
305
306         th->set_return_value(value);
307
308         /* Add action to list.  */
309         if (!already_added)
310                 add_action_to_lists(curr);
311
312         /* Is there a better interface for setting the next thread rather
313                  than this field/convoluted approach?  Perhaps like just returning
314                  it or something? */
315
316         /* Do not split atomic actions. */
317         if (curr->is_rmwr()) {
318                 nextThread = thread_current()->get_id();
319         } else {
320                 nextThread = get_next_replay_thread();
321         }
322
323         Node *currnode = curr->get_node();
324         Node *parnode = currnode->get_parent();
325
326         if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
327                 if (!next_backtrack || *curr > *next_backtrack)
328                         next_backtrack = curr;
329
330         set_backtracking(curr);
331 }
332
333 /** @returns whether the current trace is feasible. */
334 bool ModelChecker::isfeasible() {
335         return !cyclegraph->checkForCycles();
336 }
337
338 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
339 ModelAction * ModelChecker::process_rmw(ModelAction * act) {
340         int tid = id_to_int(act->get_tid());
341         ModelAction *lastread=get_last_action(tid);
342         lastread->process_rmw(act);
343         if (act->is_rmw())
344                 cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
345         return lastread;
346 }
347
348 /**
349  * Updates the cyclegraph with the constraints imposed from the current read.
350  * @param curr The current action. Must be a read.
351  * @param rf The action that curr reads from. Must be a write.
352  */
353 void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
354         std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
355         unsigned int i;
356         ASSERT(curr->is_read());
357
358         /* Iterate over all threads */
359         for (i = 0; i < thrd_lists->size(); i++) {
360                 /* Iterate over actions in thread, starting from most recent */
361                 action_list_t *list = &(*thrd_lists)[i];
362                 action_list_t::reverse_iterator rit;
363                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
364                         ModelAction *act = *rit;
365
366                         /* Include at most one act per-thread that "happens before" curr */
367                         if (act->happens_before(curr)) {
368                                 if (act->is_read()) {
369                                         const ModelAction * prevreadfrom=act->get_reads_from();
370                                         if (rf!=prevreadfrom)
371                                                 cyclegraph->addEdge(rf, prevreadfrom);
372                                 } else if (rf!=act) {
373                                         cyclegraph->addEdge(rf, act);
374                                 }
375                                 break;
376                         }
377                 }
378         }
379 }
380
381 /**
382  * Updates the cyclegraph with the constraints imposed from the current write.
383  * @param curr The current action. Must be a write.
384  */
385 void ModelChecker::w_modification_order(ModelAction * curr) {
386         std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
387         unsigned int i;
388         ASSERT(curr->is_write());
389
390         if (curr->is_seqcst()) {
391                 /* We have to at least see the last sequentially consistent write,
392                          so we are initialized. */
393                 ModelAction * last_seq_cst=get_last_seq_cst(curr->get_location());
394                 if (last_seq_cst!=NULL)
395                         cyclegraph->addEdge(curr, last_seq_cst);
396         }
397
398         /* Iterate over all threads */
399         for (i = 0; i < thrd_lists->size(); i++) {
400                 /* Iterate over actions in thread, starting from most recent */
401                 action_list_t *list = &(*thrd_lists)[i];
402                 action_list_t::reverse_iterator rit;
403                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
404                         ModelAction *act = *rit;
405
406                         /* Include at most one act per-thread that "happens before" curr */
407                         if (act->happens_before(curr)) {
408                                 if (act->is_read()) {
409                                         cyclegraph->addEdge(curr, act->get_reads_from());
410                                 } else
411                                         cyclegraph->addEdge(curr, act);
412                                 break;
413                         }
414                 }
415         }
416 }
417
418 /**
419  * Performs various bookkeeping operations for the current ModelAction. For
420  * instance, adds action to the per-object, per-thread action vector and to the
421  * action trace list of all thread actions.
422  *
423  * @param act is the ModelAction to add.
424  */
425 void ModelChecker::add_action_to_lists(ModelAction *act)
426 {
427         int tid = id_to_int(act->get_tid());
428         action_trace->push_back(act);
429
430         obj_map->ensureptr(act->get_location())->push_back(act);
431
432         std::vector<action_list_t> *vec = obj_thrd_map->ensureptr(act->get_location());
433         if (tid >= (int)vec->size())
434                 vec->resize(next_thread_id);
435         (*vec)[tid].push_back(act);
436
437         if ((int)thrd_last_action->size() <= tid)
438                 thrd_last_action->resize(get_num_threads());
439         (*thrd_last_action)[tid] = act;
440 }
441
442 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
443 {
444         int nthreads = get_num_threads();
445         if ((int)thrd_last_action->size() < nthreads)
446                 thrd_last_action->resize(nthreads);
447         return (*thrd_last_action)[id_to_int(tid)];
448 }
449
450 /**
451  * Gets the last memory_order_seq_cst action (in the total global sequence)
452  * performed on a particular object (i.e., memory location).
453  * @param location The object location to check
454  * @return The last seq_cst action performed
455  */
456 ModelAction * ModelChecker::get_last_seq_cst(const void *location)
457 {
458         action_list_t *list = obj_map->ensureptr(location);
459         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
460         action_list_t::reverse_iterator rit;
461         for (rit = list->rbegin(); rit != list->rend(); rit++)
462                 if ((*rit)->is_write() && (*rit)->is_seqcst())
463                         return *rit;
464         return NULL;
465 }
466
467 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
468 {
469         ModelAction *parent = get_last_action(tid);
470         if (!parent)
471                 parent = get_thread(tid)->get_creation();
472         return parent;
473 }
474
475 /**
476  * Returns the clock vector for a given thread.
477  * @param tid The thread whose clock vector we want
478  * @return Desired clock vector
479  */
480 ClockVector * ModelChecker::get_cv(thread_id_t tid) {
481         return get_parent_action(tid)->get_cv();
482 }
483
484 /**
485  * Build up an initial set of all past writes that this 'read' action may read
486  * from. This set is determined by the clock vector's "happens before"
487  * relationship.
488  * @param curr is the current ModelAction that we are exploring; it must be a
489  * 'read' operation.
490  */
491 void ModelChecker::build_reads_from_past(ModelAction *curr)
492 {
493         std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
494         unsigned int i;
495         ASSERT(curr->is_read());
496
497         ModelAction *last_seq_cst = NULL;
498
499         /* Track whether this object has been initialized */
500         bool initialized = false;
501
502         if (curr->is_seqcst()) {
503                 last_seq_cst = get_last_seq_cst(curr->get_location());
504                 /* We have to at least see the last sequentially consistent write,
505                          so we are initialized. */
506                 if (last_seq_cst != NULL)
507                         initialized = true;
508         }
509
510         /* Iterate over all threads */
511         for (i = 0; i < thrd_lists->size(); i++) {
512                 /* Iterate over actions in thread, starting from most recent */
513                 action_list_t *list = &(*thrd_lists)[i];
514                 action_list_t::reverse_iterator rit;
515                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
516                         ModelAction *act = *rit;
517
518                         /* Only consider 'write' actions */
519                         if (!act->is_write())
520                                 continue;
521
522                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
523                         if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
524                                 DEBUG("Adding action to may_read_from:\n");
525                                 if (DBG_ENABLED()) {
526                                         act->print();
527                                         curr->print();
528                                 }
529                                 curr->get_node()->add_read_from(act);
530                         }
531
532                         /* Include at most one act per-thread that "happens before" curr */
533                         if (act->happens_before(curr)) {
534                                 initialized = true;
535                                 break;
536                         }
537                 }
538         }
539
540         if (!initialized) {
541                 /** @todo Need a more informative way of reporting errors. */
542                 printf("ERROR: may read from uninitialized atomic\n");
543         }
544
545         if (DBG_ENABLED() || !initialized) {
546                 printf("Reached read action:\n");
547                 curr->print();
548                 printf("Printing may_read_from\n");
549                 curr->get_node()->print_may_read_from();
550                 printf("End printing may_read_from\n");
551         }
552
553         ASSERT(initialized);
554 }
555
556 static void print_list(action_list_t *list)
557 {
558         action_list_t::iterator it;
559
560         printf("---------------------------------------------------------------------\n");
561         printf("Trace:\n");
562
563         for (it = list->begin(); it != list->end(); it++) {
564                 (*it)->print();
565         }
566         printf("---------------------------------------------------------------------\n");
567 }
568
569 void ModelChecker::print_summary(void)
570 {
571         printf("\n");
572         printf("Number of executions: %d\n", num_executions);
573         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
574
575         scheduler->print();
576
577         if (!isfeasible())
578                 printf("INFEASIBLE EXECUTION!\n");
579         print_list(action_trace);
580         printf("\n");
581 }
582
583 int ModelChecker::add_thread(Thread *t)
584 {
585         thread_map->put(id_to_int(t->get_id()), t);
586         scheduler->add_thread(t);
587         return 0;
588 }
589
590 void ModelChecker::remove_thread(Thread *t)
591 {
592         scheduler->remove_thread(t);
593 }
594
595 /**
596  * Switch from a user-context to the "master thread" context (a.k.a. system
597  * context). This switch is made with the intention of exploring a particular
598  * model-checking action (described by a ModelAction object). Must be called
599  * from a user-thread context.
600  * @param act The current action that will be explored. May be NULL, although
601  * there is little reason to switch to the model-checker without an action to
602  * explore (note: act == NULL is sometimes used as a hack to allow a thread to
603  * yield control without performing any progress; see thrd_join()).
604  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
605  */
606 int ModelChecker::switch_to_master(ModelAction *act)
607 {
608         DBG();
609         Thread * old = thread_current();
610         set_current_action(act);
611         old->set_state(THREAD_READY);
612         return Thread::swap(old, get_system_context());
613 }