next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
bugs(),
- bad_synchronization(false),
asserted(false)
{ }
modelclock_t used_sequence_numbers;
SnapVector<bug_message *> bugs;
/** @brief Incorrectly-ordered synchronization was made */
- bool bad_synchronization;
bool asserted;
SNAPSHOTALLOC
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
add_thread(model_thread);
- scheduler->register_engine(this);
fuzzer->register_engine(m->get_history(), this);
+ scheduler->register_engine(this);
}
/** @brief Destructor */
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;
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);
+ }
}
}
}
-/** @brief Alert the model-checker that an incorrectly-ordered
- * synchronization was made */
-void ModelExecution::set_bad_synchronization()
-{
- priv->bad_synchronization = true;
-}
-
-bool ModelExecution::assert_bug(const char *msg)
+void ModelExecution::assert_bug(const char *msg)
{
priv->bugs.push_back(new bug_message(msg));
-
- if (isfeasibleprefix()) {
- set_assert();
- return true;
- }
- return false;
+ set_assert();
}
/** @return True, if any bugs have been reported for this execution */
rf_set->push_back(nonatomicstore);
}
+ // Remove writes that violate read modification order
+ uint i = 0;
+ while (i < rf_set->size()) {
+ ModelAction * rf = (*rf_set)[i];
+ if (!r_modification_order(curr, rf, NULL, NULL, true)) {
+ (*rf_set)[i] = rf_set->back();
+ rf_set->pop_back();
+ } else
+ i++;
+ }
+
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
- if (index == -1) // no feasible write exists
- return false;
ModelAction *rf = (*rf_set)[index];
}
return true;
}
+
+ ASSERT(false);
+ /* TODO: Following code not needed anymore */
priorset->clear();
(*rf_set)[index] = rf_set->back();
rf_set->pop_back();
case THREAD_START: {
break;
}
+ case THREAD_SLEEP: {
+ Thread *th = get_thread(curr);
+ th->set_pending(curr);
+ scheduler->add_sleep(th);
+ break;
+ }
default:
break;
}
bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
{
if (*second < *first) {
- set_bad_synchronization();
+ ASSERT(0); //This should not happend
return false;
}
return second->synchronize_with(first);
wake_up_sleeping_actions(curr);
/* Add uninitialized actions to lists */
- if (!second_part_of_rmw && curr->get_type() != NOOP)
+ if (!second_part_of_rmw)
add_uninit_action_to_lists(curr);
SnapVector<ModelAction *> * rf_set = NULL;
rf_set = build_may_read_from(curr);
if (curr->is_read() && !second_part_of_rmw) {
- bool success = process_read(curr, rf_set);
+ process_read(curr, rf_set);
delete rf_set;
- if (!success)
- return curr; // Do not add action to lists
} else
ASSERT(rf_set == NULL);
/* Add the action to lists */
- if (!second_part_of_rmw && curr->get_type() != NOOP)
+ if (!second_part_of_rmw)
add_action_to_lists(curr);
if (curr->is_write())
return curr;
}
-/**
- * This is the strongest feasibility check available.
- * @return whether the current trace (partial or complete) must be a prefix of
- * a feasible trace.
- */
-bool ModelExecution::isfeasibleprefix() const
-{
- return !is_infeasible();
-}
-
-/**
- * Print disagnostic information about an infeasible execution
- * @param prefix A string to prefix the output with; if NULL, then a default
- * message prefix will be provided
- */
-void ModelExecution::print_infeasibility(const char *prefix) const
-{
- char buf[100];
- char *ptr = buf;
- if (priv->bad_synchronization)
- ptr += sprintf(ptr, "[bad sw ordering]");
- if (ptr != buf)
- model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
-}
-
-/**
- * Check if the current partial trace is infeasible. Does not check any
- * end-of-execution flags, which might rule out the execution. Thus, this is
- * useful only for ruling an execution as infeasible.
- * @return whether the current partial trace is infeasible.
- */
-bool ModelExecution::is_infeasible() const
-{
- return priv->bad_synchronization;
-}
-
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
ModelAction * ModelExecution::process_rmw(ModelAction *act) {
ModelAction *lastread = get_last_action(act->get_tid());
*
* @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
*/
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
+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;
*act < *last_sc_fence_thread_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 4 */
*act < *last_sc_fence_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 6 */
*act < *last_sc_fence_thread_before) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
break;
}
}
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
- priorset->push_back(act);
+ if (!check_only)
+ priorset->push_back(act);
} else {
const ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
- priorset->push_back(prevrf);
+ if (!check_only)
+ priorset->push_back(prevrf);
} else {
if (act->get_tid() == curr->get_tid()) {
//Can prune curr from obj list
- *canprune = true;
+ if (!check_only)
+ *canprune = true;
}
}
}
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++) {
+ for(int i = oldsize;i < uninit_id + 1;i++) {
new (&(*vec)[i]) action_list_t();
}
}
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++)
+ for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
if (uninit)
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++)
+ for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
(*vec)[tid].push_back(act);
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++)
+ for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
(*vec)[tid].push_back(act);
#endif
model_print("Execution trace %d:", get_execution_number());
- if (isfeasibleprefix()) {
- if (scheduler->all_threads_sleeping())
- model_print(" SLEEP-SET REDUNDANT");
- if (have_bug_reports())
- model_print(" DETECTED BUG(S)");
- } else
- print_infeasibility(" INFEASIBLE");
+ if (scheduler->all_threads_sleeping())
+ model_print(" SLEEP-SET REDUNDANT");
+ if (have_bug_reports())
+ model_print(" DETECTED BUG(S)");
+
model_print("\n");
print_list(&action_trace);
projects / c11tester.git / blobdiff