From 62b2eca8da300a6221b2459eec609e2a0846365e Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 15 Jul 2004 11:04:15 +0000 Subject: [PATCH] - Implemented read symmetries reduction as a switch '--read-symm'. Works with e.g. t8. t10 is also implemented as a test. --- src/main.c | 7 +- src/modelchecker.c | 175 +++++++++++++++++++++++++++++++++++++++++++++ src/runs.c | 36 ++++++++++ src/runs.h | 2 + src/terms.c | 67 ++++++++++++++--- 5 files changed, 276 insertions(+), 11 deletions(-) diff --git a/src/main.c b/src/main.c index 2068fb5..116b64d 100644 --- a/src/main.c +++ b/src/main.c @@ -100,6 +100,7 @@ main (int argc, char **argv) struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "suppress progress bar."); struct arg_lit *switchSS = arg_lit0 (NULL, "state-space", "output state space graph."); struct arg_lit *switchFC = arg_lit0 (NULL, "force-choose", "force only explicit choose events."); + struct arg_lit *switchRS = arg_lit0 (NULL, "read-symm", "enable ready symmetry reductions."); #ifdef DEBUG struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter."); struct arg_lit *switchI = arg_lit0 ("I", "debug-indent", @@ -125,6 +126,7 @@ main (int argc, char **argv) switchS, switchSS, switchFC, + switchRS, #ifdef DEBUG porparam, switchI, @@ -277,7 +279,10 @@ main (int argc, char **argv) { /* force explicit chooses */ sys->switchForceChoose = 1; - warning ("Force choose enabled"); + } + if (switchRS->count > 0) + { + sys->switchReadSymm = 1; } #ifdef DEBUG sys->porparam = porparam->ival[0]; diff --git a/src/modelchecker.c b/src/modelchecker.c index 8e1c134..14b1a4f 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -91,6 +91,8 @@ traverse (const System sys) return traversePOR4 (sys); case 9: return traversePOR5 (sys); + case 10: + return traversePOR6 (sys); default: debug (2, "This is NOT an existing traversal method !"); exit (1); @@ -347,6 +349,7 @@ explorify (const System sys, const int run) roleCap = removeIrrelevant (sys, run, rd); + /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted, * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not * be violated anymore if they contain no terms that are encrypted with such keys */ @@ -365,6 +368,63 @@ explorify (const System sys, const int run) */ } + /* + * Special check b1: symmetry reduction part II on similar read events for equal roles. + */ + + if (sys->switchReadSymm) + { + if (sys->runs[run].firstNonAgentRead == myStep) + { + /* Apparently, we have a possible ordering with our symmetrical friend. + * Check if it has progressed enough, and has the same agents. + */ + int ridSymm; + + if (rd->type != READ) + { + error ("firstNonAgentRead is not a read?!"); + } + ridSymm = sys->runs[run].prevSymmRun; + if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents)) + { + /* same agents, so relevant */ + if (myStep > 0 && sys->runs[ridSymm].step < myStep) + { + // warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, run); + } + else + { + if (sys->runs[ridSymm].step <= myStep) + { + // warning ("Symmetrical firstread dependency #%i (for run #%i) has not read it's firstNonAgentRead %i yet, as it is only at %i!", ridSymm, run, myStep, sys->runs[ridSymm].step); + } + else + { + /* read was done, so we can compare them */ + int i; + Roledef rdSymm; + + rdSymm = sys->runs[ridSymm].start; + i = myStep; + while (i > 0) + { + rdSymm = rdSymm->next; + i--; + } + /* rdSymm now points to the instance of the symmetrical read */ + i = termOrder (rdSymm->message, rd->message); + if (i < 0) + { + /* only explore symmetrical variant */ + return; + } + } + } + } + } + } + /* Apparently, all is well, and we can explore further */ flag = 0; if (roleCap != NULL) @@ -1140,6 +1200,121 @@ traversePOR5 (const System sys) return flag; } +/* + * POR6 + * + * POR5 but has a left-oriented scan instead of working from the current run. + */ + +int +traversePOR6 (const System sys) +{ + Roledef rd; + int flag = 0; + int run; + int i; + int offset; + + /* Previously we did the sends first. This does not always improve things, + * depending on the protocol. + */ + // if (nonReads (sys)) return 1; + + /* a choice for choose */ + + /* The 'choose' implemented here is the following: + * + * choose ev#rid + * where rid = min(r: ev#r in enabled(sys): (r-lastrun) mod maxruns) + * and where lastrun is the runid of the previous event + * in the trace, or 0 if there was none. + */ + + /* First pick out any choose events */ + for (run = 0; run < sys->maxruns && !flag; run++) + { + rd = runPointerGet (sys, run); + + if (rd != NULL) + { + switch (rd->type) + { + case CLAIM: + case SEND: + break; + + case READ: + if (rd->internal) + { + flag = executeTry (sys, run); + } + break; + + default: + fprintf (stderr, "Encountered unknown event type %i.\n", rd->type); + exit (1); + } + } + } + + /* Try all events (implicitly we only handle enabled ones) starting with our + * first choice. If one was chosen, flag is set, and the loop aborts. */ + for (run = 0; run < sys->maxruns && !flag; run++) + { + rd = runPointerGet (sys, run); + + if (rd != NULL) + { + switch (rd->type) + { + case CLAIM: + case SEND: + executeTry (sys, run); + flag = 1; + break; + + case READ: + /* the sendsdone check only prevent + * some unneccessary inKnowledge tests, + * and branch tests, still improves + * about 15% */ + if (sys->knowPhase > rd->knowPhase) + { + /* apparently there has been a new knowledge item since the + * previous check */ + + /* implicit check for enabledness */ + flag = executeTry (sys, run); + + /* if it was enabled (flag) we postpone it if it makes sense + * to do so (hasVariable, non internal) */ + if (flag && hasTermVariable (rd->message) && !rd->internal) + { + int stackKnowPhase = rd->knowPhase; + + rd->knowPhase = sys->knowPhase; + if (sys->clp) + { + block_clp (sys, run); + } + else + { + block_basic (sys, run); + } + rd->knowPhase = stackKnowPhase; + } + } + break; + + default: + fprintf (stderr, "Encountered unknown event type %i.\n", rd->type); + exit (1); + } + } + } + return flag; +} + int propertyCheck (const System sys) diff --git a/src/runs.c b/src/runs.c index d99bf25..9910d3c 100644 --- a/src/runs.c +++ b/src/runs.c @@ -65,6 +65,7 @@ systemInit () sys->latex = 0; // latex output? sys->switchStatespace = 0; sys->switchForceChoose = 0; // don't force explicit chooses by default + sys->switchReadSymm = 0; // don't force read symmetries by default:w /* set illegal traversal by default, to make sure it is set later */ @@ -255,6 +256,7 @@ ensureValidRun (System sys, int run) myrun.start = NULL; myrun.know = knowledgeDuplicate (sys->know); myrun.prevSymmRun = -1; + myrun.firstNonAgentRead = -1; } } @@ -521,6 +523,36 @@ int staticRunSymmetry (const System sys,const int rid) return -1; // signal that no symmetrical run was found } +//! Determine first read with variables besides agents +/** + *@todo For now, we assume it is simply the first read after the choose, if there is one. + */ +int firstNonAgentRead (const System sys, int rid) +{ + int step; + Roledef rd; + + if (sys->runs[rid].prevSymmRun == -1) + { + /* if there is no symmetrical run, then this doesn't apply at all */ + return -1; + } + rd = sys->runs[rid].start; + step = 0; + while (rd != NULL && rd->internal && rd->type == READ) // assumes lazy LR eval + { + rd = rd->next; + step++; + } + if (rd != NULL && !rd->internal && rd->type == READ) // assumes lazy LR eval + { + warning ("First read %i with dependency on symmetrical found in run %i.", step, rid); + return step; + } + /* no such read */ + return -1; +} + //! Instantiate a role by making a new run. /** @@ -647,7 +679,11 @@ roleInstance (const System sys, const Protocol protocol, const Role role, termlistDelete (fromlist); runs[rid].locals = tolist; + /* Determine symmetric run */ runs[rid].prevSymmRun = staticRunSymmetry (sys, rid); // symmetry reduction static analysis + + /* Determine first read with variables besides agents */ + runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid); // symmetry reduction type II } //! Make a new role event with the specified parameters. diff --git a/src/runs.h b/src/runs.h index c05e485..989028a 100644 --- a/src/runs.h +++ b/src/runs.h @@ -134,6 +134,7 @@ struct run Knowledge know; //!< Current knowledge of the run. Termlist locals; //!< Locals of the run. int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter. + int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate. }; //! Shorthand for run pointer. @@ -208,6 +209,7 @@ struct system int porparam; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. int switchStatespace; //!< Output statespace for dot package int switchForceChoose; //!< Force chooses for each run, even if involved in first read + int switchReadSymm; //!< Enable read symmetry reduction //! Latex output switch. /** * Obsolete. Use globalLatex instead. diff --git a/src/terms.c b/src/terms.c index 0a5974b..35c931b 100644 --- a/src/terms.c +++ b/src/terms.c @@ -761,7 +761,7 @@ termDistance(Term t1, Term t2) } /** - * Enforce a (arbitrary) ordering on basic terms + * Enforce a (arbitrary) ordering on terms * <0 means a0 means a>b. */ int termOrder (Term t1, Term t2) @@ -771,25 +771,72 @@ int termOrder (Term t1, Term t2) t1 = deVar (t1); t2 = deVar (t2); - if (!(realTermLeaf (t1) && realTermLeaf (t2))) - { - error ("'termOrder' can only be applied to two basic terms."); - } if (isTermEqual (t1,t2)) { /* equal terms */ return 0; } + + /* differ */ if (t1->type != t2->type) { - /* unequal types (can this even occur?) */ + /* different types, so ordering on types first */ if (t1->type < t2->type) return -1; else return 1; } - /* same type, compare names */ - name1 = t1->left.symb->text; - name2 = t2->left.symb->text; - return strcmp (name1,name2); + + /* same type + * distinguish cases + */ + if (realTermLeaf (t1)) + { + /* compare names */ + int comp; + + name1 = t1->left.symb->text; + name2 = t2->left.symb->text; + comp = strcmp (name1,name2); + if (comp != 0) + { + /* names differ */ + return comp; + } + else + { + /* equal names, compare run identifiers */ + if (t1->right.runid == t2->right.runid) + { + error ("termOrder: two terms seem to be identical although local precondition says they aren't."); + } + else + { + if (t1->right.runid < t2->right.runid) + return -1; + else + return 1; + } + } + } + else + { + /* non-leaf */ + int compL,compR; + + if (isTermEncrypt (t1)) + { + compL = termOrder (t1->left.op, t2->left.op); + compR = termOrder (t1->right.key, t2->right.key); + } + else + { + compL = termOrder (t1->left.op1, t2->left.op1); + compR = termOrder (t1->right.op2, t2->right.op2); + } + if (compL != 0) + return compL; + else + return compR; + } }