Random Path-Selection based-on Dynamically Changing Path-Sets (Tirage aléatoire uniforme dans une collection dynamique de chemins)
Exposé repris d'une présentation a MTV2
Personnes présentes
- Frédéric Boulanger
- Marie-Claude Gaudel
- Nicolay Kosmatov
- Safouan Taha
- Frédéric Voisin
- Burkhart Wolff
- Lina Ye
Presentators
- Frédéric Voisin
Summary:
This is a continuation of previous talks on Auguste, Rukia, and the Phd of Romain Aissat: Trying to use uniform random-selection from paths drawn from a Call-Graph of a program. The approach suffered from the fact that the probability of randomly choosen path to be *feasible* (i.e. there actually exist input data that stimulate that path) decreases inverse exponentially with the length of the paths.
The presented work suggests to "learn" infeasible paths by interleaving the random-selection phase with checking feasibility via some smt-solver: a newly detected shortest infeasible path-prefix is notified to Rukia (via a new functional interface) as "forbidden" which leads to an *incremental* update of the internal Rukia-tables leading to "better" path-selections in the next runs: once a prefix has been notified as "forbidden", paths with such prefix can no longer be drawn. No a priori knowledge about infeasible paths is needed: starting with an empty set of forbidden prefixes, the drawing incrementally adapts to each new infeasible prefix that is discovered.
Rukia is independent of the client application (here: drawing execution paths from a C.F.G) : it only knows about prefixes of paths in graphs coined as "forbidden" by its caller, whatever the reason. Rukia only depends on being notified with the *shortest* forbidden prefix of paths that must no longer be drawn. The drawing remains uniform over all paths with no known forbidden prefix.
In addition to drawing a path whose status is still unkown (no known forbidden prefix), Rukia also provides the length of its longest prefix known to be acceptable. The client application can use that information to save unnecessary feasibility checks (calls to the SMT solver in our case) without having to handle such bookeeping itself.
Coining as "forbidden" not only paths with infeasible prefixes but also feasible paths that were drawn yields a method for drawing feasible paths without replacement ("tirage sans remise"). By iterating the calls to Rukia one gets the the full set of feasible paths of a given length, at least when the latter is not to large to be computed in practice. Using its internal table Rukia knows when to stop: no path remains.
The work presents some experimental results about the power of the approach.
Material:
Questions abordés:
Bu: Instead of declaring just a prefix as "undesirable", wouldn't it be possible to retract an infinite set of paths, given, say, by an automaton ?
Assume that we have found that "ab" is unfeasible, found that "aab" is infeasible, that "aaab" is unfeasible, and assume that we speculated or even have a proof that any "a*b" is going to be an infeasible prefix, would it be possible to retract "a*b" from the tables of Rukia ?
Current answer: the method relies only on counting and currently we have no way to complement it with additional features. Indeed we will be interested in adding "semantic features" to counting; for examples whose infeasibility of path relies on specific dependencies about loop iterations. Hence, still to investigate.
