From: bdemsky Date: Tue, 20 Dec 2016 07:59:45 +0000 (-0800) Subject: Fix yield bug X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satcheck.git;a=commitdiff_plain;h=bd644b5504a9bfc394bf245dc7a8579ebed9254a;ds=sidebyside Fix yield bug --- diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences.c index ac796c9..4689860 100644 --- 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); } - 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(); diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c index 15a6d2c..6f26031 100644 --- 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); + } else { + MC2_yield(); } } diff --git a/classlist.h b/classlist.h index 637e7f1..cd3b258 100644 --- a/classlist.h +++ b/classlist.h @@ -51,6 +51,7 @@ typedef HSIterator SnapIntHashSet; typedef HSIterator SnapIntIterator; typedef HashTable VarTable; +typedef HashTable RecToConsTable; typedef HashTable FunctionTable; typedef HashTable EqualsTable; #endif diff --git a/constgen.cc b/constgen.cc index 4f4ec3a..82042af 100644 --- a/constgen.cc +++ b/constgen.cc @@ -38,6 +38,7 @@ ConstGen::ConstGen(MCExecution *e) : rpt(new RecPairTable()), numconstraints(0), goalset(new ModelVector()), + yieldlist(new ModelVector()), goalvararray(NULL), vars(new ModelVector()), 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 (numvaluegetLen()) + if (numvaluegetLen()) { 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 * novel_branches=new ModelVector(); + 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;isize();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; } diff --git a/constgen.h b/constgen.h index 8669a7f..20420bc 100644 --- a/constgen.h +++ b/constgen.h @@ -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 * goalset; + ModelVector *yieldlist; Constraint ** goalvararray; ModelVector * 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 * stats; #endif diff --git a/doc/README.txt b/doc/README.txt index ddb8763..4f06337 100644 --- 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 + +IV. Generating doxygen docs + +Type "make docs". +Then look in doc/docs/. diff --git a/main.cc b/main.cc index 48ec61f..2b619a6 100644 --- 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; diff --git a/params.h b/params.h index 78cedcb..7f2e3cf 100644 --- 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; diff --git a/schedulebuilder.cc b/schedulebuilder.cc index 3bc6e96..6cf4b5a 100644 --- a/schedulebuilder.cc +++ b/schedulebuilder.cc @@ -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);