From 4f1c9ecb48a4fe49948a6a5eb574d47d8dcaf4b3 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 24 Jul 2004 20:30:00 +0000 Subject: [PATCH] - Amazingly, I think I implemented ni-synch partial order reduction. It still needs some careful analysis though. --- src/compiler.c | 23 +++++++++ src/modelchecker.c | 117 +++++++++++++++++++++++++++++++++++++++++++-- src/role.h | 5 ++ src/system.c | 1 + src/system.h | 1 + 5 files changed, 142 insertions(+), 5 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index bf192fe..5ece32f 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -416,6 +416,7 @@ commEvent (int event, Tac tc) } // Assert: label is unique, add claimlist info cl = memAlloc (sizeof (struct claimlist)); + cl->type = claim; cl->label = label; cl->rolename = fromrole; cl->count = 0; @@ -1041,6 +1042,21 @@ compute_prec_sets (const System sys) } r2++; } + // For ni-synch, the preceding label sets are added to the synchronising_labels sets. + if (cl->type == CLAIM_Nisynch) + { + Termlist tl_scan; + + tl_scan = cl->prec; + while (tl_scan != NULL) + { + if (!inTermlist (sys->synchronising_labels, tl_scan->term)) + { + sys->synchronising_labels = termlistAdd (sys->synchronising_labels, tl_scan->term); + } + tl_scan = tl_scan->next; + } + } // Check for empty stuff //@todo This is for debugging, mainly. if (cl->prec == NULL) @@ -1064,6 +1080,13 @@ compute_prec_sets (const System sys) */ memFree (eventlabels, size * sizeof(Term)); memFree (prec, size * size * sizeof(int)); + +#ifdef DEBUG + printf ("Synchronising labels set: "); + termlistPrint (sys->synchronising_labels); + printf ("\n"); +#endif + } //! Preprocess after system compilation diff --git a/src/modelchecker.c b/src/modelchecker.c index 8733edc..0d8984c 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -231,6 +231,45 @@ Roledef removeIrrelevant (const System sys, const int run, Roledef rd) return rdkill; } + +//! Unblock any waiting sends of my type. +/** + * Note that the caller must ensure that rd->forbidden is restored afterwards. + *\sa tryChoiceSend() + */ +void +unblock_synchronising_labels (const System sys, const int run, const Roledef rd) +{ + if (rd->type != READ || rd->internal) + return; + if (!inTermlist (sys->synchronising_labels, rd->label)) + return; + + // This read possibly unblocks other sends + int run_scan; + + for (run_scan = 0; run_scan < sys->maxruns; run_scan++) + { + if (run_scan != run) + { + Roledef rd_scan; + + rd_scan = sys->runs[run_scan].index; + if (rd_scan != NULL && + rd_scan->type == SEND && + rd_scan->forbidden != NULL && + isTermEqual (rd_scan->label, rd->label) && + isTermEqual (rd_scan->message, rd->message) && + isTermEqual (rd_scan->from, rd->from) && + isTermEqual (rd_scan->to, rd->to)) + { + rd_scan->forbidden = NULL; + } + } + } + return; +} + //! Explores the system state given by the next step of a run. /** Grandiose naming scheme (c) sjors dubya. * @@ -251,6 +290,7 @@ explorify (const System sys, const int run) int flag; int myStep; Roledef roleCap, roleCapPart; + Knowledge forbiddenBuffer; rd = runPointerGet (sys, run); myStep = sys->runs[run].step; @@ -263,6 +303,15 @@ explorify (const System sys, const int run) flag = 0; + /** + * -------------------------------------------- + * Is the event really enabled? + * Typically, a read event is only instantiated + * at this point, so we can only now do some + * instantiation related determinings. + * -------------------------------------------- + */ + /* * Special checks after (implicit) choose events; always first in run reads. */ @@ -459,13 +508,27 @@ explorify (const System sys, const int run) } } - /* Apparently, all is well, and we can explore further */ - flag = 0; + /** + * -------------------------------------------- + * Now we assume the event is indeed enabled ! + * -------------------------------------------- + */ + + /* (Possibly) do some local damage */ + // Unblock any sends + forbiddenBuffer = rd->forbidden; + if (sys->synchronising_labels != NULL) + { + unblock_synchronising_labels (sys, run, rd); + } + // Cap roles if (roleCap != NULL) { roleCapPart = roleCap->next; roleCap->next = NULL; } + + /* And explore the resulting system */ if (executeStep (sys, run)) { /* traverse the system after the step */ @@ -477,6 +540,8 @@ explorify (const System sys, const int run) sys->step--; indentSet (sys->step); + /* restore local damage */ + rd->forbidden = forbiddenBuffer; if (roleCap != NULL) { roleCap->next = roleCapPart; @@ -484,11 +549,13 @@ explorify (const System sys, const int run) return 1; // The event was indeed enabled (irrespective of traverse!) } + + +//! Simple nondeterministic traversal. + __inline__ int traverseSimple (const System sys) { - /* simple nondeterministic traversal */ - int run; int flag = 0; @@ -563,6 +630,43 @@ traverseNonReads (const System sys) return traverseSimple (sys); } +//! Execute a send +/** + *\sa unblock_synchronising_labels() + */ + +__inline__ int +tryChoiceSend (const System sys, const int run, const Roledef rd) +{ + int flag; + + flag = 0; + if (rd->forbidden == NULL) + { + /* this is allowed. So we either try it, or we try it later (if blocking) */ + /* Note that a send in executetry will always succeed. */ + /* 1. Simply try */ + flag = executeTry (sys, run); + /* 2. Postpone if synchonisable */ + if (inTermlist (sys->synchronising_labels, rd->label)) + { + /* This is supposed to be blocked, so we do so */ + /* It will possibly be unblocked by a corresponding read event, + * the actual code would be in explorify, post instantiation of the read event. + */ + if (sys->clp) + { + block_clp (sys, run); + } + else + { + block_basic (sys, run); + } + } + } + return flag; +} + //! Execute a read in the knowledge postponing way, on which the partial order reduction for secrecy depends. __inline__ int @@ -623,10 +727,13 @@ tryChoiceRoledef (const System sys, const int run, const Roledef rd) switch (rd->type) { case CLAIM: - case SEND: flag = executeTry (sys, run); break; + case SEND: + flag = tryChoiceSend (sys, run, rd); + break; + case READ: flag = tryChoiceRead (sys, run, rd); break; diff --git a/src/role.h b/src/role.h index 7c16aee..28a49ba 100644 --- a/src/role.h +++ b/src/role.h @@ -15,6 +15,8 @@ //! The container for the claim info list struct claimlist { + //! The type of claim + Term type; //! The term element for this node. Term label; //! The name of the role in which it occurs. @@ -66,6 +68,9 @@ struct roledef * Substructure for reads */ //! Illegal injections for this event. + /** + * For send this means that the send is allowed if it is NULL, otherwise it is blocked. + */ Knowledge forbidden; //! knowledge transitions counter. int knowPhase; diff --git a/src/system.c b/src/system.c index 4f6a027..bd00c87 100644 --- a/src/system.c +++ b/src/system.c @@ -80,6 +80,7 @@ systemInit () sys->variables = NULL; sys->untrusted = NULL; sys->secrets = NULL; // list of claimed secrets + sys->synchronising_labels = NULL; sys->attack = NULL; /* no protocols => no protocol preprocessed */ sys->rolecount = 0; diff --git a/src/system.h b/src/system.h index 4640836..0e48989 100644 --- a/src/system.h +++ b/src/system.h @@ -105,6 +105,7 @@ struct system /* properties */ Termlist secrets; //!< Integrate secrets list into system. + Termlist synchronising_labels; //!< List of labels that might synchronise. int shortestattack; //!< Length of shortest attack trace. /* switches */