Rambles around computer science
Diverting trains of thought, wasting precious time
Sat, 12 Nov 2011
Static versus dynamic analysis---an illusory distinction?
When writing a recent talk, I found myself arguing that static and dynamic analysis are not really that different. At least, people don't really agree on the distinction. Model checking people frequently argue that what they're doing is dynamic analysis, because it directly explores paths through a system's state space. Meanwhile, abstract interpretation people would argue the opposite, since clearly model checking is an instance of abstract interpretation, and so is all other static analysis.
I'd much rather avoid the debate entirely. Since model checking is a far cry from run-time checking or testing, my sympathies initially lay with the abstract interpretation camp on this particular issue. But the distinction becomes even more ill-defined in other cases. In particular, I've been thinking a lot about symbolic execution, of the kind done by KLEE and other tools. Is it doing a static or a dynamic analysis? I'd challenge you to defend either position.
(Meanwhile, execution environments which are somewhat speculative, like transactional memories, lazy evaluators, or even plain old branch prediction, can be considered as partial runs of a static analysis. But I should save that line of thinking for another post.)
So rather than talking about static or dynamic analyses, here are some dimensions of analyses that I think are more interesting.
- Effecting versus effect-free—this is one killer distinction between traditional “static” and traditional “dynamic” analyses. If I run it, will it do the stuff that my program does (or might do)? Sandboxing, such as the environment modelling scaffolding in KLEE, can turn an effecting analysis into a non-effecting one without (necessarily) perturbing it along other dimensions (although KLEE also uses the same layer to enable symbolic I/O).
- Exploratory versus single-path—this is what those model-checking people were talking about, and is the most essential distinction between testing and other analyses.
- Terminating versus nonterminating—termination is a property that most static analyses, including abstract interpreters, like to have. By contrast, it's interesting that model checkers are happy with the approach of CEGAR, which is a (potentially) nonterminating loop. Also, type theorists have become increasingly comfortable with undecidable type systems in recent years, meaning that type checking need not terminate. For real programs, these methods still tend to terminate, of course.
- Overapproximate, underapproximate, both, neither—more formal mindsets care to distinguish between overapproximating analyses from underapproximating analyses. The former which offer false positive error reports but no false negatives, so include “sound”type systems. The latter might miss real errors, so include most symbolic executors (which, aside from nontermination, fall back on underapproximation once the solver fails) and other bug-finding tools. Interestingly, people with a bug-finding mentality, including model checkers, call type checkers “unsound” because they report spurious errors---completely the opposite sense from abstract interpretation's “sound overapproximatino”. I think both parties are a little distracted here. Many practical analyses are both underapproximating and overapproximating, or, put differently, are neither sound nor complete (whichever way round you put the terminology). They can still be useful; indeed, they are often the most useful analyses from a practical perspective. Here's a static deadlock detector that stuck in my mind as an unsound, incomplete yet effective analysis, from ICSE '09.
- Augmenting versus abstracting—sometimes an analysis will focus on a particular subset of a program's observable behaviours---type errors are one example, being the focus of type checkers' analyses. All the abstractions I know from the verification community---predicate abstraction, types, other abstract domains, and also slices---have this property. But conversely, some analyses are designed to tell you more than you could discern from any program trace! They do this by actively computing additional information that the underlying program did not. I call these “augmenting” analyses. Most of the examples I know are instrumentation-based systems. Valgrind's Memcheck tool is arguably one such, since it computes the “definedness” of each memory location. You might quibble that this is not truly augmented, in that definedness can be retroactively derived from a trace of memory operations. So maybe a better example is Cachegrind's profiling information, since it is computed in conjunction with a CPU simulation which isn't part of the original program at all. Another class of example is hardware simulators which computing timing information for the circuits they simulate. This is what makes simulation-oriented HDL constructs special, and in particular, “non-synthesisable”---they operate on data not present in silicon (and not practical to capture in silicon), but available in the simulation environment. This environment is effectively doing an instrumented (or “augmented”) run of the physical hardware.
- Exhaustive versus non-exhaustive—this is arguably the same as “terminating”, but I think it's a useful extra bit of vocabulary to have. You can make an analysis terminating by time- or space-bounding it, but an exhaustive analysis offers a stronger property: whatever abstract space it was traversing, it is designed to traverse all of it. This means the space must not only be finite, but small enough for computationally feasible exhaustive search.
- Repeating versus non-repeating—again, this is related to exhaustiveness and termination, but I'd argue it's not the same. Model checkers keep a history of the states they've visited, so they can detect when exploration has covered all states. By contrast, symbolic executors like KLEE do not keep a history, but store only the frontier states, so (for simple enough programs) might indefinitely traverse the same path through a state space. This (along with the use of a symbolic representation) is one of the key distinctions between KLEE and its forebear CMC.
- Adaptive/iterative versus not—many analyses are tunable or configurable in some way. By incorporating feedback from one run to the next, we can build a more sophisticated analysis that adaptively configures itself. CEGAR is a notable example. These feedback loops can yield interesting analyses of both terminating and nonterminating kinds, CEGAR being of the latter. (I'm sure there are other adaptive analysis approaches, but none springs to mind right now.)
That's all for now. Let me know if you can think of any more noteworthy dimensions!
[/research] permanent link contact
