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