execution: embed snapshotted data structures in class
[model-checker.git] / action.cc
1 #include <stdio.h>
2 #define __STDC_FORMAT_MACROS
3 #include <inttypes.h>
4 #include <stdlib.h>
5
6 #include "model.h"
7 #include "action.h"
8 #include "clockvector.h"
9 #include "common.h"
10 #include "threads-model.h"
11 #include "nodestack.h"
12
13 #define ACTION_INITIAL_CLOCK 0
14
15 /** @brief A special value to represent a successful trylock */
16 #define VALUE_TRYSUCCESS 1
17
18 /** @brief A special value to represent a failed trylock */
19 #define VALUE_TRYFAILED 0
20
21 /**
22  * @brief Construct a new ModelAction
23  *
24  * @param type The type of action
25  * @param order The memory order of this action. A "don't care" for non-ATOMIC
26  * actions (e.g., THREAD_* or MODEL_* actions).
27  * @param loc The location that this action acts upon
28  * @param value (optional) A value associated with the action (e.g., the value
29  * read or written). Defaults to a given macro constant, for debugging purposes.
30  * @param thread (optional) The Thread in which this action occurred. If NULL
31  * (default), then a Thread is assigned according to the scheduler.
32  */
33 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
34                 uint64_t value, Thread *thread) :
35         type(type),
36         order(order),
37         location(loc),
38         value(value),
39         reads_from(NULL),
40         reads_from_promise(NULL),
41         last_fence_release(NULL),
42         node(NULL),
43         seq_number(ACTION_INITIAL_CLOCK),
44         cv(NULL),
45         sleep_flag(false)
46 {
47         /* References to NULL atomic variables can end up here */
48         ASSERT(loc || type == ATOMIC_FENCE || type == MODEL_FIXUP_RELSEQ);
49
50         Thread *t = thread ? thread : thread_current();
51         this->tid = t->get_id();
52 }
53
54 /** @brief ModelAction destructor */
55 ModelAction::~ModelAction()
56 {
57         /**
58          * We can't free the clock vector:
59          * Clock vectors are snapshotting state. When we delete model actions,
60          * they are at the end of the node list and have invalid old clock
61          * vectors which have already been rolled back to an unallocated state.
62          */
63
64         /*
65          if (cv)
66                 delete cv; */
67 }
68
69 void ModelAction::copy_from_new(ModelAction *newaction)
70 {
71         seq_number = newaction->seq_number;
72 }
73
74 void ModelAction::set_seq_number(modelclock_t num)
75 {
76         /* ATOMIC_UNINIT actions should never have non-zero clock */
77         ASSERT(!is_uninitialized());
78         ASSERT(seq_number == ACTION_INITIAL_CLOCK);
79         seq_number = num;
80 }
81
82 bool ModelAction::is_thread_start() const
83 {
84         return type == THREAD_START;
85 }
86
87 bool ModelAction::is_thread_join() const
88 {
89         return type == THREAD_JOIN;
90 }
91
92 bool ModelAction::is_relseq_fixup() const
93 {
94         return type == MODEL_FIXUP_RELSEQ;
95 }
96
97 bool ModelAction::is_mutex_op() const
98 {
99         return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
100 }
101
102 bool ModelAction::is_lock() const
103 {
104         return type == ATOMIC_LOCK;
105 }
106
107 bool ModelAction::is_wait() const {
108         return type == ATOMIC_WAIT;
109 }
110
111 bool ModelAction::is_notify() const {
112         return type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
113 }
114
115 bool ModelAction::is_notify_one() const {
116         return type == ATOMIC_NOTIFY_ONE;
117 }
118
119 bool ModelAction::is_unlock() const
120 {
121         return type == ATOMIC_UNLOCK;
122 }
123
124 bool ModelAction::is_trylock() const
125 {
126         return type == ATOMIC_TRYLOCK;
127 }
128
129 bool ModelAction::is_success_lock() const
130 {
131         return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
132 }
133
134 bool ModelAction::is_failed_trylock() const
135 {
136         return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
137 }
138
139 /** @return True if this operation is performed on a C/C++ atomic variable */
140 bool ModelAction::is_atomic_var() const
141 {
142         return is_read() || could_be_write();
143 }
144
145 bool ModelAction::is_uninitialized() const
146 {
147         return type == ATOMIC_UNINIT;
148 }
149
150 bool ModelAction::is_read() const
151 {
152         return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
153 }
154
155 bool ModelAction::is_write() const
156 {
157         return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT;
158 }
159
160 bool ModelAction::could_be_write() const
161 {
162         return is_write() || is_rmwr();
163 }
164
165 bool ModelAction::is_yield() const
166 {
167         return type == THREAD_YIELD;
168 }
169
170 bool ModelAction::is_rmwr() const
171 {
172         return type == ATOMIC_RMWR;
173 }
174
175 bool ModelAction::is_rmw() const
176 {
177         return type == ATOMIC_RMW;
178 }
179
180 bool ModelAction::is_rmwc() const
181 {
182         return type == ATOMIC_RMWC;
183 }
184
185 bool ModelAction::is_fence() const
186 {
187         return type == ATOMIC_FENCE;
188 }
189
190 bool ModelAction::is_initialization() const
191 {
192         return type == ATOMIC_INIT;
193 }
194
195 bool ModelAction::is_relaxed() const
196 {
197         return order == std::memory_order_relaxed;
198 }
199
200 bool ModelAction::is_acquire() const
201 {
202         switch (order) {
203         case std::memory_order_acquire:
204         case std::memory_order_acq_rel:
205         case std::memory_order_seq_cst:
206                 return true;
207         default:
208                 return false;
209         }
210 }
211
212 bool ModelAction::is_release() const
213 {
214         switch (order) {
215         case std::memory_order_release:
216         case std::memory_order_acq_rel:
217         case std::memory_order_seq_cst:
218                 return true;
219         default:
220                 return false;
221         }
222 }
223
224 bool ModelAction::is_seqcst() const
225 {
226         return order == std::memory_order_seq_cst;
227 }
228
229 bool ModelAction::same_var(const ModelAction *act) const
230 {
231         if (act->is_wait() || is_wait()) {
232                 if (act->is_wait() && is_wait()) {
233                         if (((void *)value) == ((void *)act->value))
234                                 return true;
235                 } else if (is_wait()) {
236                         if (((void *)value) == act->location)
237                                 return true;
238                 } else if (act->is_wait()) {
239                         if (location == ((void *)act->value))
240                                 return true;
241                 }
242         }
243
244         return location == act->location;
245 }
246
247 bool ModelAction::same_thread(const ModelAction *act) const
248 {
249         return tid == act->tid;
250 }
251
252 void ModelAction::copy_typeandorder(ModelAction * act)
253 {
254         this->type = act->type;
255         this->order = act->order;
256 }
257
258 /**
259  * Get the Thread which is the operand of this action. This is only valid for
260  * THREAD_* operations (currently only for THREAD_CREATE and THREAD_JOIN). Note
261  * that this provides a central place for determining the conventions of Thread
262  * storage in ModelAction, where we generally aren't very type-safe (e.g., we
263  * store object references in a (void *) address.
264  *
265  * For THREAD_CREATE, this yields the Thread which is created.
266  * For THREAD_JOIN, this yields the Thread we are joining with.
267  *
268  * @return The Thread which this action acts on, if exists; otherwise NULL
269  */
270 Thread * ModelAction::get_thread_operand() const
271 {
272         if (type == THREAD_CREATE) {
273                 /* THREAD_CREATE stores its (Thread *) in a thrd_t::priv */
274                 thrd_t *thrd = (thrd_t *)get_location();
275                 return thrd->priv;
276         } else if (type == THREAD_JOIN)
277                 /* THREAD_JOIN uses (Thread *) for location */
278                 return (Thread *)get_location();
279         else
280                 return NULL;
281 }
282
283 /**
284  * @brief Convert the read portion of an RMW
285  *
286  * Changes an existing read part of an RMW action into either:
287  *  -# a full RMW action in case of the completed write or
288  *  -# a READ action in case a failed action.
289  *
290  * @todo  If the memory_order changes, we may potentially need to update our
291  * clock vector.
292  *
293  * @param act The second half of the RMW (either RMWC or RMW)
294  */
295 void ModelAction::process_rmw(ModelAction *act)
296 {
297         this->order = act->order;
298         if (act->is_rmwc())
299                 this->type = ATOMIC_READ;
300         else if (act->is_rmw()) {
301                 this->type = ATOMIC_RMW;
302                 this->value = act->value;
303         }
304 }
305
306 /**
307  * @brief Check if this action should be backtracked with another, due to
308  * potential synchronization
309  *
310  * The is_synchronizing method should only explore interleavings if:
311  *  -# the operations are seq_cst and don't commute or
312  *  -# the reordering may establish or break a synchronization relation.
313  *
314  * Other memory operations will be dealt with by using the reads_from relation.
315  *
316  * @param act The action to consider exploring a reordering
317  * @return True, if we have to explore a reordering; otherwise false
318  */
319 bool ModelAction::could_synchronize_with(const ModelAction *act) const
320 {
321         // Same thread can't be reordered
322         if (same_thread(act))
323                 return false;
324
325         // Different locations commute
326         if (!same_var(act))
327                 return false;
328
329         // Explore interleavings of seqcst writes/fences to guarantee total
330         // order of seq_cst operations that don't commute
331         if ((could_be_write() || act->could_be_write() || is_fence() || act->is_fence()) && is_seqcst() && act->is_seqcst())
332                 return true;
333
334         // Explore synchronizing read/write pairs
335         if (is_acquire() && act->is_release() && is_read() && act->could_be_write())
336                 return true;
337
338         // lock just released...we can grab lock
339         if ((is_lock() || is_trylock()) && (act->is_unlock() || act->is_wait()))
340                 return true;
341
342         // lock just acquired...we can fail to grab lock
343         if (is_trylock() && act->is_success_lock())
344                 return true;
345
346         // other thread stalling on lock...we can release lock
347         if (is_unlock() && (act->is_trylock() || act->is_lock()))
348                 return true;
349
350         if (is_trylock() && (act->is_unlock() || act->is_wait()))
351                 return true;
352
353         if (is_notify() && act->is_wait())
354                 return true;
355
356         if (is_wait() && act->is_notify())
357                 return true;
358
359         // Otherwise handle by reads_from relation
360         return false;
361 }
362
363 bool ModelAction::is_conflicting_lock(const ModelAction *act) const
364 {
365         // Must be different threads to reorder
366         if (same_thread(act))
367                 return false;
368
369         // Try to reorder a lock past a successful lock
370         if (act->is_success_lock())
371                 return true;
372
373         // Try to push a successful trylock past an unlock
374         if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
375                 return true;
376
377         // Try to push a successful trylock past a wait
378         if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS)
379                 return true;
380
381         return false;
382 }
383
384 /**
385  * Create a new clock vector for this action. Note that this function allows a
386  * user to clobber (and leak) a ModelAction's existing clock vector. A user
387  * should ensure that the vector has already either been rolled back
388  * (effectively "freed") or freed.
389  *
390  * @param parent A ModelAction from which to inherit a ClockVector
391  */
392 void ModelAction::create_cv(const ModelAction *parent)
393 {
394         if (parent)
395                 cv = new ClockVector(parent->cv, this);
396         else
397                 cv = new ClockVector(NULL, this);
398 }
399
400 void ModelAction::set_try_lock(bool obtainedlock)
401 {
402         value = obtainedlock ? VALUE_TRYSUCCESS : VALUE_TRYFAILED;
403 }
404
405 /**
406  * @brief Get the value read by this load
407  *
408  * We differentiate this function from ModelAction::get_write_value and
409  * ModelAction::get_value for the purpose of RMW's, which may have both a
410  * 'read' and a 'write' value.
411  *
412  * Note: 'this' must be a load.
413  *
414  * @return The value read by this load
415  */
416 uint64_t ModelAction::get_reads_from_value() const
417 {
418         ASSERT(is_read());
419         if (reads_from)
420                 return reads_from->get_write_value();
421         else if (reads_from_promise)
422                 return reads_from_promise->get_value();
423         return VALUE_NONE; /* Only for new actions with no reads-from */
424 }
425
426 /**
427  * @brief Get the value written by this store
428  *
429  * We differentiate this function from ModelAction::get_reads_from_value and
430  * ModelAction::get_value for the purpose of RMW's, which may have both a
431  * 'read' and a 'write' value.
432  *
433  * Note: 'this' must be a store.
434  *
435  * @return The value written by this store
436  */
437 uint64_t ModelAction::get_write_value() const
438 {
439         ASSERT(is_write());
440         return value;
441 }
442
443 /**
444  * @brief Get the value returned by this action
445  *
446  * For atomic reads (including RMW), an operation returns the value it read.
447  * For atomic writes, an operation returns the value it wrote. For other
448  * operations, the return value varies (sometimes is a "don't care"), but the
449  * value is simply stored in the "value" field.
450  *
451  * @return This action's return value
452  */
453 uint64_t ModelAction::get_return_value() const
454 {
455         if (is_read())
456                 return get_reads_from_value();
457         else if (is_write())
458                 return get_write_value();
459         else
460                 return value;
461 }
462
463 /** @return The Node associated with this ModelAction */
464 Node * ModelAction::get_node() const
465 {
466         /* UNINIT actions do not have a Node */
467         ASSERT(!is_uninitialized());
468         return node;
469 }
470
471 /**
472  * Update the model action's read_from action
473  * @param act The action to read from; should be a write
474  */
475 void ModelAction::set_read_from(const ModelAction *act)
476 {
477         ASSERT(act);
478         reads_from = act;
479         reads_from_promise = NULL;
480         if (act->is_uninitialized())
481                 model->assert_bug("May read from uninitialized atomic\n");
482 }
483
484 /**
485  * Set this action's read-from promise
486  * @param promise The promise to read from
487  */
488 void ModelAction::set_read_from_promise(Promise *promise)
489 {
490         ASSERT(is_read());
491         reads_from_promise = promise;
492         reads_from = NULL;
493 }
494
495 /**
496  * Synchronize the current thread with the thread corresponding to the
497  * ModelAction parameter.
498  * @param act The ModelAction to synchronize with
499  * @return True if this is a valid synchronization; false otherwise
500  */
501 bool ModelAction::synchronize_with(const ModelAction *act)
502 {
503         if (*this < *act)
504                 return false;
505         cv->merge(act->cv);
506         return true;
507 }
508
509 bool ModelAction::has_synchronized_with(const ModelAction *act) const
510 {
511         return cv->synchronized_since(act);
512 }
513
514 /**
515  * Check whether 'this' happens before act, according to the memory-model's
516  * happens before relation. This is checked via the ClockVector constructs.
517  * @return true if this action's thread has synchronized with act's thread
518  * since the execution of act, false otherwise.
519  */
520 bool ModelAction::happens_before(const ModelAction *act) const
521 {
522         return act->cv->synchronized_since(this);
523 }
524
525 /** @brief Print nicely-formatted info about this ModelAction */
526 void ModelAction::print() const
527 {
528         const char *type_str, *mo_str;
529         switch (this->type) {
530         case MODEL_FIXUP_RELSEQ:
531                 type_str = "relseq fixup";
532                 break;
533         case THREAD_CREATE:
534                 type_str = "thread create";
535                 break;
536         case THREAD_START:
537                 type_str = "thread start";
538                 break;
539         case THREAD_YIELD:
540                 type_str = "thread yield";
541                 break;
542         case THREAD_JOIN:
543                 type_str = "thread join";
544                 break;
545         case THREAD_FINISH:
546                 type_str = "thread finish";
547                 break;
548         case ATOMIC_UNINIT:
549                 type_str = "uninitialized";
550                 break;
551         case ATOMIC_READ:
552                 type_str = "atomic read";
553                 break;
554         case ATOMIC_WRITE:
555                 type_str = "atomic write";
556                 break;
557         case ATOMIC_RMW:
558                 type_str = "atomic rmw";
559                 break;
560         case ATOMIC_FENCE:
561                 type_str = "fence";
562                 break;
563         case ATOMIC_RMWR:
564                 type_str = "atomic rmwr";
565                 break;
566         case ATOMIC_RMWC:
567                 type_str = "atomic rmwc";
568                 break;
569         case ATOMIC_INIT:
570                 type_str = "init atomic";
571                 break;
572         case ATOMIC_LOCK:
573                 type_str = "lock";
574                 break;
575         case ATOMIC_UNLOCK:
576                 type_str = "unlock";
577                 break;
578         case ATOMIC_TRYLOCK:
579                 type_str = "trylock";
580                 break;
581         case ATOMIC_WAIT:
582                 type_str = "wait";
583                 break;
584         case ATOMIC_NOTIFY_ONE:
585                 type_str = "notify one";
586                 break;
587         case ATOMIC_NOTIFY_ALL:
588                 type_str = "notify all";
589                 break;
590         default:
591                 type_str = "unknown type";
592         }
593
594         switch (this->order) {
595         case std::memory_order_relaxed:
596                 mo_str = "relaxed";
597                 break;
598         case std::memory_order_acquire:
599                 mo_str = "acquire";
600                 break;
601         case std::memory_order_release:
602                 mo_str = "release";
603                 break;
604         case std::memory_order_acq_rel:
605                 mo_str = "acq_rel";
606                 break;
607         case std::memory_order_seq_cst:
608                 mo_str = "seq_cst";
609                 break;
610         default:
611                 mo_str = "unknown";
612                 break;
613         }
614
615         model_print("(%4d) Thread: %-2d   Action: %-13s   MO: %7s  Loc: %14p   Value: %-#18" PRIx64,
616                         seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());
617         if (is_read()) {
618                 if (reads_from)
619                         model_print("  Rf: %-3d", reads_from->get_seq_number());
620                 else if (reads_from_promise) {
621                         int idx = reads_from_promise->get_index();
622                         if (idx >= 0)
623                                 model_print("  Rf: P%-2d", idx);
624                         else
625                                 model_print("  Rf: P? ");
626                 } else
627                         model_print("  Rf: ?  ");
628         }
629         if (cv) {
630                 if (is_read())
631                         model_print(" ");
632                 else
633                         model_print("          ");
634                 cv->print();
635         } else
636                 model_print("\n");
637 }
638
639 /** @brief Get a (likely) unique hash for this ModelAction */
640 unsigned int ModelAction::hash() const
641 {
642         unsigned int hash = (unsigned int)this->type;
643         hash ^= ((unsigned int)this->order) << 3;
644         hash ^= seq_number << 5;
645         hash ^= id_to_int(tid) << 6;
646
647         if (is_read()) {
648                if (reads_from)
649                        hash ^= reads_from->get_seq_number();
650                else if (reads_from_promise)
651                        hash ^= reads_from_promise->get_index();
652                hash ^= get_reads_from_value();
653         }
654         return hash;
655 }
656
657 /**
658  * @brief Checks the NodeStack to see if a ModelAction is in our may-read-from set
659  * @param write The ModelAction to check for
660  * @return True if the ModelAction is found; false otherwise
661  */
662 bool ModelAction::may_read_from(const ModelAction *write) const
663 {
664         for (int i = 0; i < node->get_read_from_past_size(); i++)
665                 if (node->get_read_from_past(i) == write)
666                         return true;
667         return false;
668 }
669
670 /**
671  * @brief Checks the NodeStack to see if a Promise is in our may-read-from set
672  * @param promise The Promise to check for
673  * @return True if the Promise is found; false otherwise
674  */
675 bool ModelAction::may_read_from(const Promise *promise) const
676 {
677         for (int i = 0; i < node->get_read_from_promise_size(); i++)
678                 if (node->get_read_from_promise(i) == promise)
679                         return true;
680         return false;
681 }
682
683 /**
684  * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations.
685  * @return The mutex operated on by this action, if any; otherwise NULL
686  */
687 std::mutex * ModelAction::get_mutex() const
688 {
689         if (is_trylock() || is_lock() || is_unlock())
690                 return (std::mutex *)get_location();
691         else if (is_wait())
692                 return (std::mutex *)get_value();
693         else
694                 return NULL;
695 }