Fix yield bug

diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences.c
index ac796c973b934cbf0ac3f1ae774a6fdf2fee91dd..46898604050c10de35e62546ee797b6be53b7d7c 100644 (file)
--- a/benchmarks/satcheck-precompiled/dekker/dekker-fences.c
+++ b/benchmarks/satcheck-precompiled/dekker/dekker-fences.c
@@ -136,7 +136,9 @@ MC2_exitLoop();
                        // std::atomic_thread_fence(std::memory_order_seq_cst);
                        MC2_merge(_br4);
                }
                        // std::atomic_thread_fence(std::memory_order_seq_cst);
                        MC2_merge(_br4);
                }

- else { _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true); MC2_merge(_br4);
+ else { _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true);
+                       MC2_yield();
+        MC2_merge(_br4);

         }      }
 MC2_exitLoop();
 
         }      }
 MC2_exitLoop();
 

diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c
index 15a6d2c539f1cd59629c0e4f90d892d7339b40b5..6f2603120a0466de4486cb6261d61ebbacd2f578 100644 (file)
--- a/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c
+++ b/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c
@@ -85,6 +85,8 @@ void p1() {
                        
                        store_32(&flag1, true);
                        // std::atomic_thread_fence(std::memory_order_seq_cst);
                        
                        store_32(&flag1, true);
                        // std::atomic_thread_fence(std::memory_order_seq_cst);

+               } else {
+                       MC2_yield();

                }
        }
 
                }
        }
 

diff --git a/classlist.h b/classlist.h
index 637e7f14efb88736c04e664cd3fa74345b8f148c..cd3b25888d15c69ea6706ed558f64afcecbdfa47 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -51,6 +51,7 @@ typedef HSIterator<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free
 typedef HashSet<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> SnapIntHashSet;
 typedef HSIterator<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> SnapIntIterator;
 typedef HashTable<EPRecord *, Constraint **, uintptr_t, 4, model_malloc, model_calloc, model_free> VarTable;
 typedef HashSet<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> SnapIntHashSet;
 typedef HSIterator<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> SnapIntIterator;
 typedef HashTable<EPRecord *, Constraint **, uintptr_t, 4, model_malloc, model_calloc, model_free> VarTable;

+typedef HashTable<EPRecord *, Constraint *, uintptr_t, 4, model_malloc, model_calloc, model_free> RecToConsTable;

 typedef HashTable<EPRecord *, FunctionRecord *, uintptr_t, 4, model_malloc, model_calloc, model_free> FunctionTable;
 typedef HashTable<EPRecord *, EqualsRecord *, uintptr_t, 4, model_malloc, model_calloc, model_free> EqualsTable;
 #endif
 typedef HashTable<EPRecord *, FunctionRecord *, uintptr_t, 4, model_malloc, model_calloc, model_free> FunctionTable;
 typedef HashTable<EPRecord *, EqualsRecord *, uintptr_t, 4, model_malloc, model_calloc, model_free> EqualsTable;
 #endif

diff --git a/constgen.cc b/constgen.cc
index 4f4ec3a65bee2e42d0db39233fe0de5314335df1..82042af420bedfdd4b7b29c084f64aeeb33c081d 100644 (file)
--- a/constgen.cc
+++ b/constgen.cc
@@ -38,6 +38,7 @@ ConstGen::ConstGen(MCExecution *e) :
        rpt(new RecPairTable()),
        numconstraints(0),
        goalset(new ModelVector<Constraint *>()),
        rpt(new RecPairTable()),
        numconstraints(0),
        goalset(new ModelVector<Constraint *>()),

+       yieldlist(new ModelVector<EPRecord *>()),

        goalvararray(NULL),
        vars(new ModelVector<Constraint *>()),
        branchtable(new BranchTable()),
        goalvararray(NULL),
        vars(new ModelVector<Constraint *>()),
        branchtable(new BranchTable()),


@@ -45,9 +46,11 @@ ConstGen::ConstGen(MCExecution *e) :
        equalstable(new EqualsTable()),
        schedulebuilder(new ScheduleBuilder(e, this)),
        nonlocaltrans(new RecordSet()),
        equalstable(new EqualsTable()),
        schedulebuilder(new ScheduleBuilder(e, this)),
        nonlocaltrans(new RecordSet()),

