#include "model.h"
#include "execution.h"
#include "action.h"
-#include "nodestack.h"
#include "schedule.h"
#include "common.h"
#include "clockvector.h"
#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
+#include "history.h"
+#include "fuzzer.h"
+#include "newfuzzer.h"
-#define INITIAL_THREAD_ID 0
+#define INITIAL_THREAD_ID 0
/**
* Structure for holding small ModelChecker members that should be snapshotted
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
- next_backtrack(NULL),
bugs(),
- too_many_reads(false),
- no_valid_reads(false),
bad_synchronization(false),
- bad_sc_read(false),
asserted(false)
{ }
~model_snapshot_members() {
- for (unsigned int i = 0; i < bugs.size(); i++)
+ 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 too_many_reads;
- bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
- bool bad_sc_read;
bool asserted;
SNAPSHOTALLOC
};
/** @brief Constructor */
-ModelExecution::ModelExecution(ModelChecker *m,
- const struct model_params *params,
- Scheduler *scheduler,
- NodeStack *node_stack) :
- pthread_counter(0),
+ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
model(m),
- params(params),
+ params(NULL),
scheduler(scheduler),
action_trace(),
- thread_map(2), /* We'll always need at least 2 threads */
+ thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
+ pthread_counter(1),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
mutex_map(),
- cond_map(),
- 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())
+ priv(new struct model_snapshot_members ()),
+ mo_graph(new CycleGraph()),
+ fuzzer(new NewFuzzer()),
+ thrd_func_list(),
+ thrd_func_act_lists(),
+ isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
- model_thread = new Thread(get_next_id()); // L: Create model thread
- add_thread(model_thread); // L: Add model thread to scheduler
+ model_thread = new Thread(get_next_id());
+ add_thread(model_thread);
scheduler->register_engine(this);
- node_stack->register_engine(this);
+ fuzzer->register_engine(m->get_history(), this);
}
/** @brief Destructor */
ModelExecution::~ModelExecution()
{
- for (unsigned int i = 0; i < get_num_threads(); i++)
+ for (unsigned int i = 0;i < get_num_threads();i++)
delete get_thread(int_to_id(i));
delete mo_graph;
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)
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
{
action_list_t *tmp = hash->get(ptr);
if (tmp == NULL) {
return tmp;
}
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
{
SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
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->used_sequence_numbers;
}
+/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
+void ModelExecution::restore_last_seq_num()
+{
+ priv->used_sequence_numbers--;
+}
+
/**
* @brief Should the current action wake up a given thread?
*
if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
return true;
}
+ /* The sleep is literally sleeping */
+ if (asleep->is_sleep()) {
+ if (fuzzer->shouldWake(asleep))
+ return true;
+ }
+
return false;
}
void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
{
- for (unsigned int i = 0; i < get_num_threads(); i++) {
+ 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))
+ if (should_wake_up(curr, thr)) {
/* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
+ if (thr->get_pending()->is_sleep())
+ thr->set_wakeup_state(true);
+ }
}
}
}
priv->bad_synchronization = true;
}
-/** @brief Alert the model-checker that an incorrectly-ordered
- * synchronization was made */
-void ModelExecution::set_bad_sc_read()
-{
- priv->bad_sc_read = true;
-}
-
bool ModelExecution::assert_bug(const char *msg)
{
priv->bugs.push_back(new bug_message(msg));
bool ModelExecution::is_deadlocked() const
{
bool blocking_threads = false;
- for (unsigned int i = 0; i < get_num_threads(); i++) {
+ for (unsigned int i = 0;i < get_num_threads();i++) {
thread_id_t tid = int_to_id(i);
if (is_enabled(tid))
return false;
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
*/
bool ModelExecution::is_complete_execution() const
{
- if (is_yieldblocked())
- return false;
- for (unsigned int i = 0; i < get_num_threads(); i++)
+ 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;
+ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
+ uint64_t value = *((const uint64_t *) location);
+ modelclock_t storeclock;
+ thread_id_t storethread;
+ getStoreThreadAndClock(location, &storethread, &storeclock);
+ setAtomicStoreFlag(location);
+ ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
+ act->set_seq_number(storeclock);
+ add_normal_write_to_lists(act);
+ add_write_to_lists(act);
+ w_modification_order(act);
+ model->get_history()->process_action(act, act->get_tid());
+ return act;
}
/**
- * @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.
+ * Processes a read model action.
+ * @param curr is the read model action to process.
+ * @param rf_set is the set of model actions we can possibly read from
+ * @return True if processing this read updates the mo_graph.
*/
-void ModelExecution::set_backtracking(ModelAction *act)
+bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
{
- 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();
+ SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
+ bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
+ if (hasnonatomicstore) {
+ ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
+ rf_set->push_back(nonatomicstore);
}
- 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();
+ // Remove writes that violate read modification order
+ for (uint i = 0; i < rf_set->size(); i++) {
+ ModelAction * rf = (*rf_set)[i];
+ if (!r_modification_order(curr, rf, NULL, NULL, true)) {
+ (*rf_set)[i] = rf_set->back();
+ rf_set->pop_back();
}
}
-}
-/**
- * @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;
-}
+ while(true) {
+ int index = fuzzer->selectWrite(curr, rf_set);
+ if (index == -1) // no feasible write exists
+ 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;
-}
+ ModelAction *rf = (*rf_set)[index];
-/**
- * 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;
- }
+ ASSERT(rf);
+ bool canprune = false;
+ if (r_modification_order(curr, rf, priorset, &canprune)) {
+ for(unsigned int i=0;i<priorset->size();i++) {
+ mo_graph->addEdge((*priorset)[i], rf);
}
-
- updated = r_modification_order(curr, rf);
read_from(curr, rf);
- mo_graph->commitChanges();
- break;
- }
- default:
- ASSERT(false);
+ get_thread(curr)->set_return_value(curr->get_return_value());
+ delete priorset;
+ if (canprune && curr->get_type() == ATOMIC_READ) {
+ int tid = id_to_int(curr->get_tid());
+ (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
+ }
+ return true;
}
- get_thread(curr)->set_return_value(curr->get_return_value());
- return updated;
+ priorset->clear();
+ (*rf_set)[index] = rf_set->back();
+ rf_set->pop_back();
}
}
}
get_thread(curr)->set_return_value(1);
}
- //otherwise fall into the lock case
+ //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");
+ //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
+ //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
}
break;
}
- case ATOMIC_WAIT:
- case ATOMIC_UNLOCK: {
+ case ATOMIC_WAIT: {
/* wake up the other threads */
- for (unsigned int i = 0; i < get_num_threads(); i++) {
+ 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())
/* 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) {
+ if (fuzzer->shouldWait(curr)) {
+ /* disable this thread */
get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
- /* disable us */
scheduler->sleep(get_thread(curr));
}
+
+ break;
+ }
+ case ATOMIC_TIMEDWAIT:
+ case ATOMIC_UNLOCK: {
+ //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
+
+ /* 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;
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));
+ for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
+ scheduler->wake(get_thread(rit->getVal()));
}
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();
-
- // WL
- if (it == waiters->end())
- break;
-
- advance(it, wakeupthread);
- scheduler->wake(get_thread(*it));
- waiters->erase(it);
+ if (waiters->size() != 0) {
+ Thread * thread = fuzzer->selectNotify(waiters);
+ scheduler->wake(thread);
+ }
break;
}
/**
* 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)
+void ModelExecution::process_write(ModelAction *curr)
{
-
- bool updated_mod_order = w_modification_order(curr);
-
- mo_graph->commitChanges();
-
+ w_modification_order(curr);
get_thread(curr)->set_return_value(VALUE_NONE);
- return updated_mod_order;
}
/**
bool updated = false;
if (curr->is_acquire()) {
action_list_t *list = &action_trace;
- action_list_t::reverse_iterator rit;
+ sllnode<ModelAction *> * rit;
/* Find X : is_read(X) && X --sb-> curr */
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
if (act == curr)
continue;
if (act->get_tid() != curr->get_tid())
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)
+ ClockVector *cv = get_hb_from_write(act->get_reads_from());
+ if (cv != NULL && curr->get_cv()->merge(cv))
updated = true;
}
}
* @param curr The current action
* @return True if synchronization was updated or a thread completed
*/
-bool ModelExecution::process_thread_action(ModelAction *curr)
+void ModelExecution::process_thread_action(ModelAction *curr)
{
- bool updated = false;
-
switch (curr->get_type()) {
case THREAD_CREATE: {
thrd_t *thrd = (thrd_t *)curr->get_location();
break;
}
case PTHREAD_CREATE: {
- (*(pthread_t *)curr->get_location()) = pthread_counter++;
+ (*(uint32_t *)curr->get_location()) = pthread_counter++;
struct pthread_params *params = (struct pthread_params *)curr->get_value();
Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
add_thread(th);
th->set_creation(curr);
- if ( pthread_map.size() < pthread_counter )
- pthread_map.resize( pthread_counter );
+ if ( pthread_map.size() < pthread_counter )
+ pthread_map.resize( pthread_counter );
pthread_map[ pthread_counter-1 ] = th;
break;
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 PTHREAD_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; // WL: to be add (modified)
+ break; // WL: to be add (modified)
}
+ case THREADONLY_FINISH:
case THREAD_FINISH: {
Thread *th = get_thread(curr);
+ if (curr->get_type() == THREAD_FINISH &&
+ th == model->getInitThread()) {
+ th->complete();
+ setFinished();
+ break;
+ }
+
/* Wake up any joining threads */
- for (unsigned int i = 0; i < get_num_threads(); i++) {
+ 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();
- updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
break;
}
+ case THREAD_SLEEP: {
+ Thread *th = get_thread(curr);
+ th->set_pending(curr);
+ scheduler->add_sleep(th);
+ break;
+ }
default:
break;
}
-
- return updated;
}
/**
* Initialize the current action by performing one or more of the following
- * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
- * in the NodeStack, manipulating backtracking sets, allocating and
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions,
+ * manipulating backtracking sets, allocating and
* initializing clock vectors, and computing the promises to fulfill.
*
* @param curr The current action, as passed from the user context; may be
*/
bool ModelExecution::initialize_curr_action(ModelAction **curr)
{
- ModelAction *newcurr;
-
if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
- newcurr = process_rmw(*curr);
+ ModelAction *newcurr = process_rmw(*curr);
delete *curr;
*curr = newcurr;
return false;
- }
-
- (*curr)->set_seq_number(get_next_seq_num());
-
- newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
- if (newcurr) {
- /* First restore type and order in case of RMW operation */
- if ((*curr)->is_rmwr())
- newcurr->copy_typeandorder(*curr);
-
- ASSERT((*curr)->get_location() == newcurr->get_location());
- newcurr->copy_from_new(*curr);
-
- /* Discard duplicate ModelAction; use action from NodeStack */
- delete *curr;
-
- /* Always compute new clock vector */
- newcurr->create_cv(get_parent_action(newcurr->get_tid()));
-
- *curr = newcurr;
- return false; /* Action was explored previously */
} else {
- newcurr = *curr;
+ ModelAction *newcurr = *curr;
+ newcurr->set_seq_number(get_next_seq_num());
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/* Assign most recent release fence */
newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
- /*
- * Perform one-time actions when pushing new ModelAction onto
- * NodeStack
- */
- if (newcurr->is_wait())
- newcurr->get_node()->set_misc_max(2);
- else if (newcurr->is_notify_one()) {
- newcurr->get_node()->set_misc_max(get_safe_ptr_action(&condvar_waiters_map, newcurr->get_location())->size());
- }
- return true; /* This was a new ModelAction */
+ return true; /* This was a new ModelAction */
}
}
* @return True if this read established synchronization
*/
-bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
+void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
{
ASSERT(rf);
ASSERT(rf->is_write());
act->set_read_from(rf);
if (act->is_acquire()) {
- rel_heads_list_t release_heads;
- get_release_seq_heads(act, act, &release_heads);
- int num_heads = release_heads.size();
- for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!synchronize(release_heads[i], act))
- num_heads--;
- return num_heads > 0;
+ ClockVector *cv = get_hb_from_write(rf);
+ if (cv == NULL)
+ return;
+ act->get_cv()->merge(cv);
}
- return false;
}
/**
if (!blocking->is_complete()) {
return false;
}
- } else if (params->yieldblock && curr->is_yield()) {
- return false;
+ } else if (curr->is_sleep()) {
+ if (!fuzzer->shouldSleep(curr))
+ return false;
}
return true;
wake_up_sleeping_actions(curr);
- /* Compute fairness information for CHESS yield algorithm */
- if (params->yieldon) {
- curr->get_node()->update_yield(scheduler);
- }
-
- /* Add the action to lists before any other model-checking tasks */
+ /* Add uninitialized actions to lists */
if (!second_part_of_rmw)
- add_action_to_lists(curr);
+ add_uninit_action_to_lists(curr);
+ SnapVector<ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
- build_may_read_from(curr);
+ rf_set = build_may_read_from(curr);
- /* Initialize work_queue with the "current action" work */
- work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
- while (!work_queue.empty() && !has_asserted()) {
- WorkQueueEntry work = work_queue.front();
- work_queue.pop_front();
+ if (curr->is_read() && !second_part_of_rmw) {
+ process_read(curr, rf_set);
+ delete rf_set;
- switch (work.type) {
- case WORK_CHECK_CURR_ACTION: {
- ModelAction *act = work.action;
+/* bool success = process_read(curr, rf_set);
+ delete rf_set;
+ if (!success)
+ return curr; // Do not add action to lists
+*/
+ } else
+ ASSERT(rf_set == NULL);
- process_thread_action(curr);
+ /* Add the action to lists */
+ if (!second_part_of_rmw)
+ add_action_to_lists(curr);
- if (act->is_read() && !second_part_of_rmw)
- process_read(act);
+ if (curr->is_write())
+ add_write_to_lists(curr);
- if (act->is_write())
- process_write(act, &work_queue);
-
- if (act->is_fence())
- process_fence(act);
-
- if (act->is_mutex_op())
- process_mutex(act);
+ process_thread_action(curr);
- break;
- }
- case WORK_CHECK_MO_EDGES: {
- /** @todo Complete verification of work_queue */
- ModelAction *act = work.action;
-
- if (act->is_read()) {
- const ModelAction *rf = act->get_reads_from();
- r_modification_order(act, rf);
- if (act->is_seqcst()) {
- ModelAction *last_sc_write = get_last_seq_cst_write(act);
- if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
- set_bad_sc_read();
- }
- }
- }
- if (act->is_write()) {
- w_modification_order(act);
- }
- mo_graph->commitChanges();
- break;
- }
- default:
- ASSERT(false);
- break;
- }
- }
+ if (curr->is_write())
+ process_write(curr);
- check_curr_backtracking(curr);
- set_backtracking(curr);
- return curr;
-}
+ if (curr->is_fence())
+ process_fence(curr);
-void ModelExecution::check_curr_backtracking(ModelAction *curr)
-{
- Node *currnode = curr->get_node();
- Node *parnode = currnode->get_parent();
+ if (curr->is_mutex_op())
+ process_mutex(curr);
- if ((parnode && !parnode->backtrack_empty()) ||
- !currnode->misc_empty() ||
- !currnode->read_from_empty()) {
- set_latest_backtrack(curr);
- }
+ return curr;
}
/**
*/
bool ModelExecution::isfeasibleprefix() const
{
- return !is_infeasible();
+ return !is_infeasible();
}
/**
{
char buf[100];
char *ptr = buf;
- if (mo_graph->checkForCycles())
- ptr += sprintf(ptr, "[mo cycle]");
- if (priv->too_many_reads)
- ptr += sprintf(ptr, "[too many reads]");
- if (priv->no_valid_reads)
- ptr += sprintf(ptr, "[no valid reads-from]");
if (priv->bad_synchronization)
ptr += sprintf(ptr, "[bad sw ordering]");
- if (priv->bad_sc_read)
- ptr += sprintf(ptr, "[bad sc read]");
if (ptr != buf)
model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
}
*/
bool ModelExecution::is_infeasible() const
{
- return mo_graph->checkForCycles() ||
- priv->no_valid_reads ||
- priv->too_many_reads ||
- priv->bad_synchronization ||
- priv->bad_sc_read;
+ return priv->bad_synchronization;
}
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
ModelAction *lastread = get_last_action(act->get_tid());
lastread->process_rmw(act);
if (act->is_rmw()) {
- mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
- mo_graph->commitChanges();
+ mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
}
return lastread;
}
-/**
- * A helper function for ModelExecution::check_recency, to check if the current
- * thread is able to read from a different write/promise for 'params.maxreads'
- * number of steps and if that write/promise should become visible (i.e., is
- * ordered later in the modification order). This helps model memory liveness.
- *
- * @param curr The current action. Must be a read.
- * @param rf The write/promise from which we plan to read
- * @param other_rf The write/promise from which we may read
- * @return True if we were able to read from other_rf for params.maxreads steps
- */
-template <typename T, typename U>
-bool ModelExecution::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
-{
- /* Need a different write/promise */
- if (other_rf->equals(rf))
- return false;
-
- /* Only look for "newer" writes/promises */
- if (!mo_graph->checkReachable(rf, other_rf))
- return false;
-
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
- action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
- action_list_t::reverse_iterator rit = list->rbegin();
- ASSERT((*rit) == curr);
- /* Skip past curr */
- rit++;
-
- /* Does this write/promise work for everyone? */
- for (int i = 0; i < params->maxreads; i++, rit++) {
- ModelAction *act = *rit;
- if (!act->may_read_from(other_rf))
- return false;
- }
- return true;
-}
-
-/**
- * Checks whether a thread has read from the same write or Promise for too many
- * times without seeing the effects of a later write/Promise.
- *
- * Basic idea:
- * 1) there must a different write/promise that we could read from,
- * 2) we must have read from the same write/promise in excess of maxreads times,
- * 3) that other write/promise must have been in the reads_from set for maxreads times, and
- * 4) that other write/promise must be mod-ordered after the write/promise we are reading.
- *
- * If so, we decide that the execution is no longer feasible.
- *
- * @param curr The current action. Must be a read.
- * @param rf The ModelAction/Promise from which we might read.
- * @return True if the read should succeed; false otherwise
- */
-template <typename T>
-bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const
-{
- if (!params->maxreads)
- return true;
-
- //NOTE: Next check is just optimization, not really necessary....
- if (curr->get_node()->get_read_from_past_size() <= 1)
- return true;
-
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
- int tid = id_to_int(curr->get_tid());
- ASSERT(tid < (int)thrd_lists->size());
- action_list_t *list = &(*thrd_lists)[tid];
- action_list_t::reverse_iterator rit = list->rbegin();
- ASSERT((*rit) == curr);
- /* Skip past curr */
- rit++;
-
- action_list_t::reverse_iterator ritcopy = rit;
- /* See if we have enough reads from the same value */
- for (int count = 0; count < params->maxreads; ritcopy++, count++) {
- if (ritcopy == list->rend())
- return true;
- ModelAction *act = *ritcopy;
- if (!act->is_read())
- return true;
- if (act->get_reads_from() && !act->get_reads_from()->equals(rf))
- return true;
- if (act->get_node()->get_read_from_past_size() <= 1)
- return true;
- }
- for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
- const ModelAction *write = curr->get_node()->get_read_from_past(i);
- if (should_read_instead(curr, rf, write))
- return false; /* liveness failure */
- }
- return true;
-}
-
/**
* @brief Updates the mo_graph with the constraints imposed from the current
* read.
*
* @param curr The current action. Must be a read.
* @param rf The ModelAction or Promise that curr reads from. Must be a write.
+ * @param check_only If true, then only check whether the current action satisfies
+ * read modification order or not, without modifiying priorset and canprune.
+ * False by default.
* @return True if modification order edges were added; false otherwise
*/
-template <typename rf_type>
-bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
+
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
+ SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
- bool added = false;
ASSERT(curr->is_read());
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
- ModelAction *last_sc_write = NULL;
- if (curr->is_seqcst())
- last_sc_write = get_last_seq_cst_write(curr);
+ int tid = curr->get_tid();
+ ModelAction *prev_same_thread = NULL;
/* Iterate over all threads */
- for (i = 0; i < thrd_lists->size(); i++) {
- /* Last SC fence in thread i */
+ for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
+ /* Last SC fence in thread tid */
ModelAction *last_sc_fence_thread_local = NULL;
- if (int_to_id((int)i) != curr->get_tid())
- last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+ if (i != 0)
+ last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
- /* Last SC fence in thread i, before last SC fence in current thread */
+ /* Last SC fence in thread tid, before last SC fence in current thread */
ModelAction *last_sc_fence_thread_before = NULL;
if (last_sc_fence_local)
- last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
+
+ //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
+ if (prev_same_thread != NULL &&
+ (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
+ (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
+ continue;
+ }
/* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
+ action_list_t *list = &(*thrd_lists)[tid];
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
/* Skip curr */
if (act == curr)
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
- added = mo_graph->addEdge(act, rf) || added;
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ if (!check_only)
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
- *act < *last_sc_fence_local) {
- added = mo_graph->addEdge(act, rf) || added;
+ *act < *last_sc_fence_local) {
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ if (!check_only)
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
- *act < *last_sc_fence_thread_before) {
- added = mo_graph->addEdge(act, rf) || added;
+ *act < *last_sc_fence_thread_before) {
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ if (!check_only)
+ priorset->push_back(act);
break;
}
}
* before" curr
*/
if (act->happens_before(curr)) {
+ if (i==0) {
+ if (last_sc_fence_local == NULL ||
+ (*last_sc_fence_local < *act)) {
+ prev_same_thread = act;
+ }
+ }
if (act->is_write()) {
- added = mo_graph->addEdge(act, rf) || added;
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ if (!check_only)
+ priorset->push_back(act);
} else {
const ModelAction *prevrf = act->get_reads_from();
- if (!prevrf->equals(rf))
- added = mo_graph->addEdge(prevrf, rf) || added;
+ if (!prevrf->equals(rf)) {
+ if (mo_graph->checkReachable(rf, prevrf))
+ return false;
+ if (!check_only)
+ priorset->push_back(prevrf);
+ } else {
+ if (act->get_tid() == curr->get_tid()) {
+ //Can prune curr from obj list
+ if (!check_only)
+ *canprune = true;
+ }
+ }
}
break;
}
}
}
-
- /*
- * All compatible, thread-exclusive promises must be ordered after any
- * concrete loads from the same thread
- */
-
- return added;
+ return true;
}
/**
* value. If NULL, then don't record any future values.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelExecution::w_modification_order(ModelAction *curr)
+void ModelExecution::w_modification_order(ModelAction *curr)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
- bool added = false;
ASSERT(curr->is_write());
+ SnapList<ModelAction *> edgeset;
+
if (curr->is_seqcst()) {
/* We have to at least see the last sequentially consistent write,
- so we are initialized. */
+ so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
- added = mo_graph->addEdge(last_seq_cst, curr) || added;
+ edgeset.push_back(last_seq_cst);
}
+ //update map for next query
+ obj_last_sc_map.put(curr->get_location(), curr);
}
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
/* Iterate over all threads */
- for (i = 0; i < thrd_lists->size(); i++) {
+ for (i = 0;i < thrd_lists->size();i++) {
/* Last SC fence in thread i, before last SC fence in current thread */
ModelAction *last_sc_fence_thread_before = NULL;
if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction*>* rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
if (act == curr) {
/*
* 1) If RMW and it actually read from something, then we
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
- added = mo_graph->addEdge(act, curr) || added;
+ edgeset.push_back(act);
break;
}
* readfrom(act) --mo--> act
*/
if (act->is_write())
- added = mo_graph->addEdge(act, curr) || added;
+ edgeset.push_back(act);
else if (act->is_read()) {
//if previous read accessed a null, just keep going
- added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+ edgeset.push_back(act->get_reads_from());
}
break;
- } else if (act->is_read() && !act->could_synchronize_with(curr) &&
- !act->same_thread(curr)) {
- /* We have an action that:
- (1) did not happen before us
- (2) is a read and we are a write
- (3) cannot synchronize with us
- (4) is in a different thread
- =>
- that read could potentially read from our write. Note that
- these checks are overly conservative at this point, we'll
- do more checks before actually removing the
- pendingfuturevalue.
-
- */
-
}
}
}
+ mo_graph->addEdges(&edgeset, curr);
- return added;
}
/**
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
unsigned int i;
/* Iterate over all threads */
- for (i = 0; i < thrd_lists->size(); i++) {
+ for (i = 0;i < thrd_lists->size();i++) {
const ModelAction *write_after_read = NULL;
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction *>* rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
/* Don't disallow due to act == reader */
if (!reader->happens_before(act) || reader == act)
}
/**
- * Finds the head(s) of the release sequence(s) containing a given ModelAction.
- * The ModelAction under consideration is expected to be taking part in
- * release/acquire synchronization as an object of the "reads from" relation.
- * Note that this can only provide release sequence support for RMW chains
- * which do not read from the future, as those actions cannot be traced until
- * their "promise" is fulfilled. Similarly, we may not even establish the
- * presence of a release sequence with certainty, as some modification order
- * constraints may be decided further in the future. Thus, this function
- * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
- * and a boolean representing certainty.
+ * Computes the clock vector that happens before propagates from this write.
*
* @param rf The action that might be part of a release sequence. Must be a
* write.
- * @param release_heads A pass-by-reference style return parameter. After
- * execution of this function, release_heads will contain the heads of all the
- * relevant release sequences, if any exists with certainty
- * @param pending A pass-by-reference style return parameter which is only used
- * when returning false (i.e., uncertain). Returns most information regarding
- * an uncertain release sequence, including any write operations that might
- * break the sequence.
- * @return true, if the ModelExecution is certain that release_heads is complete;
- * false otherwise
+ * @return ClockVector of happens before relation.
*/
-bool ModelExecution::release_seq_heads(const ModelAction *rf,
- rel_heads_list_t *release_heads,
- struct release_seq *pending) const
-{
- /* Only check for release sequences if there are no cycles */
- if (mo_graph->checkForCycles())
- return false;
- for ( ; rf != NULL; rf = rf->get_reads_from()) {
+ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
+ SnapVector<ModelAction *> * processset = NULL;
+ for ( ;rf != NULL;rf = rf->get_reads_from()) {
ASSERT(rf->is_write());
-
- if (rf->is_release())
- release_heads->push_back(rf);
- else if (rf->get_last_fence_release())
- release_heads->push_back(rf->get_last_fence_release());
- if (!rf->is_rmw())
- break; /* End of RMW chain */
-
- /** @todo Need to be smarter here... In the linux lock
- * example, this will run to the beginning of the program for
- * every acquire. */
- /** @todo The way to be smarter here is to keep going until 1
- * thread has a release preceded by an acquire and you've seen
- * both. */
-
- /* acq_rel RMW is a sufficient stopping condition */
- if (rf->is_acquire() && rf->is_release())
- return true; /* complete */
- };
- if (!rf) {
- /* read from future: need to settle this later */
- pending->rf = NULL;
- return false; /* incomplete */
- }
-
- if (rf->is_release())
- return true; /* complete */
-
- /* else relaxed write
- * - check for fence-release in the same thread (29.8, stmt. 3)
- * - check modification order for contiguous subsequence
- * -> rf must be same thread as release */
-
- const ModelAction *fence_release = rf->get_last_fence_release();
- /* Synchronize with a fence-release unconditionally; we don't need to
- * find any more "contiguous subsequence..." for it */
- if (fence_release)
- release_heads->push_back(fence_release);
-
- int tid = id_to_int(rf->get_tid());
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(rf->get_location());
- action_list_t *list = &(*thrd_lists)[tid];
- action_list_t::const_reverse_iterator rit;
-
- /* Find rf in the thread list */
- rit = std::find(list->rbegin(), list->rend(), rf);
- ASSERT(rit != list->rend());
-
- /* Find the last {write,fence}-release */
- for (; rit != list->rend(); rit++) {
- if (fence_release && *(*rit) < *fence_release)
- break;
- if ((*rit)->is_release())
+ if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
break;
- }
- if (rit == list->rend()) {
- /* No write-release in this thread */
- return true; /* complete */
- } else if (fence_release && *(*rit) < *fence_release) {
- /* The fence-release is more recent (and so, "stronger") than
- * the most recent write-release */
- return true; /* complete */
- } /* else, need to establish contiguous release sequence */
- ModelAction *release = *rit;
-
- ASSERT(rf->same_thread(release));
-
- pending->writes.clear();
-
- bool certain = true;
- for (unsigned int i = 0; i < thrd_lists->size(); i++) {
- if (id_to_int(rf->get_tid()) == (int)i)
- continue;
- list = &(*thrd_lists)[i];
-
- /* Can we ensure no future writes from this thread may break
- * the release seq? */
- bool future_ordered = false;
-
- ModelAction *last = get_last_action(int_to_id(i));
- Thread *th = get_thread(int_to_id(i));
- if ((last && rf->happens_before(last)) ||
- !is_enabled(th) ||
- th->is_complete())
- future_ordered = true;
-
- ASSERT(!th->is_model_thread() || future_ordered);
-
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- const ModelAction *act = *rit;
- /* Reach synchronization -> this thread is complete */
- if (act->happens_before(release))
- break;
- if (rf->happens_before(act)) {
- future_ordered = true;
- continue;
- }
-
- /* Only non-RMW writes can break release sequences */
- if (!act->is_write() || act->is_rmw())
- continue;
-
- /* Check modification order */
- if (mo_graph->checkReachable(rf, act)) {
- /* rf --mo--> act */
- future_ordered = true;
- continue;
- }
- if (mo_graph->checkReachable(act, release))
- /* act --mo--> release */
- break;
- if (mo_graph->checkReachable(release, act) &&
- mo_graph->checkReachable(act, rf)) {
- /* release --mo-> act --mo--> rf */
- return true; /* complete */
+ if (processset == NULL)
+ processset = new SnapVector<ModelAction *>();
+ processset->push_back(rf);
+ }
+
+ int i = (processset == NULL) ? 0 : processset->size();
+
+ ClockVector * vec = NULL;
+ while(true) {
+ if (rf->get_rfcv() != NULL) {
+ vec = rf->get_rfcv();
+ } else if (rf->is_acquire() && rf->is_release()) {
+ vec = rf->get_cv();
+ } else if (rf->is_release() && !rf->is_rmw()) {
+ vec = rf->get_cv();
+ } else if (rf->is_release()) {
+ //have rmw that is release and doesn't have a rfcv
+ (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
+ rf->set_rfcv(vec);
+ } else {
+ //operation that isn't release
+ if (rf->get_last_fence_release()) {
+ if (vec == NULL)
+ vec = rf->get_last_fence_release()->get_cv();
+ else
+ (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
}
- /* act may break release sequence */
- pending->writes.push_back(act);
- certain = false;
+ rf->set_rfcv(vec);
}
- if (!future_ordered)
- certain = false; /* This thread is uncertain */
- }
-
- if (certain) {
- release_heads->push_back(release);
- pending->writes.clear();
- } else {
- pending->release = release;
- pending->rf = rf;
- }
- return certain;
-}
-
-/**
- * An interface for getting the release sequence head(s) with which a
- * given ModelAction must synchronize. This function only returns a non-empty
- * result when it can locate a release sequence head with certainty. Otherwise,
- * it may mark the internal state of the ModelExecution so that it will handle
- * the release sequence at a later time, causing @a acquire to update its
- * synchronization at some later point in execution.
- *
- * @param acquire The 'acquire' action that may synchronize with a release
- * sequence
- * @param read The read action that may read from a release sequence; this may
- * be the same as acquire, or else an earlier action in the same thread (i.e.,
- * when 'acquire' is a fence-acquire)
- * @param release_heads A pass-by-reference return parameter. Will be filled
- * with the head(s) of the release sequence(s), if they exists with certainty.
- * @see ModelExecution::release_seq_heads
- */
-void ModelExecution::get_release_seq_heads(ModelAction *acquire,
- ModelAction *read, rel_heads_list_t *release_heads)
-{
- const ModelAction *rf = read->get_reads_from();
- struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
- sequence->acquire = acquire;
- sequence->read = read;
-
- if (!release_seq_heads(rf, release_heads, sequence)) {
- /* add act to 'lazy checking' list */
- pending_rel_seqs.push_back(sequence);
- } else {
- snapshot_free(sequence);
+ i--;
+ if (i >= 0) {
+ rf = (*processset)[i];
+ } else
+ break;
}
+ if (processset != NULL)
+ delete processset;
+ return vec;
}
/**
- * @brief Propagate a modified clock vector to actions later in the execution
- * order
+ * Performs various bookkeeping operations for the current ModelAction when it is
+ * the first atomic action occurred at its memory location.
*
- * After an acquire operation lazily completes a release-sequence
- * synchronization, we must update all clock vectors for operations later than
- * the acquire in the execution order.
+ * For instance, adds uninitialized action to the per-object, per-thread action vector
+ * and to the action trace list of all thread actions.
*
- * @param acquire The ModelAction whose clock vector must be propagated
- * @param work The work queue to which we can add work items, if this
- * propagation triggers more updates (e.g., to the modification order)
+ * @param act is the ModelAction to process.
*/
-void ModelExecution::propagate_clockvector(ModelAction *acquire, work_queue_t *work)
+void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
{
- /* Re-check read-acquire for mo_graph edges */
- work->push_back(MOEdgeWorkEntry(acquire));
-
- /* propagate synchronization to later actions */
- action_list_t::reverse_iterator rit = action_trace.rbegin();
- for (; (*rit) != acquire; rit++) {
- ModelAction *propagate = *rit;
- if (acquire->happens_before(propagate)) {
- synchronize(acquire, propagate);
- /* Re-check 'propagate' for mo_graph edges */
- work->push_back(MOEdgeWorkEntry(propagate));
+ int tid = id_to_int(act->get_tid());
+ ModelAction *uninit = NULL;
+ int uninit_id = -1;
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ if (list->empty() && act->is_atomic_var()) {
+ uninit = get_uninitialized_action(act);
+ uninit_id = id_to_int(uninit->get_tid());
+ list->push_front(uninit);
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ if ((int)vec->size() <= uninit_id) {
+ int oldsize = (int) vec->size();
+ vec->resize(uninit_id + 1);
+ for(int i = oldsize; i < uninit_id + 1; i++) {
+ new (&(*vec)[i]) action_list_t();
+ }
}
+ (*vec)[uninit_id].push_front(uninit);
}
-}
-/**
- * Attempt to resolve all stashed operations that might synchronize with a
- * release sequence for a given location. This implements the "lazy" portion of
- * determining whether or not a release sequence was contiguous, since not all
- * modification order information is present at the time an action occurs.
- *
- * @param location The location/object that should be checked for release
- * sequence resolutions. A NULL value means to check all locations.
- * @param work_queue The work queue to which to add work items as they are
- * generated
- * @return True if any updates occurred (new synchronization, new mo_graph
- * edges)
- */
-bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *work_queue)
-{
- bool updated = false;
- SnapVector<struct release_seq *>::iterator it = pending_rel_seqs.begin();
- while (it != pending_rel_seqs.end()) {
- struct release_seq *pending = *it;
- ModelAction *acquire = pending->acquire;
- const ModelAction *read = pending->read;
-
- /* Only resolve sequences on the given location, if provided */
- if (location && read->get_location() != location) {
- it++;
- continue;
- }
+ // Update action trace, a total order of all actions
+ if (uninit)
+ action_trace.push_front(uninit);
- const ModelAction *rf = read->get_reads_from();
- rel_heads_list_t release_heads;
- bool complete;
- complete = release_seq_heads(rf, &release_heads, pending);
- for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!acquire->has_synchronized_with(release_heads[i]))
- if (synchronize(release_heads[i], acquire))
- updated = true;
-
- if (updated) {
- /* Propagate the changed clock vector */
- propagate_clockvector(acquire, work_queue);
- }
- if (complete) {
- it = pending_rel_seqs.erase(it);
- snapshot_free(pending);
- } else {
- it++;
- }
+ // Update obj_thrd_map, a per location, per thread, order of actions
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ if ((int)vec->size() <= tid) {
+ uint oldsize = vec->size();
+ vec->resize(priv->next_thread_id);
+ for(uint i = oldsize; i < priv->next_thread_id; i++)
+ new (&(*vec)[i]) action_list_t();
}
+ if (uninit)
+ (*vec)[uninit_id].push_front(uninit);
- // If we resolved promises or data races, see if we have realized a data race.
- checkDataRaces();
-
- return updated;
+ // Update thrd_last_action, the last action taken by each thrad
+ if ((int)thrd_last_action.size() <= tid)
+ thrd_last_action.resize(get_num_threads());
+ if (uninit)
+ thrd_last_action[uninit_id] = uninit;
}
+
/**
* Performs various bookkeeping operations for the current ModelAction. For
* instance, adds action to the per-object, per-thread action vector and to the
void ModelExecution::add_action_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- ModelAction *uninit = NULL;
- int uninit_id = -1;
action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- if (list->empty() && act->is_atomic_var()) {
- uninit = get_uninitialized_action(act);
- uninit_id = id_to_int(uninit->get_tid());
- list->push_front(uninit);
- }
list->push_back(act);
+ // Update action trace, a total order of all actions
action_trace.push_back(act);
- if (uninit)
- action_trace.push_front(uninit);
+ // Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
- if (tid >= (int)vec->size())
+ if ((int)vec->size() <= tid) {
+ uint oldsize = vec->size();
vec->resize(priv->next_thread_id);
+ for(uint i = oldsize; i < priv->next_thread_id; i++)
+ new (&(*vec)[i]) action_list_t();
+ }
(*vec)[tid].push_back(act);
- if (uninit)
- (*vec)[uninit_id].push_front(uninit);
+ // Update thrd_last_action, the last action taken by each thrad
if ((int)thrd_last_action.size() <= tid)
thrd_last_action.resize(get_num_threads());
thrd_last_action[tid] = act;
- if (uninit)
- thrd_last_action[uninit_id] = uninit;
+ // Update thrd_last_fence_release, the last release fence taken by each thread
if (act->is_fence() && act->is_release()) {
if ((int)thrd_last_fence_release.size() <= tid)
thrd_last_fence_release.resize(get_num_threads());
get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
- if (tid >= (int)vec->size())
+ if ((int)vec->size() <= tid) {
+ uint oldsize = vec->size();
vec->resize(priv->next_thread_id);
+ for(uint i = oldsize; i < priv->next_thread_id; i++)
+ new (&(*vec)[i]) action_list_t();
+ }
(*vec)[tid].push_back(act);
}
}
+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+ sllnode<ModelAction*> * rit = list->end();
+ modelclock_t next_seq = act->get_seq_number();
+ if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
+ list->push_back(act);
+ else {
+ for(;rit != NULL;rit=rit->getPrev()) {
+ if (rit->getVal()->get_seq_number() == next_seq) {
+ list->insertAfter(rit, act);
+ break;
+ }
+ }
+ }
+}
+
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+ sllnode<ModelAction*> * rit = list->end();
+ modelclock_t next_seq = act->get_seq_number();
+ if (rit == NULL) {
+ act->create_cv(NULL);
+ } else if (rit->getVal()->get_seq_number() == next_seq) {
+ act->create_cv(rit->getVal());
+ list->push_back(act);
+ } else {
+ for(;rit != NULL;rit=rit->getPrev()) {
+ if (rit->getVal()->get_seq_number() == next_seq) {
+ act->create_cv(rit->getVal());
+ list->insertAfter(rit, act);
+ break;
+ }
+ }
+ }
+}
+
+/**
+ * Performs various bookkeeping operations for a normal write. The
+ * complication is that we are typically inserting a normal write
+ * lazily, so we need to insert it into the middle of lists.
+ *
+ * @param act is the ModelAction to add.
+ */
+
+void ModelExecution::add_normal_write_to_lists(ModelAction *act)
+{
+ int tid = id_to_int(act->get_tid());
+ insertIntoActionListAndSetCV(&action_trace, act);
+
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ insertIntoActionList(list, act);
+
+ // Update obj_thrd_map, a per location, per thread, order of actions
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ if (tid >= (int)vec->size()) {
+ uint oldsize =vec->size();
+ vec->resize(priv->next_thread_id);
+ for(uint i=oldsize;i<priv->next_thread_id;i++)
+ new (&(*vec)[i]) action_list_t();
+ }
+ insertIntoActionList(&(*vec)[tid],act);
+
+ // Update thrd_last_action, the last action taken by each thrad
+ if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
+ thrd_last_action[tid] = act;
+}
+
+
+void ModelExecution::add_write_to_lists(ModelAction *write) {
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
+ int tid = id_to_int(write->get_tid());
+ if (tid >= (int)vec->size()) {
+ uint oldsize =vec->size();
+ vec->resize(priv->next_thread_id);
+ for(uint i=oldsize;i<priv->next_thread_id;i++)
+ new (&(*vec)[i]) action_list_t();
+ }
+ (*vec)[tid].push_back(write);
+}
+
/**
* @brief Get the last action performed by a particular Thread
* @param tid The thread ID of the Thread in question
ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map.get(location);
- /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); (*rit) != curr; rit++)
- ;
- rit++; /* Skip past curr */
- for ( ; rit != list->rend(); rit++)
- if ((*rit)->is_write() && (*rit)->is_seqcst())
- return *rit;
- return NULL;
+ return obj_last_sc_map.get(location);
}
/**
if (!list)
return NULL;
- action_list_t::reverse_iterator rit = list->rbegin();
+ sllnode<ModelAction*>* rit = list->end();
if (before_fence) {
- for (; rit != list->rend(); rit++)
- if (*rit == before_fence)
+ for (;rit != NULL;rit=rit->getPrev())
+ if (rit->getVal() == before_fence)
break;
- ASSERT(*rit == before_fence);
- rit++;
+ ASSERT(rit->getVal() == before_fence);
+ rit=rit->getPrev();
}
- for (; rit != list->rend(); rit++)
- if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
- return *rit;
+ for (;rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
+ if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
+ return act;
+ }
return NULL;
}
action_list_t *list = obj_map.get(location);
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++)
- if ((*rit)->is_unlock() || (*rit)->is_wait())
- return *rit;
+ sllnode<ModelAction*>* rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev())
+ if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
+ return rit->getVal();
return NULL;
}
*/
ClockVector * ModelExecution::get_cv(thread_id_t tid) const
{
- return get_parent_action(tid)->get_cv();
+ ModelAction *firstaction=get_parent_action(tid);
+ return firstaction != NULL ? firstaction->get_cv() : NULL;
+}
+
+bool valequals(uint64_t val1, uint64_t val2, int size) {
+ switch(size) {
+ case 1:
+ return ((uint8_t)val1) == ((uint8_t)val2);
+ case 2:
+ return ((uint16_t)val1) == ((uint16_t)val2);
+ case 4:
+ return ((uint32_t)val1) == ((uint32_t)val2);
+ case 8:
+ return val1==val2;
+ default:
+ ASSERT(0);
+ return false;
+ }
}
/**
* @param curr is the current ModelAction that we are exploring; it must be a
* 'read' operation.
*/
-void ModelExecution::build_may_read_from(ModelAction *curr)
+SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
+ SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
+ SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
+
/* Iterate over all threads */
- for (i = 0; i < thrd_lists->size(); i++) {
+ for (i = 0;i < thrd_lists->size();i++) {
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
- /* Only consider 'write' actions */
- if (!act->is_write() || act == curr)
+ if (act == curr)
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
allow_read = false;
- else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
- allow_read = false;
+
+ /* Need to check whether we will have two RMW reading from the same value */
+ if (curr->is_rmwr()) {
+ /* It is okay if we have a failing CAS */
+ if (!curr->is_rmwrcas() ||
+ valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+ //Need to make sure we aren't the second RMW
+ CycleNode * node = mo_graph->getNode_noCreate(act);
+ if (node != NULL && node->getRMW() != NULL) {
+ //we are the second RMW
+ allow_read = false;
+ }
+ }
+ }
if (allow_read) {
/* Only add feasible reads */
- mo_graph->startChanges();
- r_modification_order(curr, act);
- if (!is_infeasible())
- curr->get_node()->add_read_from_past(act);
- mo_graph->rollbackChanges();
+ rf_set->push_back(act);
}
/* Include at most one act per-thread that "happens before" curr */
}
}
- /* We may find no valid may-read-from only if the execution is doomed */
- if (!curr->get_node()->read_from_size()) {
- priv->no_valid_reads = true;
- set_assert();
- }
-
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
curr->print();
- model_print("Printing read_from_past\n");
- curr->get_node()->print_read_from_past();
model_print("End printing read_from_past\n");
}
-}
-
-bool ModelExecution::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
-{
- for ( ; write != NULL; write = write->get_reads_from()) {
- /* UNINIT actions don't have a Node, and they never sleep */
- if (write->is_uninitialized())
- return true;
- Node *prevnode = write->get_node()->get_parent();
-
- bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
- if (write->is_release() && thread_sleep)
- return true;
- if (!write->is_rmw())
- return false;
- }
- return true;
+ return rf_set;
}
/**
* @brief Get an action representing an uninitialized atomic
*
- * This function may create a new one or try to retrieve one from the NodeStack
+ * This function may create a new one.
*
* @param curr The current action, which prompts the creation of an UNINIT action
* @return A pointer to the UNINIT ModelAction
*/
-ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
+ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
{
- Node *node = curr->get_node();
- ModelAction *act = node->get_uninit_action();
+ ModelAction *act = curr->get_uninit_action();
if (!act) {
act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
- node->set_uninit_action(act);
+ curr->set_uninit_action(act);
}
act->create_cv(NULL);
return act;
}
-static void print_list(const action_list_t *list)
+static void print_list(action_list_t *list)
{
- action_list_t::const_iterator it;
+ sllnode<ModelAction*> *it;
model_print("------------------------------------------------------------------------------------\n");
model_print("# t Action type MO Location Value Rf CV\n");
unsigned int hash = 0;
- for (it = list->begin(); it != list->end(); it++) {
- const ModelAction *act = *it;
+ for (it = list->begin();it != NULL;it=it->getNext()) {
+ const ModelAction *act = it->getVal();
if (act->get_seq_number() > 0)
act->print();
- hash = hash^(hash<<3)^((*it)->hash());
+ hash = hash^(hash<<3)^(it->getVal()->hash());
}
model_print("HASH %u\n", hash);
model_print("------------------------------------------------------------------------------------\n");
}
#if SUPPORT_MOD_ORDER_DUMP
-void ModelExecution::dumpGraph(char *filename) const
+void ModelExecution::dumpGraph(char *filename)
{
char buffer[200];
sprintf(buffer, "%s.dot", filename);
mo_graph->dumpNodes(file);
ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
- for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
- ModelAction *act = *it;
+ for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
+ ModelAction *act = it->getVal();
if (act->is_read()) {
mo_graph->dot_print_node(file, act);
mo_graph->dot_print_edge(file,
- act->get_reads_from(),
- act,
- "label=\"rf\", color=red, weight=2");
+ act->get_reads_from(),
+ act,
+ "label=\"rf\", color=red, weight=2");
}
if (thread_array[act->get_tid()]) {
mo_graph->dot_print_edge(file,
- thread_array[id_to_int(act->get_tid())],
- act,
- "label=\"sb\", color=blue, weight=400");
+ thread_array[id_to_int(act->get_tid())],
+ act,
+ "label=\"sb\", color=blue, weight=400");
}
thread_array[act->get_tid()] = act;
#endif
/** @brief Prints an execution trace summary. */
-void ModelExecution::print_summary() const
+void ModelExecution::print_summary()
{
#if SUPPORT_MOD_ORDER_DUMP
char buffername[100];
model_print("Execution trace %d:", get_execution_number());
if (isfeasibleprefix()) {
- if (is_yieldblocked())
- model_print(" YIELD BLOCKED");
if (scheduler->all_threads_sleeping())
model_print(" SLEEP-SET REDUNDANT");
if (have_bug_reports())
* @return A Thread reference
*/
Thread * ModelExecution::get_pthread(pthread_t pid) {
- if (pid < pthread_counter + 1) return pthread_map[pid];
- else return NULL;
+ union {
+ pthread_t p;
+ uint32_t v;
+ } x;
+ x.p = pid;
+ uint32_t thread_id = x.v;
+ if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
+ else return NULL;
}
/**
Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
{
/* Do not split atomic RMW */
- if (curr->is_rmwr())
+ if (curr->is_rmwr() && !paused_by_fuzzer(curr))
return get_thread(curr);
- if (curr->is_write()) {
-// std::memory_order order = curr->get_mo();
-// switch(order) {
-// case std::memory_order_relaxed:
-// return get_thread(curr);
-// case std::memory_order_release:
-// return get_thread(curr);
-// defalut:
-// return NULL;
-// }
- return NULL;
- }
-
/* Follow CREATE with the created thread */
/* which is not needed, because model.cc takes care of this */
if (curr->get_type() == THREAD_CREATE)
- return curr->get_thread_operand();
+ return curr->get_thread_operand();
if (curr->get_type() == PTHREAD_CREATE) {
return curr->get_thread_operand();
}
return NULL;
}
-/** @return True if the execution has taken too many steps */
-bool ModelExecution::too_many_steps() const
+/** @param act A read atomic action */
+bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
{
- return params->bound != 0 && priv->used_sequence_numbers > params->bound;
+ ASSERT(act->is_read());
+
+ // Actions paused by fuzzer have their sequence number reset to 0
+ return act->get_seq_number() == 0;
}
/**
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
- ASSERT(check_action_enabled(curr)); /* May have side effects? */
+ ASSERT(check_action_enabled(curr)); /* May have side effects? */
curr = check_current_action(curr);
ASSERT(curr);
+ /* Process this action in ModelHistory for records */
+ model->get_history()->process_action( curr, curr->get_tid() );
+
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
return action_select_next_thread(curr);
}
+Fuzzer * ModelExecution::getFuzzer() {
+ return fuzzer;
+}
projects / c11tester.git / blobdiff