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),
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_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;
}
* @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