+       incompleteexploredbranch(new RecordSet()),

        execcondtable(new LoadHashTable()),
        solver(NULL),
        rectoint(new RecToIntTable()),
        execcondtable(new LoadHashTable()),
        solver(NULL),
        rectoint(new RecToIntTable()),

+       yieldtable(new RecToConsTable()),

        varindex(1),
        schedule_graph(0),
        has_untaken_branches(false)
        varindex(1),
        schedule_graph(0),
        has_untaken_branches(false)


@@ -80,14 +83,17 @@ ConstGen::~ConstGen() {
        delete threadactions;
        delete rpt;
        delete goalset;
        delete threadactions;
        delete rpt;
        delete goalset;

+       delete yieldlist;

        delete vars;
        delete branchtable;
        delete functiontable;
        delete equalstable;
        delete schedulebuilder;
        delete nonlocaltrans;
        delete vars;
        delete branchtable;
        delete functiontable;
        delete equalstable;
        delete schedulebuilder;
        delete nonlocaltrans;

+       delete incompleteexploredbranch;

        delete execcondtable;
        delete rectoint;
        delete execcondtable;
        delete rectoint;

+       delete yieldtable;

 }
 
 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
 }
 
 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {


@@ -128,8 +134,11 @@ void ConstGen::reset() {
        rpt->resetanddelete();
        resetstoreloadtable(storeloadtable);
        nonlocaltrans->reset();
        rpt->resetanddelete();
        resetstoreloadtable(storeloadtable);
        nonlocaltrans->reset();

+       incompleteexploredbranch->reset();

        threadactions->clear();
        rectoint->reset();
        threadactions->clear();
        rectoint->reset();

+       yieldtable->reset();
+       yieldlist->clear();

        goalset->clear();
        varindex=1;
        numconstraints=0;
        goalset->clear();
        varindex=1;
        numconstraints=0;


@@ -1138,8 +1147,12 @@ bool ConstGen::isAlwaysExecuted(EPRecord *record) {
 void ConstGen::insertBranch(EPRecord *record) {
        uint numvalue=record->numValues();
        /** need one value for new directions */
 void ConstGen::insertBranch(EPRecord *record) {
        uint numvalue=record->numValues();
        /** need one value for new directions */

-       if (numvalue<record->getLen())
+       if (numvalue<record->getLen()) {

                numvalue++;
                numvalue++;

+               if (model->params.noexecyields) {
+                       incompleteexploredbranch->add(record);
+               }
+       }

        /** need extra value to represent that branch wasn't executed. **/
        bool alwaysexecuted=isAlwaysExecuted(record);
        if (!alwaysexecuted)
        /** need extra value to represent that branch wasn't executed. **/
        bool alwaysexecuted=isAlwaysExecuted(record);
        if (!alwaysexecuted)


@@ -1471,13 +1484,84 @@ void ConstGen::processStore(EPRecord *record) {
        processAddresses(record);
 }
 
        processAddresses(record);
 }
 

+/** **/
+
+void ConstGen::computeYieldCond(EPRecord *record) {
+       ExecPoint *yieldep=record->getEP();
+       EPRecord *prevyield=NULL;
+       ExecPoint *prevyieldep=NULL;
+       
+       for(int i=(int)(yieldlist->size()-1);i>=0;i--) {
+               EPRecord *tmpyield=(*yieldlist)[i];
+               ExecPoint *tmpep=tmpyield->getEP();
+               //Do we have a previous yield operation
+               if (yieldep->compare(tmpep)==CR_BEFORE) {
+                       //Yes
+                       prevyield=tmpyield;
+                       prevyieldep=prevyield->getEP();
+                       break;
+               }
+       }
+       
+       yieldlist->push_back(record);
+
+       ModelVector<Constraint *> * novel_branches=new ModelVector<Constraint *>();
+       RecordIterator *sri=incompleteexploredbranch->iterator();
+       while(sri->hasNext()) {
+               EPRecord * unexploredbranch=sri->next();
+               ExecPoint * branchep=unexploredbranch->getEP();
+               if (yieldep->compare(branchep)!=CR_BEFORE) {
+                       //Branch does not occur before yield, so skip
+                       continue;
+               }
+
+               //See if the previous yield already accounts for this branch
+               if (prevyield != NULL &&
+                               prevyieldep->compare(branchep)==CR_BEFORE) {
+                       //Branch occurs before previous yield, so we can safely skip this branch
+                                               continue;
+               }
+
+               //This is a branch that could prevent this yield from being executed
+               BranchRecord *br=branchtable->get(unexploredbranch);
+               Constraint * novel_branch=br->getNewBranch();
+               novel_branches->push_back(novel_branch);
+       }
+
+       int num_constraints=((prevyield==NULL)?0:1)+novel_branches->size();
+       Constraint *carray[num_constraints];
+       int arr_index=0;
+       
+       if (prevyield!=NULL) {
+               carray[arr_index++]=yieldtable->get(prevyield);//get constraint for old yield
+       }
+       for(uint i=0;i<novel_branches->size();i++) {
+               carray[arr_index++]=(*novel_branches)[i];
+       }
+       
+       Constraint *cor=num_constraints!=0?new Constraint(OR, num_constraints, carray):&cfalse;
+
+       Constraint *var=getNewVar();
+       //If the variable is true, then we need to have taken some branch
+       //ahead of the yield
+       Constraint *implies=new Constraint(IMPLIES, var, cor);
+       ADDCONSTRAINT(implies, "possiblebranchnoyield");
+       yieldtable->put(record, var);
+       
+       delete novel_branches;
+       delete sri;
+}
+
+

 /** Handle yields by just forbidding them via the SAT formula. */
 
 void ConstGen::processYield(EPRecord *record) {
 /** Handle yields by just forbidding them via the SAT formula. */
 
 void ConstGen::processYield(EPRecord *record) {

-       if (model->params.noyields &&
-                       record->getBranch()!=NULL) {
-               Constraint * noyield=getExecutionConstraint(record)->negate();
-               ADDCONSTRAINT(noyield, "noyield");
+       if (model->params.noexecyields) {
+               computeYieldCond(record);
+               Constraint * noexecyield=getExecutionConstraint(record)->negate();
+               Constraint * branchaway=yieldtable->get(record);
+               Constraint * avoidbranch=new Constraint(OR, noexecyield, branchaway);
+               ADDCONSTRAINT(avoidbranch, "noexecyield");

        }
 }
 
        }
 }
 


@@ -1732,6 +1816,9 @@ void ConstGen::processFence(EPRecord *record) {
 }
 #endif
 
 }
 #endif
 

+/** processRecord performs actions on second traversal of event
+               graph. */
+

 void ConstGen::processRecord(EPRecord *record) {
        switch (record->getType()) {
        case FUNCTION:
 void ConstGen::processRecord(EPRecord *record) {
        switch (record->getType()) {
        case FUNCTION:


@@ -1775,6 +1862,9 @@ void ConstGen::processRecord(EPRecord *record) {
        }
 }
 
        }
 }
 

+/** visitRecord performs actions done on first traversal of event
+ *     graph. */
+

 void ConstGen::visitRecord(EPRecord *record) {
        switch (record->getType()) {
        case EQUALS:
 void ConstGen::visitRecord(EPRecord *record) {
        switch (record->getType()) {
        case EQUALS:


@@ -1890,6 +1980,9 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
                if (record->getType()==NONLOCALTRANS) {
                        return;
                }
                if (record->getType()==NONLOCALTRANS) {
                        return;
                }

+               if (record->getType()==YIELD && model->params.noexecyields) {
+                       return;
+               }

                if (record->getType()==LOOPEXIT) {
                        return;
                }
                if (record->getType()==LOOPEXIT) {
                        return;
                }

diff --git a/constgen.h b/constgen.h
index 8669a7f98bcc3aaa13e40c7c792d7c2c965e04d3..20420bc1bc601242f67b525503bf3457e963f61a 100644 (file)
--- a/constgen.h
+++ b/constgen.h
@@ -115,7 +115,8 @@ private:
        void processLoad(EPRecord *record);
        void processAddresses(EPRecord *record);
        void recordExecCond(EPRecord *record);
        void processLoad(EPRecord *record);
        void processAddresses(EPRecord *record);
        void recordExecCond(EPRecord *record);

-
+       void computeYieldCond(EPRecord *record);
+       

        /** TSO Specific methods */
 #ifdef TSO
        void genTSOTransOrderConstraints();
        /** TSO Specific methods */
 #ifdef TSO
        void genTSOTransOrderConstraints();


@@ -148,6 +149,7 @@ private:
        RecPairTable *rpt;
        uint numconstraints;
        ModelVector<Constraint *> * goalset;
        RecPairTable *rpt;
        uint numconstraints;
        ModelVector<Constraint *> * goalset;

+       ModelVector<EPRecord *> *yieldlist;

        Constraint ** goalvararray;
        ModelVector<Constraint *> * vars;
        BranchTable * branchtable;
        Constraint ** goalvararray;
        ModelVector<Constraint *> * vars;
        BranchTable * branchtable;


@@ -155,9 +157,11 @@ private:
        EqualsTable *equalstable;
        ScheduleBuilder *schedulebuilder;
        RecordSet *nonlocaltrans;
        EqualsTable *equalstable;
        ScheduleBuilder *schedulebuilder;
        RecordSet *nonlocaltrans;

+       RecordSet *incompleteexploredbranch;

        LoadHashTable *execcondtable;
        IncrementalSolver *solver;
        RecToIntTable *rectoint;
        LoadHashTable *execcondtable;
        IncrementalSolver *solver;
        RecToIntTable *rectoint;

+       RecToConsTable *yieldtable;

 #ifdef STATS
        ModelVector<struct MC_Stat *> * stats;
 #endif
 #ifdef STATS
        ModelVector<struct MC_Stat *> * stats;
 #endif

diff --git a/doc/README.txt b/doc/README.txt
index ddb8763c9ec22c975bd0ad15a1d695455cbd2c50..4f063373477404f0327d8a6cbc44aed75aab9d02 100644 (file)
--- a/doc/README.txt
+++ b/doc/README.txt
@@ -42,3 +42,8 @@ handle SIGBUS nostop noprint
 
 To run in Linux under gdb, use:
 handle SIGSEGV nostop noprint
 
 To run in Linux under gdb, use:
 handle SIGSEGV nostop noprint

+
+IV. Generating doxygen docs
+
+Type "make docs".
+Then look in doc/docs/.

diff --git a/main.cc b/main.cc
index 48ec61fc8f9535fbb2b7ee73d6672740ce41be7c..2b619a6debe4b5c0b9d715813780f47d0ed0adc6 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -27,7 +27,7 @@
 static void param_defaults(struct model_params *params)
 {
        params->branches = false;
 static void param_defaults(struct model_params *params)
 {
        params->branches = false;

-       params->noyields = false;
+       params->noexecyields = false;

        params->verbose = !!DBG_ENABLED();
 }
 
        params->verbose = !!DBG_ENABLED();
 }
 


@@ -67,7 +67,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                        params->branches = true;
                        break;
                case 'Y':
                        params->branches = true;
                        break;
                case 'Y':

-                       params->noyields = true;
+                       params->noexecyields = true;

                        break;
                case 'v':
                        params->verbose = optarg ? atoi(optarg) : 1;
                        break;
                case 'v':
                        params->verbose = optarg ? atoi(optarg) : 1;

diff --git a/params.h b/params.h
index 78cedcbc1d925249f9dbd43158109ab67d3c36e5..7f2e3cf6299fd4db469ca51a1a6c4060f7e6d70a 100644 (file)
--- a/params.h
+++ b/params.h
@@ -18,8 +18,8 @@ struct model_params {
        /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
        int verbose;
 
        /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
        int verbose;
 

-       /** @brief Avoid executiny yields. */
-       bool noyields;
+       /** @brief Avoid executing yields. */
+       bool noexecyields;

 
        /** @brief Only explore branches. */
        bool branches;
 
        /** @brief Only explore branches. */
        bool branches;

diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index 3bc6e96b2a729d6e1f0dac59922bf386901fa5d7..6cf4b5aae9598963b8e6a86b2fa6cf68c7319b78 100644 (file)
--- a/schedulebuilder.cc
+++ b/schedulebuilder.cc
@@ -13,6 +13,7 @@
 #include "constgen.h"
 #include "branchrecord.h"
 #include "storeloadset.h"
 #include "constgen.h"
 #include "branchrecord.h"
 #include "storeloadset.h"

+#include "model.h"

 
 ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
        cg(cgen),
 
 ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
        cg(cgen),


@@ -215,6 +216,8 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
        case LABEL:
                break;
        case YIELD:
        case LABEL:
                break;
        case YIELD:

+               if (model->params.noexecyields)
+                       return NULL;

                break;
        default:
                ASSERT(0);
                break;
        default:
                ASSERT(0);