#define INITIAL_THREAD_ID 0
+#ifdef COLLECT_STAT
+static unsigned int atomic_load_count = 0;
+static unsigned int atomic_store_count = 0;
+static unsigned int atomic_rmw_count = 0;
+
+static unsigned int atomic_fence_count = 0;
+static unsigned int atomic_lock_count = 0;
+static unsigned int atomic_trylock_count = 0;
+static unsigned int atomic_unlock_count = 0;
+static unsigned int atomic_notify_count = 0;
+static unsigned int atomic_wait_count = 0;
+static unsigned int atomic_timedwait_count = 0;
+#endif
+
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
* action lists may change. Hence we need to fix the parent pointer of the children
* of root.
*/
-static void fixup_action_list (SnapVector<action_list_t> * vec)
+static void fixup_action_list(SnapVector<action_list_t> * vec)
{
- for (uint i = 0; i < vec->size(); i++) {
+ for (uint i = 0;i < vec->size();i++) {
action_list_t * list = &(*vec)[i];
if (list != NULL)
list->fixupParent();
}
}
+#ifdef COLLECT_STAT
+static inline void record_atomic_stats(ModelAction * act)
+{
+ switch (act->get_type()) {
+ case ATOMIC_WRITE:
+ atomic_store_count++;
+ break;
+ case ATOMIC_RMW:
+ atomic_load_count++;
+ break;
+ case ATOMIC_READ:
+ atomic_rmw_count++;
+ break;
+ case ATOMIC_FENCE:
+ atomic_fence_count++;
+ break;
+ case ATOMIC_LOCK:
+ atomic_lock_count++;
+ break;
+ case ATOMIC_TRYLOCK:
+ atomic_trylock_count++;
+ break;
+ case ATOMIC_UNLOCK:
+ atomic_unlock_count++;
+ break;
+ case ATOMIC_NOTIFY_ONE:
+ case ATOMIC_NOTIFY_ALL:
+ atomic_notify_count++;
+ break;
+ case ATOMIC_WAIT:
+ atomic_wait_count++;
+ break;
+ case ATOMIC_TIMEDWAIT:
+ atomic_timedwait_count++;
+ default:
+ return;
+ }
+}
+
+void print_atomic_accesses()
+{
+ model_print("atomic store count: %u\n", atomic_store_count);
+ model_print("atomic load count: %u\n", atomic_load_count);
+ model_print("atomic rmw count: %u\n", atomic_rmw_count);
+
+ model_print("atomic fence count: %u\n", atomic_fence_count);
+ model_print("atomic lock count: %u\n", atomic_lock_count);
+ model_print("atomic trylock count: %u\n", atomic_trylock_count);
+ model_print("atomic unlock count: %u\n", atomic_unlock_count);
+ model_print("atomic notify count: %u\n", atomic_notify_count);
+ model_print("atomic wait count: %u\n", atomic_wait_count);
+ model_print("atomic timedwait count: %u\n", atomic_timedwait_count);
+}
+#endif
/** @return a thread ID for a new Thread */
thread_id_t ModelExecution::get_next_id()
{
void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
{
for (unsigned int i = 0;i < get_num_threads();i++) {
- Thread *thr = get_thread(int_to_id(i));
- if (scheduler->is_sleep_set(thr)) {
+ thread_id_t tid = int_to_id(i);
+ Thread *thr = get_thread(tid);
+ if (scheduler->is_sleep_set(tid)) {
if (should_wake_up(curr, thr)) {
/* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
/* remove old wait action and disable this thread */
simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
- for (sllnode<ModelAction *> * it = waiters->begin(); it != NULL; it = it->getNext()) {
+ for (sllnode<ModelAction *> * it = waiters->begin();it != NULL;it = it->getNext()) {
ModelAction * wait = it->getVal();
if (wait->get_tid() == curr->get_tid()) {
waiters->erase(it);
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
- break; // WL: to be add (modified)
+ break;
}
case THREADONLY_FINISH:
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
ASSERT(curr);
- bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
bool newly_explored = initialize_curr_action(&curr);
DBG();
wake_up_sleeping_actions(curr);
SnapVector<ModelAction *> * rf_set = NULL;
+ bool canprune = false;
/* Build may_read_from set for newly-created actions */
- if (newly_explored && curr->is_read())
+ if (curr->is_read() && newly_explored) {
rf_set = build_may_read_from(curr);
-
- bool canprune = false;
-
- if (curr->is_read() && !second_part_of_rmw) {
canprune = process_read(curr, rf_set);
delete rf_set;
} else
ASSERT(rf_set == NULL);
- /* Add the action to lists */
- if (!second_part_of_rmw)
+ /* Add the action to lists if not the second part of a rmw */
+ if (newly_explored) {
+#ifdef COLLECT_STAT
+ record_atomic_stats(curr);
+#endif
add_action_to_lists(curr, canprune);
+ }
if (curr->is_write())
add_write_to_lists(curr);
*/
bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
- SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
+ SnapVector<ModelAction *> * priorset, bool * canprune)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
ASSERT(curr->is_read());
*act < *last_sc_fence_thread_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
break;
}
/* C++, Section 29.3 statement 4 */
*act < *last_sc_fence_local) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ 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;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
break;
}
}
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
- if (!check_only)
- priorset->push_back(act);
+ priorset->push_back(act);
} else {
ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
- if (!check_only)
- priorset->push_back(prevrf);
+ priorset->push_back(prevrf);
} else {
if (act->get_tid() == curr->get_tid()) {
//Can prune curr from obj list
- if (!check_only)
- *canprune = true;
+ *canprune = true;
}
}
}
}
-/**
- * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
- * some constraints. This method checks one the following constraint (others
- * require compiler support):
- *
- * If X --hb-> Y --mo-> Z, then X should not read from Z.
- * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
- */
-bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
-{
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
- unsigned int i;
- /* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++) {
- const ModelAction *write_after_read = NULL;
-
- /* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
- sllnode<ModelAction *>* rit;
- for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
- ModelAction *act = rit->getVal();
-
- /* Don't disallow due to act == reader */
- if (!reader->happens_before(act) || reader == act)
- break;
- else if (act->is_write())
- write_after_read = act;
- else if (act->is_read() && act->get_reads_from() != NULL)
- write_after_read = act->get_reads_from();
- }
-
- if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
- return false;
- }
- return true;
-}
-
/**
* Computes the clock vector that happens before propagates from this write.
*
//operation that isn't release
if (rf->get_last_fence_release()) {
if (vec == NULL)
- vec = rf->get_last_fence_release()->get_cv();
+ vec = new ClockVector(rf->get_last_fence_release()->get_cv(), NULL);
else
(vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
+ } else {
+ if (vec == NULL) {
+ if (rf->is_rmw()) {
+ vec = new ClockVector(NULL, NULL);
+ }
+ } else {
+ vec = new ClockVector(vec, NULL);
+ }
}
rf->set_rfcv(vec);
}
//Thread 0 isn't a real thread, so skip it..
for(unsigned int i = 1;i < thread_map.size();i++) {
Thread * t = thread_map[i];
- if (t->get_state() == THREAD_COMPLETED)
+ if (t->is_complete())
continue;
thread_id_t tid = int_to_id(i);
ClockVector * cv = get_cv(tid);