schedule: drop the ModelChecker::check_promises_thread_disabled interface

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 83a82275098d3a6b6e9ebd2b7f03cb1999cec27e..01c53cdc677cb21d2ab152efb1e8a3897ae27ebc 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -2,8 +2,11 @@
 #include "action.h"
 #include "threads-model.h"
 #include "clockvector.h"
+#include "execution.h"
 
-SCAnalysis::SCAnalysis() {
+SCAnalysis::SCAnalysis(const ModelExecution *execution) :
+       execution(execution)
+{
        cvmap=new HashTable<const ModelAction *, ClockVector *, uintptr_t, 4>();
        cycleset=new HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4>();
        threadlists=new SnapVector<action_list_t>(1);
@@ -65,10 +68,35 @@ ModelAction * SCAnalysis::getNextAction() {
                        act=first;
                }
        }
+       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;
+                       }
+               }
+       }
+
+       //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();
+               }
+       }
+
        return act;
 }
 
-action_list_t * SCAnalysis::generateSC(action_list_t *list) {  
+action_list_t * SCAnalysis::generateSC(action_list_t *list) {
        action_list_t *sclist=new action_list_t();
        while (true) {
                ModelAction * act=getNextAction();
@@ -123,7 +151,7 @@ bool SCAnalysis::updateConstraints(ModelAction *act) {
                                changed=true;
                                break;
                        }
-               }               
+               }
        }
        return changed;
 }
@@ -134,7 +162,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
        /* Merge in the clock vector from the write */
        const ModelAction *write=read->get_reads_from();
        ClockVector *writecv=cvmap->get(write);
-       changed|= ( writecv == NULL || merge(cv, read, writecv) && (*read < *write));
+       changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write));
 
        for(int i=0;i<=maxthreads;i++) {
                thread_id_t tid=int_to_id(i);
@@ -142,7 +170,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
                        continue;
                if (tid==write->get_tid())
                        continue;
-               action_list_t * list=model->get_actions_on_obj(read->get_location(), tid);
+               action_list_t * list=execution->get_actions_on_obj(read->get_location(), tid);
                if (list==NULL)
                        continue;
                for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
@@ -153,14 +181,14 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
                        ClockVector *write2cv = cvmap->get(write2);
                        if (write2cv == NULL)
                                continue;
-                       
+
                        /* write -sc-> write2 &&
                                 write -rf-> R =>
                                 R -sc-> write2 */
                        if (write2cv->synchronized_since(write)) {
                                changed |= merge(write2cv, write2, cv);
                        }
-               
+
                        //looking for earliest write2 in iteration to satisfy this
                        /* write2 -sc-> R &&
                                 write -rf-> R =>
@@ -187,7 +215,7 @@ void SCAnalysis::computeCV(action_list_t *list) {
                        ModelAction *act = *it;
                        ModelAction *lastact = last_act[id_to_int(act->get_tid())];
                        if (act->is_thread_start())
-                               lastact=model->get_thread(act)->get_creation();
+                               lastact=execution->get_thread(act)->get_creation();
                        ClockVector *lastcv=(lastact != NULL) ? cvmap->get(lastact) : NULL;
                        last_act[id_to_int(act->get_tid())]=act;
                        ClockVector *cv=cvmap->get(act);
@@ -199,16 +227,10 @@ void SCAnalysis::computeCV(action_list_t *list) {
                        }
                        if (act->is_thread_join()) {
                                Thread *joinedthr = act->get_thread_operand();
-                               ModelAction *finish = model->get_last_action(joinedthr->get_id());
+                               ModelAction *finish = execution->get_last_action(joinedthr->get_id());
                                ClockVector *finishcv = cvmap->get(finish);
                                changed |= (finishcv == NULL) || merge(cv, act, finishcv);
                        }
-                       if (act->is_thread_join()) {
-                               Thread *joinedthr = act->get_thread_operand();
-                               ModelAction *finish = model->get_last_action(joinedthr->get_id());
-                               ClockVector *finishcv = cvmap->get(finish);
-                               changed |= (finishcv == NULL) || cv->merge(finishcv);
-                       }
                        if (act->is_read()) {
                                changed|=processRead(act, cv);
                        }