Fix yield bug
authorbdemsky <bdemsky@uci.edu>
Tue, 20 Dec 2016 07:59:45 +0000 (23:59 -0800)
committerbdemsky <bdemsky@uci.edu>
Tue, 20 Dec 2016 08:00:49 +0000 (00:00 -0800)
benchmarks/satcheck-precompiled/dekker/dekker-fences.c
benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c
classlist.h
constgen.cc
constgen.h
doc/README.txt
main.cc
params.h
schedulebuilder.cc

index ac796c9..4689860 100644 (file)
@@ -136,7 +136,9 @@ MC2_exitLoop();
                        // 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();
 
index 15a6d2c..6f26031 100644 (file)
@@ -85,6 +85,8 @@ void p1() {
                        
                        store_32(&flag1, true);
                        // std::atomic_thread_fence(std::memory_order_seq_cst);
+               } else {
+                       MC2_yield();
                }
        }
 
index 637e7f1..cd3b258 100644 (file)
@@ -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 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
index 4f4ec3a..82042af 100644 (file)
@@ -38,6 +38,7 @@ ConstGen::ConstGen(MCExecution *e) :
        rpt(new RecPairTable()),
        numconstraints(0),
        goalset(new ModelVector<Constraint *>()),
+       yieldlist(new ModelVector<EPRecord *>()),
        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()),
+       incompleteexploredbranch(new RecordSet()),
        execcondtable(new LoadHashTable()),
        solver(NULL),
        rectoint(new RecToIntTable()),
+       yieldtable(new RecToConsTable()),
        varindex(1),
        schedule_graph(0),
        has_untaken_branches(false)
@@ -80,14 +83,17 @@ ConstGen::~ConstGen() {
        delete threadactions;
        delete rpt;
        delete goalset;
+       delete yieldlist;
        delete vars;
        delete branchtable;
        delete functiontable;
        delete equalstable;
        delete schedulebuilder;
        delete nonlocaltrans;
+       delete incompleteexploredbranch;
        delete execcondtable;
        delete rectoint;
+       delete yieldtable;
 }
 
 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
@@ -128,8 +134,11 @@ void ConstGen::reset() {
        rpt->resetanddelete();
        resetstoreloadtable(storeloadtable);
        nonlocaltrans->reset();
+       incompleteexploredbranch->reset();
        threadactions->clear();
        rectoint->reset();
+       yieldtable->reset();
+       yieldlist->clear();
        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 */
-       if (numvalue<record->getLen())
+       if (numvalue<record->getLen()) {
                numvalue++;
+               if (model->params.noexecyields) {
+                       incompleteexploredbranch->add(record);
+               }
+       }
        /** 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);
 }
 
+/** **/
+
+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) {
-       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
 
+/** processRecord performs actions on second traversal of event
+               graph. */
+
 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:
@@ -1890,6 +1980,9 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
                if (record->getType()==NONLOCALTRANS) {
                        return;
                }
+               if (record->getType()==YIELD && model->params.noexecyields) {
+                       return;
+               }
                if (record->getType()==LOOPEXIT) {
                        return;
                }
index 8669a7f..20420bc 100644 (file)
@@ -115,7 +115,8 @@ private:
        void processLoad(EPRecord *record);
        void processAddresses(EPRecord *record);
        void recordExecCond(EPRecord *record);
-
+       void computeYieldCond(EPRecord *record);
+       
        /** TSO Specific methods */
 #ifdef TSO
        void genTSOTransOrderConstraints();
@@ -148,6 +149,7 @@ private:
        RecPairTable *rpt;
        uint numconstraints;
        ModelVector<Constraint *> * goalset;
+       ModelVector<EPRecord *> *yieldlist;
        Constraint ** goalvararray;
        ModelVector<Constraint *> * vars;
        BranchTable * branchtable;
@@ -155,9 +157,11 @@ private:
        EqualsTable *equalstable;
        ScheduleBuilder *schedulebuilder;
        RecordSet *nonlocaltrans;
+       RecordSet *incompleteexploredbranch;
        LoadHashTable *execcondtable;
        IncrementalSolver *solver;
        RecToIntTable *rectoint;
+       RecToConsTable *yieldtable;
 #ifdef STATS
        ModelVector<struct MC_Stat *> * stats;
 #endif
index ddb8763..4f06337 100644 (file)
@@ -42,3 +42,8 @@ handle SIGBUS 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 48ec61f..2b619a6 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -27,7 +27,7 @@
 static void param_defaults(struct model_params *params)
 {
        params->branches = false;
-       params->noyields = false;
+       params->noexecyields = false;
        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->noyields = true;
+                       params->noexecyields = true;
                        break;
                case 'v':
                        params->verbose = optarg ? atoi(optarg) : 1;
index 78cedcb..7f2e3cf 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 Avoid executiny yields. */
-       bool noyields;
+       /** @brief Avoid executing yields. */
+       bool noexecyields;
 
        /** @brief Only explore branches. */
        bool branches;
index 3bc6e96..6cf4b5a 100644 (file)
@@ -13,6 +13,7 @@
 #include "constgen.h"
 #include "branchrecord.h"
 #include "storeloadset.h"
+#include "model.h"
 
 ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
        cg(cgen),
@@ -215,6 +216,8 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
        case LABEL:
                break;
        case YIELD:
+               if (model->params.noexecyields)
+                       return NULL;
                break;
        default:
                ASSERT(0);