When re-ordering the execution of JOIN and LOCK operations (e.g., when
they attempt to execute when not enabled), the sequence numbers became
out of order. Also, RMW operations would cause sequence numbers to jump
by 2 every time.
This fix arranges initialization such that a ModelAction is only
assigned a sequence number after it passes some initial checks to ensure
that it will be executed and utilized immediately. Otherwise, it will
either be discarded or held pending until it is enabled.
#include "clockvector.h"
#include "common.h"
#include "clockvector.h"
#include "common.h"
+#define ACTION_INITIAL_CLOCK 0
+
ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) :
type(type),
order(order),
location(loc),
value(value),
reads_from(NULL),
ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) :
type(type),
order(order),
location(loc),
value(value),
reads_from(NULL),
+ seq_number(ACTION_INITIAL_CLOCK),
cv(NULL)
{
Thread *t = thread_current();
this->tid = t->get_id();
cv(NULL)
{
Thread *t = thread_current();
this->tid = t->get_id();
- this->seq_number = model->get_next_seq_num();
}
ModelAction::~ModelAction()
}
ModelAction::~ModelAction()
seq_number = newaction->seq_number;
}
seq_number = newaction->seq_number;
}
+void ModelAction::set_seq_number(modelclock_t num)
+{
+ ASSERT(seq_number == ACTION_INITIAL_CLOCK);
+ seq_number = num;
+}
+
bool ModelAction::is_mutex_op() const
{
return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
bool ModelAction::is_mutex_op() const
{
return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
void set_node(Node *n) { node = n; }
void copy_from_new(ModelAction *newaction);
void set_node(Node *n) { node = n; }
void copy_from_new(ModelAction *newaction);
+ void set_seq_number(modelclock_t num);
void set_try_lock(bool obtainedlock);
bool is_mutex_op() const;
bool is_lock() const;
void set_try_lock(bool obtainedlock);
bool is_mutex_op() const;
bool is_lock() const;
+ curr->set_seq_number(get_next_seq_num());
+
newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */
thread_id_t get_next_id();
int get_num_threads();
thread_id_t get_next_id();
int get_num_threads();
- modelclock_t get_next_seq_num();
/** @return The currently executing Thread. */
Thread * get_current_thread() { return scheduler->get_current_thread(); }
/** @return The currently executing Thread. */
Thread * get_current_thread() { return scheduler->get_current_thread(); }
int num_feasible_executions;
bool promises_expired();
int num_feasible_executions;
bool promises_expired();
+ modelclock_t get_next_seq_num();
+
/**
* Stores the ModelAction for the current thread action. Call this
* immediately before switching from user- to system-context to pass
/**
* Stores the ModelAction for the current thread action. Call this
* immediately before switching from user- to system-context to pass