used_sequence_numbers(0),
bugs(),
bad_synchronization(false),
- bad_sc_read(false),
asserted(false)
{ }
SnapVector<bug_message *> bugs;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
- bool bad_sc_read;
bool asserted;
SNAPSHOTALLOC
};
/** @brief Constructor */
-ModelExecution::ModelExecution(ModelChecker *m,
- Scheduler *scheduler,
- NodeStack *node_stack) :
+ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
model(m),
params(NULL),
scheduler(scheduler),
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 */
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()
{
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));
* @param rf_set is the set of model actions we can possibly read from
* @return True if processing this read updates the mo_graph.
*/
-bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
+void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
{
+ SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
ASSERT(rf);
-
- mo_graph->startChanges();
- bool updated = r_modification_order(curr, rf);
- if (!is_infeasible()) {
+ 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);
- mo_graph->commitChanges();
get_thread(curr)->set_return_value(curr->get_return_value());
- return updated;
+ 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;
}
- mo_graph->rollbackChanges();
+ priorset->clear();
(*rf_set)[index] = rf_set->back();
rf_set->pop_back();
}
}
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;
}
* @param curr The ModelAction to process
* @return True if the mo_graph was updated or promises were resolved
*/
-bool ModelExecution::process_write(ModelAction *curr)
+void ModelExecution::process_write(ModelAction *curr)
{
- bool updated_mod_order = w_modification_order(curr);
+ w_modification_order(curr);
- mo_graph->commitChanges();
get_thread(curr)->set_return_value(VALUE_NONE);
- return updated_mod_order;
}
/**
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);
- ModelVector<ModelAction *> * rf_set = NULL;
+ SnapVector<const ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
rf_set = build_may_read_from(curr);
{
char buf[100];
char *ptr = buf;
- if (mo_graph->checkForCycles())
- ptr += sprintf(ptr, "[mo cycle]");
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->bad_synchronization ||
- priv->bad_sc_read;
+ return priv->bad_synchronization;
}
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
lastread->process_rmw(act);
if (act->is_rmw()) {
mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
- mo_graph->commitChanges();
}
return lastread;
}
* @param rf The ModelAction or Promise that curr reads from. Must be a write.
* @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)
{
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 */
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;
/* 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;
+ 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;
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ 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;
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ 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 < *prev_same_thread)) {
+ prev_same_thread = act;
+ }
+ }
if (act->is_write()) {
- added = mo_graph->addEdge(act, rf) || added;
+ if (mo_graph->checkReachable(rf, act))
+ return false;
+ 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;
+ priorset->push_back(prevrf);
+ } else {
+ if (act->get_tid() == curr->get_tid()) {
+ //Can prune curr from obj list
+ *canprune = true;
+ }
+ }
}
break;
}
}
}
-
- 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());
if (curr->is_seqcst()) {
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;
+ mo_graph->addEdge(last_seq_cst, curr);
}
}
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
+ bool force_edge = false;
for (rit = list->rbegin();rit != list->rend();rit++) {
ModelAction *act = *rit;
if (act == curr) {
* 3) If normal write, we need to look at earlier actions, so
* continue processing list.
*/
+ force_edge = true;
if (curr->is_rmw()) {
if (curr->get_reads_from() != NULL)
break;
/* 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;
+ mo_graph->addEdge(act, curr, force_edge);
break;
}
* readfrom(act) --mo--> act
*/
if (act->is_write())
- added = mo_graph->addEdge(act, curr) || added;
+ mo_graph->addEdge(act, curr, force_edge);
else if (act->is_read()) {
//if previous read accessed a null, just keep going
- added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+ mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
}
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&
}
}
}
-
- return added;
}
/**
* @return true, if the ModelExecution is certain that release_heads is complete;
* false otherwise
*/
-bool ModelExecution::release_seq_heads(const ModelAction *rf,
- rel_heads_list_t *release_heads) const
+bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) 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()) {
ASSERT(rf->is_write());
* @param curr is the current ModelAction that we are exploring; it must be a
* 'read' operation.
*/
-ModelVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
+SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
- ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();
+ SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
/* Iterate over all threads */
for (i = 0;i < thrd_lists->size();i++) {
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin();rit != list->rend();rit++) {
- ModelAction *act = *rit;
+ const 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)) {
+ const 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. */
}
if (allow_read) {
- /* Only add feasible reads */
- rf_set->push_back(act);
+ /* Only add feasible reads */
+ rf_set->push_back(act);
}
/* Include at most one act per-thread that "happens before" curr */
projects / c11tester.git / blobdiff