/
execution.cc
2874 lines (2595 loc) · 85.8 KB
/
execution.cc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
#include <stdio.h>
#include <algorithm>
#include <mutex>
#include <new>
#include <stdarg.h>
#include "model.h"
#include "execution.h"
#include "action.h"
#include "nodestack.h"
#include "schedule.h"
#include "common.h"
#include "clockvector.h"
#include "cyclegraph.h"
#include "promise.h"
#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
#define INITIAL_THREAD_ID 0
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
struct model_snapshot_members {
model_snapshot_members() :
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
next_backtrack(NULL),
bugs(),
failed_promise(false),
too_many_reads(false),
no_valid_reads(false),
bad_synchronization(false),
asserted(false)
{ }
~model_snapshot_members() {
for (unsigned int i = 0; i < bugs.size(); i++)
delete bugs[i];
bugs.clear();
}
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
SnapVector<bug_message *> bugs;
bool failed_promise;
bool too_many_reads;
bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
bool asserted;
SNAPSHOTALLOC
};
/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m,
const struct model_params *params,
Scheduler *scheduler,
NodeStack *node_stack) :
model(m),
params(params),
scheduler(scheduler),
action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
promises(),
futurevalues(),
pending_rel_seqs(),
thrd_last_action(1),
thrd_last_fence_release(),
node_stack(node_stack),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
add_thread(model_thread);
scheduler->register_engine(this);
node_stack->register_engine(this);
}
/** @brief Destructor */
ModelExecution::~ModelExecution()
{
for (unsigned int i = 0; i < get_num_threads(); i++)
delete get_thread(int_to_id(i));
for (unsigned int i = 0; i < promises.size(); i++)
delete promises[i];
delete mo_graph;
delete priv;
}
int ModelExecution::get_execution_number() const
{
return model->get_execution_number();
}
static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
{
action_list_t *tmp = hash->get(ptr);
if (tmp == NULL) {
tmp = new action_list_t();
hash->put(ptr, tmp);
}
return tmp;
}
static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
{
SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
tmp = new SnapVector<action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
}
action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
{
SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
if (wrv==NULL)
return NULL;
unsigned int thread=id_to_int(tid);
if (thread < wrv->size())
return &(*wrv)[thread];
else
return NULL;
}
/** @return a thread ID for a new Thread */
thread_id_t ModelExecution::get_next_id()
{
return priv->next_thread_id++;
}
/** @return the number of user threads created during this execution */
unsigned int ModelExecution::get_num_threads() const
{
return priv->next_thread_id;
}
/** @return a sequence number for a new ModelAction */
modelclock_t ModelExecution::get_next_seq_num()
{
return ++priv->used_sequence_numbers;
}
/**
* @brief Should the current action wake up a given thread?
*
* @param curr The current action
* @param thread The thread that we might wake up
* @return True, if we should wake up the sleeping thread; false otherwise
*/
bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
{
const ModelAction *asleep = thread->get_pending();
/* Don't allow partial RMW to wake anyone up */
if (curr->is_rmwr())
return false;
/* Synchronizing actions may have been backtracked */
if (asleep->could_synchronize_with(curr))
return true;
/* All acquire/release fences and fence-acquire/store-release */
if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
return true;
/* Fence-release + store can awake load-acquire on the same location */
if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
ModelAction *fence_release = get_last_fence_release(curr->get_tid());
if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
return true;
}
return false;
}
void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
{
for (unsigned int i = 0; i < get_num_threads(); i++) {
Thread *thr = get_thread(int_to_id(i));
if (scheduler->is_sleep_set(thr)) {
if (should_wake_up(curr, thr))
/* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
}
}
}
/** @brief Alert the model-checker that an incorrectly-ordered
* synchronization was made */
void ModelExecution::set_bad_synchronization()
{
priv->bad_synchronization = true;
}
bool ModelExecution::assert_bug(const char *msg)
{
priv->bugs.push_back(new bug_message(msg));
if (isfeasibleprefix()) {
set_assert();
return true;
}
return false;
}
/** @return True, if any bugs have been reported for this execution */
bool ModelExecution::have_bug_reports() const
{
return priv->bugs.size() != 0;
}
SnapVector<bug_message *> * ModelExecution::get_bugs() const
{
return &priv->bugs;
}
/**
* Check whether the current trace has triggered an assertion which should halt
* its execution.
*
* @return True, if the execution should be aborted; false otherwise
*/
bool ModelExecution::has_asserted() const
{
return priv->asserted;
}
/**
* Trigger a trace assertion which should cause this execution to be halted.
* This can be due to a detected bug or due to an infeasibility that should
* halt ASAP.
*/
void ModelExecution::set_assert()
{
priv->asserted = true;
}
/**
* Check if we are in a deadlock. Should only be called at the end of an
* execution, although it should not give false positives in the middle of an
* execution (there should be some ENABLED thread).
*
* @return True if program is in a deadlock; false otherwise
*/
bool ModelExecution::is_deadlocked() const
{
bool blocking_threads = false;
for (unsigned int i = 0; i < get_num_threads(); i++) {
thread_id_t tid = int_to_id(i);
if (is_enabled(tid))
return false;
Thread *t = get_thread(tid);
if (!t->is_model_thread() && t->get_pending())
blocking_threads = true;
}
return blocking_threads;
}
/**
* @brief Check if we are yield-blocked
*
* A program can be "yield-blocked" if all threads are ready to execute a
* yield.
*
* @return True if the program is yield-blocked; false otherwise
*/
bool ModelExecution::is_yieldblocked() const
{
if (!params->yieldblock)
return false;
for (unsigned int i = 0; i < get_num_threads(); i++) {
thread_id_t tid = int_to_id(i);
Thread *t = get_thread(tid);
if (t->get_pending() && t->get_pending()->is_yield())
return true;
}
return false;
}
/**
* Check if this is a complete execution. That is, have all thread completed
* execution (rather than exiting because sleep sets have forced a redundant
* execution).
*
* @return True if the execution is complete.
*/
bool ModelExecution::is_complete_execution() const
{
if (is_yieldblocked())
return false;
for (unsigned int i = 0; i < get_num_threads(); i++)
if (is_enabled(int_to_id(i)))
return false;
return true;
}
/**
* @brief Find the last fence-related backtracking conflict for a ModelAction
*
* This function performs the search for the most recent conflicting action
* against which we should perform backtracking, as affected by fence
* operations. This includes pairs of potentially-synchronizing actions which
* occur due to fence-acquire or fence-release, and hence should be explored in
* the opposite execution order.
*
* @param act The current action
* @return The most recent action which conflicts with act due to fences
*/
ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
{
/* Only perform release/acquire fence backtracking for stores */
if (!act->is_write())
return NULL;
/* Find a fence-release (or, act is a release) */
ModelAction *last_release;
if (act->is_release())
last_release = act;
else
last_release = get_last_fence_release(act->get_tid());
if (!last_release)
return NULL;
/* Skip past the release */
const action_list_t *list = &action_trace;
action_list_t::const_reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++)
if (*rit == last_release)
break;
ASSERT(rit != list->rend());
/* Find a prior:
* load-acquire
* or
* load --sb-> fence-acquire */
ModelVector<ModelAction *> acquire_fences(get_num_threads(), NULL);
ModelVector<ModelAction *> prior_loads(get_num_threads(), NULL);
bool found_acquire_fences = false;
for ( ; rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (act->same_thread(prev))
continue;
int tid = id_to_int(prev->get_tid());
if (prev->is_read() && act->same_var(prev)) {
if (prev->is_acquire()) {
/* Found most recent load-acquire, don't need
* to search for more fences */
if (!found_acquire_fences)
return NULL;
} else {
prior_loads[tid] = prev;
}
}
if (prev->is_acquire() && prev->is_fence() && !acquire_fences[tid]) {
found_acquire_fences = true;
acquire_fences[tid] = prev;
}
}
ModelAction *latest_backtrack = NULL;
for (unsigned int i = 0; i < acquire_fences.size(); i++)
if (acquire_fences[i] && prior_loads[i])
if (!latest_backtrack || *latest_backtrack < *acquire_fences[i])
latest_backtrack = acquire_fences[i];
return latest_backtrack;
}
/**
* @brief Find the last backtracking conflict for a ModelAction
*
* This function performs the search for the most recent conflicting action
* against which we should perform backtracking. This primary includes pairs of
* synchronizing actions which should be explored in the opposite execution
* order.
*
* @param act The current action
* @return The most recent action which conflicts with act
*/
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
case ATOMIC_FENCE:
/* Only seq-cst fences can (directly) cause backtracking */
if (!act->is_seqcst())
break;
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
ModelAction *ret = NULL;
/* linear search: from most recent to oldest */
action_list_t *list = obj_map.get(act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (prev == act)
continue;
if (prev->could_synchronize_with(act)) {
ret = prev;
break;
}
}
ModelAction *ret2 = get_last_fence_conflict(act);
if (!ret2)
return ret;
if (!ret)
return ret2;
if (*ret < *ret2)
return ret2;
return ret;
}
case ATOMIC_LOCK:
case ATOMIC_TRYLOCK: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map.get(act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (act->is_conflicting_lock(prev))
return prev;
}
break;
}
case ATOMIC_UNLOCK: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map.get(act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (!act->same_thread(prev) && prev->is_failed_trylock())
return prev;
}
break;
}
case ATOMIC_WAIT: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map.get(act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (!act->same_thread(prev) && prev->is_failed_trylock())
return prev;
if (!act->same_thread(prev) && prev->is_notify())
return prev;
}
break;
}
case ATOMIC_NOTIFY_ALL:
case ATOMIC_NOTIFY_ONE: {
/* linear search: from most recent to oldest */
action_list_t *list = obj_map.get(act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (!act->same_thread(prev) && prev->is_wait())
return prev;
}
break;
}
default:
break;
}
return NULL;
}
/** This method finds backtracking points where we should try to
* reorder the parameter ModelAction against.
*
* @param the ModelAction to find backtracking points for.
*/
void ModelExecution::set_backtracking(ModelAction *act)
{
Thread *t = get_thread(act);
ModelAction *prev = get_last_conflict(act);
if (prev == NULL)
return;
Node *node = prev->get_node()->get_parent();
/* See Dynamic Partial Order Reduction (addendum), POPL '05 */
int low_tid, high_tid;
if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
low_tid = id_to_int(act->get_tid());
high_tid = low_tid + 1;
} else {
low_tid = 0;
high_tid = get_num_threads();
}
for (int i = low_tid; i < high_tid; i++) {
thread_id_t tid = int_to_id(i);
/* Make sure this thread can be enabled here. */
if (i >= node->get_num_threads())
break;
/* See Dynamic Partial Order Reduction (addendum), POPL '05 */
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid) != THREAD_ENABLED)
continue;
/* Check if this has been explored already */
if (node->has_been_explored(tid))
continue;
/* See if fairness allows */
if (params->fairwindow != 0 && !node->has_priority(tid)) {
bool unfair = false;
for (int t = 0; t < node->get_num_threads(); t++) {
thread_id_t tother = int_to_id(t);
if (node->is_enabled(tother) && node->has_priority(tother)) {
unfair = true;
break;
}
}
if (unfair)
continue;
}
/* See if CHESS-like yield fairness allows */
if (params->yieldon) {
bool unfair = false;
for (int t = 0; t < node->get_num_threads(); t++) {
thread_id_t tother = int_to_id(t);
if (node->is_enabled(tother) && node->has_priority_over(tid, tother)) {
unfair = true;
break;
}
}
if (unfair)
continue;
}
/* Cache the latest backtracking point */
set_latest_backtrack(prev);
/* If this is a new backtracking point, mark the tree */
if (!node->set_backtrack(tid))
continue;
DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
id_to_int(prev->get_tid()),
id_to_int(t->get_id()));
if (DBG_ENABLED()) {
prev->print();
act->print();
}
}
}
/**
* @brief Cache the a backtracking point as the "most recent", if eligible
*
* Note that this does not prepare the NodeStack for this backtracking
* operation, it only caches the action on a per-execution basis
*
* @param act The operation at which we should explore a different next action
* (i.e., backtracking point)
* @return True, if this action is now the most recent backtracking point;
* false otherwise
*/
bool ModelExecution::set_latest_backtrack(ModelAction *act)
{
if (!priv->next_backtrack || *act > *priv->next_backtrack) {
priv->next_backtrack = act;
return true;
}
return false;
}
/**
* Returns last backtracking point. The model checker will explore a different
* path for this point in the next execution.
* @return The ModelAction at which the next execution should diverge.
*/
ModelAction * ModelExecution::get_next_backtrack()
{
ModelAction *next = priv->next_backtrack;
priv->next_backtrack = NULL;
return next;
}
/**
* Processes a read model action.
* @param curr is the read model action to process.
* @return True if processing this read updates the mo_graph.
*/
bool ModelExecution::process_read(ModelAction *curr)
{
Node *node = curr->get_node();
while (true) {
bool updated = false;
switch (node->get_read_from_status()) {
case READ_FROM_PAST: {
const ModelAction *rf = node->get_read_from_past();
ASSERT(rf);
mo_graph->startChanges();
ASSERT(!is_infeasible());
if (!check_recency(curr, rf)) {
if (node->increment_read_from()) {
mo_graph->rollbackChanges();
continue;
} else {
priv->too_many_reads = true;
}
}
updated = r_modification_order(curr, rf);
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
break;
}
case READ_FROM_PROMISE: {
Promise *promise = curr->get_node()->get_read_from_promise();
if (promise->add_reader(curr))
priv->failed_promise = true;
curr->set_read_from_promise(promise);
mo_graph->startChanges();
if (!check_recency(curr, promise))
priv->too_many_reads = true;
updated = r_modification_order(curr, promise);
mo_graph->commitChanges();
break;
}
case READ_FROM_FUTURE: {
/* Read from future value */
struct future_value fv = node->get_future_value();
Promise *promise = new Promise(this, curr, fv);
curr->set_read_from_promise(promise);
promises.push_back(promise);
mo_graph->startChanges();
updated = r_modification_order(curr, promise);
mo_graph->commitChanges();
break;
}
default:
ASSERT(false);
}
get_thread(curr)->set_return_value(curr->get_return_value());
return updated;
}
}
/**
* Processes a lock, trylock, or unlock model action. @param curr is
* the read model action to process.
*
* The try lock operation checks whether the lock is taken. If not,
* it falls to the normal lock operation case. If so, it returns
* fail.
*
* The lock operation has already been checked that it is enabled, so
* it just grabs the lock and synchronizes with the previous unlock.
*
* The unlock operation has to re-enable all of the threads that are
* waiting on the lock.
*
* @return True if synchronization was updated; false otherwise
*/
bool ModelExecution::process_mutex(ModelAction *curr)
{
std::mutex *mutex = curr->get_mutex();
struct std::mutex_state *state = NULL;
if (mutex)
state = mutex->get_state();
switch (curr->get_type()) {
case ATOMIC_TRYLOCK: {
bool success = !state->locked;
curr->set_try_lock(success);
if (!success) {
get_thread(curr)->set_return_value(0);
break;
}
get_thread(curr)->set_return_value(1);
}
//otherwise fall into the lock case
case ATOMIC_LOCK: {
if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
assert_bug("Lock access before initialization");
state->locked = get_thread(curr);
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
if (unlock != NULL) {
synchronize(unlock, curr);
return true;
}
break;
}
case ATOMIC_WAIT:
case ATOMIC_UNLOCK: {
/* wake up the other threads */
for (unsigned int i = 0; i < get_num_threads(); i++) {
Thread *t = get_thread(int_to_id(i));
Thread *curr_thrd = get_thread(curr);
if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
scheduler->wake(t);
}
/* unlock the lock - after checking who was waiting on it */
state->locked = NULL;
if (!curr->is_wait())
break; /* The rest is only for ATOMIC_WAIT */
/* Should we go to sleep? (simulate spurious failures) */
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
/* disable us */
scheduler->sleep(get_thread(curr));
}
break;
}
case ATOMIC_NOTIFY_ALL: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
scheduler->wake(get_thread(*rit));
}
waiters->clear();
break;
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
int wakeupthread = curr->get_node()->get_misc();
action_list_t::iterator it = waiters->begin();
advance(it, wakeupthread);
scheduler->wake(get_thread(*it));
waiters->erase(it);
break;
}
default:
ASSERT(0);
}
return false;
}
/**
* @brief Check if the current pending promises allow a future value to be sent
*
* It is unsafe to pass a future value back if there exists a pending promise Pr
* such that:
*
* reader --exec-> Pr --exec-> writer
*
* If such Pr exists, we must save the pending future value until Pr is
* resolved.
*
* @param writer The operation which sends the future value. Must be a write.
* @param reader The operation which will observe the value. Must be a read.
* @return True if the future value can be sent now; false if it must wait.
*/
bool ModelExecution::promises_may_allow(const ModelAction *writer,
const ModelAction *reader) const
{
for (int i = promises.size() - 1; i >= 0; i--) {
ModelAction *pr = promises[i]->get_reader(0);
//reader is after promise...doesn't cross any promise
if (*reader > *pr)
return true;
//writer is after promise, reader before...bad...
if (*writer > *pr)
return false;
}
return true;
}
/**
* @brief Add a future value to a reader
*
* This function performs a few additional checks to ensure that the future
* value can be feasibly observed by the reader
*
* @param writer The operation whose value is sent. Must be a write.
* @param reader The read operation which may read the future value. Must be a read.
*/
void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *reader)
{
/* Do more ambitious checks now that mo is more complete */
if (!mo_may_allow(writer, reader))
return;
Node *node = reader->get_node();
/* Find an ancestor thread which exists at the time of the reader */
Thread *write_thread = get_thread(writer);
while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
write_thread = write_thread->get_parent();
struct future_value fv = {
writer->get_write_value(),
writer->get_seq_number() + params->maxfuturedelay,
write_thread->get_id(),
};
if (node->add_future_value(fv))
set_latest_backtrack(reader);
}
/**
* Process a write ModelAction
* @param curr The ModelAction to process
* @param work The work queue, for adding fixup work
* @return True if the mo_graph was updated or promises were resolved
*/
bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work)
{
/* Readers to which we may send our future value */
ModelVector<ModelAction *> send_fv;
const ModelAction *earliest_promise_reader;
bool updated_promises = false;
bool updated_mod_order = w_modification_order(curr, &send_fv);
Promise *promise = pop_promise_to_resolve(curr);
if (promise) {
earliest_promise_reader = promise->get_reader(0);
updated_promises = resolve_promise(curr, promise, work);
} else
earliest_promise_reader = NULL;
for (unsigned int i = 0; i < send_fv.size(); i++) {
ModelAction *read = send_fv[i];
/* Don't send future values to reads after the Promise we resolve */
if (!earliest_promise_reader || *read < *earliest_promise_reader) {
/* Check if future value can be sent immediately */
if (promises_may_allow(curr, read)) {
add_future_value(curr, read);
} else {
futurevalues.push_back(PendingFutureValue(curr, read));
}
}
}
/* Check the pending future values */
for (int i = (int)futurevalues.size() - 1; i >= 0; i--) {
struct PendingFutureValue pfv = futurevalues[i];
if (promises_may_allow(pfv.writer, pfv.reader)) {
add_future_value(pfv.writer, pfv.reader);
futurevalues.erase(futurevalues.begin() + i);
}
}
mo_graph->commitChanges();
mo_check_promises(curr, false);
get_thread(curr)->set_return_value(VALUE_NONE);
return updated_mod_order || updated_promises;
}
/**
* Process a fence ModelAction
* @param curr The ModelAction to process
* @return True if synchronization was updated
*/
bool ModelExecution::process_fence(ModelAction *curr)
{
/*
* fence-relaxed: no-op
* fence-release: only log the occurence (not in this function), for
* use in later synchronization
* fence-acquire (this function): search for hypothetical release
* sequences
* fence-seq-cst: MO constraints formed in {r,w}_modification_order
*/
bool updated = false;
if (curr->is_acquire()) {
action_list_t *list = &action_trace;
action_list_t::reverse_iterator rit;
/* Find X : is_read(X) && X --sb-> curr */
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
if (act == curr)
continue;
if (act->get_tid() != curr->get_tid())
continue;
/* Stop at the beginning of the thread */
if (act->is_thread_start())
break;
/* Stop once we reach a prior fence-acquire */
if (act->is_fence() && act->is_acquire())
break;
if (!act->is_read())
continue;
/* read-acquire will find its own release sequences */
if (act->is_acquire())
continue;
/* Establish hypothetical release sequences */
rel_heads_list_t release_heads;
get_release_seq_heads(curr, act, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++)
synchronize(release_heads[i], curr);
if (release_heads.size() != 0)
updated = true;
}
}
return updated;
}
/**
* @brief Process the current action for thread-related activity
*
* Performs current-action processing for a THREAD_* ModelAction. Proccesses
* may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
* synchronization, etc. This function is a no-op for non-THREAD actions
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
* @return True if synchronization was updated or a thread completed
*/
bool ModelExecution::process_thread_action(ModelAction *curr)
{
bool updated = false;
switch (curr->get_type()) {
case THREAD_CREATE: {
thrd_t *thrd = (thrd_t *)curr->get_location();
struct thread_params *params = (struct thread_params *)curr->get_value();
Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
add_thread(th);
th->set_creation(curr);
/* Promises can be satisfied by children */
for (unsigned int i = 0; i < promises.size(); i++) {
Promise *promise = promises[i];
if (promise->thread_is_available(curr->get_tid()))
promise->add_thread(th->get_id());
}
break;
}
case THREAD_JOIN: {
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_FINISH: {
Thread *th = get_thread(curr);
/* Wake up any joining threads */
for (unsigned int i = 0; i < get_num_threads(); i++) {
Thread *waiting = get_thread(int_to_id(i));
if (waiting->waiting_on() == th &&
waiting->get_pending()->is_thread_join())
scheduler->wake(waiting);
}
th->complete();
/* Completed thread can't satisfy promises */
for (unsigned int i = 0; i < promises.size(); i++) {
Promise *promise = promises[i];
if (promise->thread_is_available(th->get_id()))
if (promise->eliminate_thread(th->get_id()))
priv->failed_promise = true;
}
updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
check_promises(curr->get_tid(), NULL, curr->get_cv());
break;
}
default:
break;
}
return updated;
}
/**
* @brief Process the current action for release sequence fixup activity
*
* Performs model-checker release sequence fixups for the current action,
* forcing a single pending release sequence to break (with a given, potential
* "loose" write) or to complete (i.e., synchronize). If a pending release
* sequence forms a complete release sequence, then we must perform the fixup
* synchronization, mo_graph additions, etc.
*
* @param curr The current action; must be a release sequence fixup action
* @param work_queue The work queue to which to add work items as they are
* generated
*/
void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)