ModelAction * SCAnalysis::getNextAction() {
ModelAction *act = NULL;
+ /* Find the earliest in SC ordering */
for (int i = 0; i <= maxthreads; i++) {
action_list_t *threadlist = &threadlists[i];
if (threadlist->empty())
continue;
ModelAction *first = threadlist->front();
- if (act == NULL) {
- act = first;
+ if (act==NULL) {
+ act=first;
continue;
}
ClockVector *cv = cvmap.get(act);
}
if (act == NULL)
return act;
- //print cycles in a nice way to avoid confusion
- //make sure thread starts appear after the create
- if (act->is_thread_start()) {
- ModelAction *createact = execution->get_thread(act)->get_creation();
- if (createact) {
- action_list_t *threadlist = &threadlists[id_to_int(createact->get_tid())];
- if (!threadlist->empty()) {
- ModelAction *first = threadlist->front();
- if (first->get_seq_number() <= createact->get_seq_number())
- act = first;
- }
+
+
+ /* Find the model action with the earliest sequence number in case of a cycle.
+ */
+
+ for (int i = 0; i <= maxthreads; i++) {
+ action_list_t *threadlist = &threadlists[i];
+ if (threadlist->empty())
+ continue;
+ ModelAction *first = threadlist->front();
+ ClockVector *cv = cvmap.get(act);
+ ClockVector *cvfirst = cvmap.get(first);
+ if (first->get_seq_number()<act->get_seq_number()&&
+ (cv->synchronized_since(first)||!cvfirst->synchronized_since(act))) {
+ act=first;
}
}
- //make sure that joins appear after the thread is finished
- if (act->is_thread_join()) {
- int jointhread = id_to_int(act->get_thread_operand()->get_id());
- action_list_t *threadlist = &threadlists[jointhread];
- if (!threadlist->empty()) {
- act = threadlist->front();
+ /* See if hb demands an earlier action. */
+ for (int i = 0; i <= maxthreads; i++) {
+ action_list_t *threadlist = &threadlists[i];
+ if (threadlist->empty())
+ continue;
+ ModelAction *first = threadlist->front();
+ ClockVector *cv = act->get_cv();
+ if (cv->synchronized_since(first)) {
+ act = first;
}
}
-
return act;
}