#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),
+ seq_number(ACTION_INITIAL_CLOCK),
cv(NULL)
{
Thread *t = thread_current();
this->tid = t->get_id();
- this->seq_number = model->get_next_seq_num();
}
ModelAction::~ModelAction()
delete cv;
}
-void ModelAction::copy_from_new(ModelAction *newaction) {
- seq_number=newaction->seq_number;
+void ModelAction::copy_from_new(ModelAction *newaction)
+{
+ 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 {
+bool ModelAction::is_mutex_op() const
+{
return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
}
-bool ModelAction::is_lock() const {
+bool ModelAction::is_lock() const
+{
return type == ATOMIC_LOCK;
}
-bool ModelAction::is_unlock() const {
+bool ModelAction::is_unlock() const
+{
return type == ATOMIC_UNLOCK;
}
-bool ModelAction::is_trylock() const {
+bool ModelAction::is_trylock() const
+{
return type == ATOMIC_TRYLOCK;
}
-bool ModelAction::is_success_lock() const {
+bool ModelAction::is_success_lock() const
+{
return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
}
-bool ModelAction::is_failed_trylock() const {
+bool ModelAction::is_failed_trylock() const
+{
return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
}
}
void ModelAction::copy_typeandorder(ModelAction * act) {
- this->type=act->type;
- this->order=act->order;
+ this->type = act->type;
+ this->order = act->order;
}
/** This method changes an existing read part of an RMW action into either:
return act->cv->synchronized_since(this);
}
-void ModelAction::print(void) const
+/**
+ * Print nicely-formatted info about this ModelAction
+ *
+ * @param print_cv True if we want to print clock vector data. Might be false,
+ * for instance, in situations where the clock vector might be invalid
+ */
+void ModelAction::print(bool print_cv) const
{
const char *type_str, *mo_str;
switch (this->type) {
else
printf(" Rf: ?");
}
- if (cv) {
+ if (cv && print_cv) {
printf("\t");
cv->print();
} else
public:
ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
~ModelAction();
- void print(void) const;
+ void print(bool print_cv = true) const;
thread_id_t get_tid() const { return tid; }
action_type get_type() const { return type; }
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;
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
- earliest_diverge->print();
+ earliest_diverge->print(false);
else
printf("(Not set)\n");
action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
- scheduler->add_thread(get_thread((*rit)->get_tid()));
+ scheduler->wake(get_thread(*rit));
}
waiters->clear();
break;
break;
}
case THREAD_JOIN: {
- Thread *waiting, *blocking;
- waiting = get_thread(curr);
- blocking = (Thread *)curr->get_location();
- if (!blocking->is_complete()) {
- blocking->push_wait_list(curr);
- scheduler->sleep(waiting);
- } else {
- do_complete_join(curr);
- synchronized = true;
- }
+ Thread *blocking = (Thread *)curr->get_location();
+ ModelAction *act = get_last_action(blocking->get_id());
+ curr->synchronize_with(act);
+ synchronized = true;
break;
}
case THREAD_FINISH: {
Thread *th = get_thread(curr);
while (!th->wait_list_empty()) {
ModelAction *act = th->pop_wait_list();
- Thread *wake = get_thread(act);
- scheduler->wake(wake);
- do_complete_join(act);
- synchronized = true;
+ scheduler->wake(get_thread(act));
}
th->complete();
break;
return newcurr;
}
+ 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 */
}
/**
- * This method checks whether a model action is enabled at the given point.
- * At this point, it checks whether a lock operation would be successful at this point.
- * If not, it puts the thread in a waiter list.
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
* @param curr is the ModelAction to check whether it is enabled.
* @return a bool that indicates whether the action is enabled.
*/
lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
return false;
}
+ } else if (curr->get_type() == THREAD_JOIN) {
+ Thread *blocking = (Thread *)curr->get_location();
+ if (!blocking->is_complete()) {
+ blocking->push_wait_list(curr);
+ return false;
+ }
}
return true;
if (!check_action_enabled(curr)) {
/* Make the execution look like we chose to run this action
- * much later, when a lock is actually available to release */
+ * much later, when a lock/join can succeed */
get_current_thread()->set_pending(curr);
- remove_thread(get_current_thread());
+ scheduler->sleep(get_current_thread());
return get_next_thread(NULL);
}
return get_next_thread(curr);
}
-/**
- * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
- * operation from the Thread it is joining with. Must be called after the
- * completion of the Thread in question.
- * @param join The THREAD_JOIN action
- */
-void ModelChecker::do_complete_join(ModelAction *join)
-{
- Thread *blocking = (Thread *)join->get_location();
- ModelAction *act = get_last_action(blocking->get_id());
- join->synchronize_with(act);
-}
-
void ModelChecker::check_curr_backtracking(ModelAction * curr) {
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
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(); }
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
bool w_modification_order(ModelAction *curr);
bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
- void do_complete_join(ModelAction *join);
ModelAction *diverge;
ModelAction *earliest_diverge;