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
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());
add_thread(model_thread);
- scheduler->register_engine(this);
fuzzer->register_engine(m->get_history(), this);
+ scheduler->register_engine(this);
+#ifdef TLS
+ pthread_key_create(&pthreadkey, tlsdestructor);
+#endif
}
/** @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;
/* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
if (thr->get_pending()->is_sleep())
- thr->set_pending(NULL);
+ 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 */
}
// Remove writes that violate read modification order
- for (uint i = 0; i < rf_set->size(); i++) {
+ 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();
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);
if (curr->is_read() && !second_part_of_rmw) {
process_read(curr, rf_set);
delete rf_set;
-
-/* 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);
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());
* @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 check_only)
+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;
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()) {
+ SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ if (objvec->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++) {
+ 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)
void ModelExecution::add_action_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->push_back(act);
+ if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->push_back(act);
+ }
// Update action trace, a total order of all actions
action_trace.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);
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);
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()) {
#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