cdiggins.com

Below is a post  I made to a discussion thread at Lambda-the-Ultimate. I though I would share it here, because it might help give others  some insight as to how abstract interpretation (AI) relates to the real worlds issues of static analyses and compiler optimizations. 

… I am using the definition of AI as “a partial execution of a computer program which gains information about its semantics without performing all the calculations.”.

This is an algorithmic definition of AI as opposed to the formal mathematical one that I realize that others here are apparently more familiar with: :a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices.”

“You’re speculating about what ought to be possible, rather than what existing abstract interpretation systems do, correct?”

No not really. What I am saying is based on the observation that many static analsysis and compiler optimizations are actually a form of abstract intrepretation (a point which the OP I believe was trying to get at). These usually yield increasingly helpful partial information while they executes whether or not they halts. Thus they aren’t neccessary to diverge, and can be executed in a non-deterministic manner.

So by extension I am saying that convergence isn’t neccessary for AI to be useful, just like other static analyses don’t have to halt to yield useful information. This really shouldn’t be a contentious statement. It may be very hard to model formally using probabilistic functions and lattices (I wouldn’t be able to) but algorithmically it is pretty trivial stuff.

It should be well-established that to deal with any algorithm that doesn’t guarantee halting, but yields useful partial information, is to simply write a nondeterministic multi-threaded version of the algorithm. By nondeterministic I am suggesting that during partial execution you can deal with branches and loops by spawning new threads. This makes it non-deterministic because, you can just halt (whether or not all threads converge) based on some arbitrary heruistic and you can schedule threads arbitrarily.

What I am suggesting shouldn’t be a new idea to other researchers, and I doubt it is. A quick search on ‘nondeterminsism + “abstract interpretation”‘ yields some apparently relevant papers:

• Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation (2000)
• Probabilistic Abstract Interpretation
• Trace-Based Abstract Interpretation of Operational Semantics
• Towards Viewing Nondeterminism as Abstract Interpretation (no paper, but interesting title)

Adhoc non-deterministic AI algorithms already exist in many compilers, it’s just that many programmers aren’t really aware of what it is that they are doing in formal terms. So the usefulness is pretty clear, whether the formal models of AI have reached that point or not.

Finally as for an example of a non-deterministic AI algorithm, consider the identification of whether or not a control path executes.