cv(NULL),
rf_cv(NULL),
value(value),
- reads_from_value(VALUE_NONE),
type(type),
order(order),
original_order(order),
cv(NULL),
rf_cv(NULL),
value(value),
- reads_from_value(VALUE_NONE),
type(type),
order(order),
original_order(order),
cv(NULL),
rf_cv(NULL),
value(value),
- reads_from_value(VALUE_NONE),
type(type),
order(order),
original_order(order),
cv(NULL),
rf_cv(NULL),
value(value),
- reads_from_value(VALUE_NONE),
type(type),
order(order),
original_order(order),
cv(NULL),
rf_cv(NULL),
value(value),
- reads_from_value(VALUE_NONE),
type(type),
order(order),
original_order(order),
seq_number = num;
}
+void ModelAction::reset_seq_number()
+{
+ seq_number = 0;
+}
+
bool ModelAction::is_thread_start() const
{
return type == THREAD_START;
bool ModelAction::is_mutex_op() const
{
- return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
+ return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_TIMEDWAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
}
bool ModelAction::is_lock() const
}
bool ModelAction::is_wait() const {
- return type == ATOMIC_WAIT;
+ return type == ATOMIC_WAIT || type == ATOMIC_TIMEDWAIT;
}
bool ModelAction::is_notify() const {
uint64_t ModelAction::get_reads_from_value() const
{
ASSERT(is_read());
- if (reads_from) {
- if (reads_from->is_uninitialized())
- return reads_from_value;
- else
- return reads_from->get_write_value();
- }
+ if (reads_from)
+ return reads_from->get_write_value();
return VALUE_NONE; // Only for new actions with no reads-from
}
ModelAction * act_uninitialized = (ModelAction *)act;
act_uninitialized->set_value(val);
reads_from = act_uninitialized;
- reads_from_value = val;
// disabled by WL, because LLVM IR is unable to detect atomic init
/* model->assert_bug("May read from uninitialized atomic:\n"
case ATOMIC_UNLOCK: return "unlock";
case ATOMIC_TRYLOCK: return "trylock";
case ATOMIC_WAIT: return "wait";
+ case ATOMIC_TIMEDWAIT: return "timed wait";
case ATOMIC_NOTIFY_ONE: return "notify one";
case ATOMIC_NOTIFY_ALL: return "notify all";
case ATOMIC_ANNOTATION: return "annotation";