#include "model.h"
#include "execution.h"
#include "action.h"
-#include "nodestack.h"
#include "schedule.h"
#include "common.h"
#include "clockvector.h"
};
/** @brief Constructor */
-ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
+ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
model(m),
params(NULL),
scheduler(scheduler),
action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
- pthread_counter(0),
+ pthread_counter(1),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
mutex_map(),
thrd_last_action(1),
thrd_last_fence_release(),
- node_stack(node_stack),
priv(new struct model_snapshot_members ()),
- mo_graph(new CycleGraph()),
+ mo_graph(new CycleGraph()),
fuzzer(new Fuzzer())
{
/* 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 */
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, 4> * 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()
{
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
- const ModelAction *rf = (*rf_set)[index];
+ ModelAction *rf = (*rf_set)[index];
ASSERT(rf);
-
- if (r_modification_order(curr, rf, priorset)) {
+ 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);
}
read_from(curr, rf);
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;
}
priorset->clear();
}
case ATOMIC_WAIT:
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));
}
case ATOMIC_NOTIFY_ONE: {
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
- Thread * thread = fuzzer->selectNotify(waiters);
- scheduler->wake(thread);
+ if (waiters->size() != 0) {
+ Thread * thread = fuzzer->selectNotify(waiters);
+ scheduler->wake(thread);
+ }
break;
}
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);
+ if (curr->get_cv()->merge(cv))
updated = true;
}
}
/**
* 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);
- 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()));
* @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;
}
/**
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
- if (!second_part_of_rmw)
+ if (!second_part_of_rmw && curr->get_type() != NOOP)
add_action_to_lists(curr);
SnapVector<ModelAction *> * rf_set = NULL;
* @return True if modification order edges were added; false otherwise
*/
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
/* 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 *list = &(*thrd_lists)[tid];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin();rit != list->rend();rit++) {
ModelAction *act = *rit;
* before" curr
*/
if (act->happens_before(curr)) {
+ if (i==0) {
+ if (last_sc_fence_local == NULL ||
+ (*last_sc_fence_local < *prev_same_thread)) {
+ prev_same_thread = act;
+ }
+ }
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
if (mo_graph->checkReachable(rf, prevrf))
return false;
priorset->push_back(prevrf);
+ } else {
+ if (act->get_tid() == curr->get_tid()) {
+ //Can prune curr from obj list
+ *canprune = true;
+ }
}
}
break;
mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
}
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.
-
- */
-
}
}
}
}
/**
- * 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
- * @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) const
-{
+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_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
+ break;
+ if (processset == NULL)
+ processset = new SnapVector<ModelAction *>();
+ processset->push_back(rf);
+ }
- 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 */
- };
- ASSERT(rf); // Needs to be real write
-
- 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);
-
- return true; /* complete */
-}
-
-/**
- * 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();
+ int i = (processset == NULL) ? 0 : processset->size();
- release_seq_heads(rf, release_heads);
+ 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());
+ }
+ rf->set_rfcv(vec);
+ }
+ i--;
+ if (i >= 0) {
+ rf = (*processset)[i];
+ } else
+ break;
+ }
+ if (processset != NULL)
+ delete processset;
+ return vec;
}
/**
}
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())
vec->resize(priv->next_thread_id);
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());
*/
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) {
ModelAction *act = *rit;
/* Only consider 'write' actions */
- if (!act->is_write() || act == curr)
+ if (!act->is_write()) {
+ if (act != curr && act->is_read() && act->happens_before(curr)) {
+ ModelAction *tmp = act->get_reads_from();
+ if (((unsigned int) id_to_int(tmp->get_tid()))==i)
+ act = tmp;
+ else
+ break;
+ } else
+ continue;
+ }
+
+ if (act == curr)
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
/**
* @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;
/* Do not split atomic RMW */
if (curr->is_rmwr())
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);
- default:
- 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)
projects / c11tester.git / blobdiff