Zak's research blog

This is not a particularly good way to spend time

2009-09-22T07:10:00.000-07:00

I've written many hello world program in my lifetime. This one took me the longest to write.


import sys
w = 0

fl=reduce

o="he = lambda l:fl(lambda x, (o,z):x.replace(o,z), l)\np=lambda(f, x): \"w = \"  + str(w)+ \"\\n\\nfl=reduce\\n\\no=\\\"\"+f(x) + \"\\\"\"\ndef rg2(l):\n  d=0\n  while l>0:\n    l=l>>1\n    d= 1+d\n  return d\nq = lambda d: he([d,(\"\\\\\", \"\\\\\\\\\"),(\"\\\"\", \"\\\\\\\"\"),(\"\\n\",\"\\\\n\")])\nsys.stdout.write(o[w])\nif w < 173:\n  w = w+(3*rg2(w))+1\n  exec(p((q,o)) + \"\\n\" + o)"
he = lambda l:fl(lambda x, (o,z):x.replace(o,z), l)
p=lambda(f, x): "w = "  + str(w)+ "\n\nfl=reduce\n\no=\""+f(x) + "\""
def rg2(l):
  d=0
  while l>0:
    l=l>>1
    d= 1+d
  return d
q = lambda d: he([d,("\\", "\\\\"),("\"", "\\\""),("\n","\\n")])
sys.stdout.write(o[w])
if w < 173:
  w = w+(3*rg2(w))+1
  exec(p((q,o)) + "\n" + o)
  sys.stdout.write("\n")

... anybody know how it works? The poor choice of variable names and non-standard spacing are, unfortunately, necessary.

EDIT: interestingly, one of the lines seems to be truncated in blogger. But copy+paste seems to get the full line.

Reading last week

2009-03-15T18:18:00.000-07:00

Patrick Cousot: "Abstract Interpretation Based Formal Methods and Future Challenges" (pdf)

The basic idea (I think): project values onto abstract domains. Lift all operations to those abstract domains. Replace conditional branches with nondeterministic ones. Compute fixpoints in the abstract domain, then map back to the concrete domain and query the resulting structure.
Reaffirms my feeling that abstract interpretation is the "right way" to do program analysis.
Unfortunately, not much in the way of math. I feel like I understand more about abstract interpretation, but only in a vague, handwavey-type of way

Patrick Lincoln: "Linear Logic" (ps)

Nice introduction to linear logic; would have been more helpful if I knew less about linear logic. Handy list of sequent calculus rules on the back!

Tanel Tammet: "Proof Strategies in Linear Logic" (springerlink)

I skipped a (long) section of this paper because it deals with resolution theorem proving in LL, and I'm thinking the prover I'm working on is going to be bottom-up. I also don't really know what the computational interpretation of resolution is, or if there is one.
Formalized a few intuitive ideas, said how they were proved (it's likely that the proofs are straightforward)
Gave me a better idea of what focusing is. I should probably read the references for that subsection.

Silvia Richter, Malte Helmert, Matthias Westphal: "Landmarks Revisited" (pdf)

A landmark for a planning task is a proposition that must hold at some point in any solution to the task. Given the landmarks of a task and the ordering between them gives a planner an idea of the "shape" of solution plans.
Computing landmarks and their orderings is (PSPACE-) hard. But a good way to extract some of them is to start at the goals of the task (which are trivially landmarks), and work backwards (a precondition of every task that achieves a landmark is a landmark, etc)
Landmarks/orderings can be used to estimate goal distances and also in action selection

Hector Palacios, Hector Geffner: "From Conformant Into Classical Planning: Efficient Translations That May be Complete Too" (pdf)

Conformant planning is a generalization of classical planning in which the initial state is only partially known (specified by a CNF formula)
Epistemic logic is a modal logic that can be used to reason about knowledge rather than truth (a fact can be true without my knowledge). Conformant planning tasks can be translated naturally to epistemic logic, where each literal is tagged by its "world" (the conditions that must have held in the initial state for the fact to hold - which actually specifies a set of initial states). Merge actions are used to combine knowledge about different worlds.
This translation can then be encoded propositionally, and the planning task can be solved by a classical planner.
It's possible to place bounds on how "specific" the world tags need to be for the translation to remain complete.

Rory - you are the worst person. The worst.

2009-03-02T08:25:00.000-08:00

Malte Helmert: "A Planning Heuristic Based on Causal Graph Analysis" (pdf)

Advocates multi-valued planning domains, because the extra structure can be exploited to obtain effective heuristics
Defines a causal graph, which is basically represents the "may interact with" relation among variables in a planning task
Defines a domain transition graph, which basically represents the paths a variable can make through its domain using the supplied actions (eg, a traffic light needs to go through a "yellow" state to transition from "green" to "red").
Defines a heuristic based on these two structures that appears to be pretty effective on several of the IPC domains. The heuristic is computed using costs to move each variable through its domain, where costs are computed by a modification of Dijkstra's algorithm on the domain transition graph. The edge weights of a variable's DTG are computed on-the-fly using information from the DTGs of the causal predecessors of the variable. This makes cyclic causal graphs awkward.

Malte Helmert, Hector Geffner: "Unifying the Causal Graph and Additive Heuristics" (pdf)

More multi-valued planning
Gives a declarative formulation of the causal graph and additive heuristics (that doesn't rely on any auxiliary strucutures like causual graphs, domain transition graphs, or planning graphs).
Shows how to obtain a heuristic that (sorta) generalizes both these heuristics. Really, the equations that define it look like the additive heuristic, and the actual meaning behind those equations is more like the causal graph heuristic. One notable success of this formalization is that it gets rid of some of the awkwardness that occurs in the CG heuristic when the causal graph contains cycles.

Patrik Haslum, Blai Bonet, Hector Geffner: "New Admissible Heuristics for Domain-Independent Planning" (pdf)

I wasn't crazy about this paper. It seemed very... ad hoc in places. This is possibly because I'm new to planning and I haven't built up my intuition yet.
One heuristic is based on another admissible heuristic which estimates the cost of achieving a set of goals by estimating (through recursive application of the heuristic) the cost of achieving a (fixed-size) subset of those goals. The idea of the paper is to partition the set of actions and compute the heuristic for each cell in the parition, relaxing the cost of each action not in the current cell, and then adding the results. It retains admissibility because the cells are disjoint so actions can't be counted twice. It is intuitively sometimes bigger, because actions that were "free" in the previous heuristic because of the fixed-size subset limitation may have to be paid for in the new heuristic. But it seems like the heuristic can also be smaller if there are multiple actions that can achieve the same goals and we choose the parition poorly.
The other heuristic is based on pattern databases, and hopefully its description will require less typing then the previous. The gist is that some mutex relations between variables are easy to find (particularly those that appear as a result of encoding multi-value variables into a propositional domain). We can exploit these relationships to prune inconsistent branches of the abstract search space (which are created by abstracting away information required to maintain the mutex relation).

Lucas Dixon, Alan Smaill, Tracy Tsang: "Plans, Actions and Dialogues using Linear Logic" (pdf), and
Lucas Dixon, Alan Smaill, Alan Bundy: "Planning as Deductive Synthesis in Intuitionist Linear Logic" (pdf)

Linear logic is obtained from classical logic by rejecting the inference rules of weakening and contraction. This allows for an interpretation of LL in which the proofs are essentially about resources rather than logical facts. A logical fact may be used arbitrarily many times (by contraction), or not used at all (by weakening). This is not the case for resources - I cannot use the fact that I have a quarter to buy myself a red gum ball and a green one; I cannot simply "forget" that I have an income so that I won't have to pay income taxes. Similarly, planning tasks feature fluents, whose truth value changes during plan execution. Interestingly, planning problems can be encoded into LL sequents such that each solution plan of a task will have a corresponding proof in LL.
Limiting LL to the intuitionistic fragment allows us to give a computational interpretation of the logic. Proofs in intuitionistic logics are constructive, which allows a proof of a sequent $\Gamma \vdash G$ to be seen as a program that, given objects corresponding to each type of $\Gamma$, constructs an object of type $G$. This computational interpretation of ILL tightens the correspondence between linear logic and planning: proofs of an encoded planning task can be seen as executable plans. That is, not only do plans map into ILL proofs, but ILL proofs map to plans. Thus, classical planning can be reduced to ILL theorem proving (the opposite reduction, however, is not possible).
The first paper is mostly about encoding multi-agent planning problems featuring dialogue into ILL, and then solving the planning problems using Lolli
The second paper is about a writing a prover for ILL in Isabelle/HOL. In particular, it features a neat way to handle $\otimes$R which they call lazy context splitting (which is pretty much what it sounds like).
Will become the basis of my Topics in KR&R course. Basically, I'm hoping to use planning techniques in an efficient(ish) theorem prover for intuitionist linear logic. Most of what I wrote here was stolen from my proposal.
Interestingly, the idea for this project came from Lucas Dixon, who I emailed looking for the IsaPlanner email and ended up exchanging a few emails. He suggested the project and offered to advise me on it, which I'm pretty excited about. Lucas is a nice guy.

Vijay D'Silva, Daniel Kroening, and Georg Weissenbacher: "A Survey of Automated Techniques for Formal Software Verification" (pdf)
(Survey paper, so here's a list of things that were mentioned that I'd like to know more about)

Abstract interpretation
Shape analysis
Predicate abstraction
Counterexample-guided abstraction refinement

Bonus! Random idea I've been thinking about lately: declarative concurrency. Instead of inventing concurrency mechanisms every time we need something done and then verify that our programs do not violate those mechanisms, it would be neat to specify the constraints that can't be violated and leave it to the compiler to come up with the mechanisms to guarantee this. For example, I can write a function atomic that just evaluates a thunk, but also give the compiler a constraint that no other thread can access shared memory while a function is in an atomic evaluation context. (Ok, that example's a bit awkward because then we'd also have to specify that atomic created an evaluation context or else we'd "forget" we're in an atomic context (call-by-name), or never realize that we're in one (call-by-value). But you get the picture). Thinking further along these lines, can we program in temporal logic?

Reading last week

2009-02-24T11:22:00.000-08:00

Vineet Kahlon, Franjo Ivančić, Aarti Gupta: "Reasoning about Threads Communicating via Locks"

We propose a new technique for the static analysis of concurrent programs comprised of multiple threads. In general, the problem is known to be undecidable even for programs with only two threads but where the threads communicate using CCS-style pairwise rendezvous [11]. However, in practice, a large fraction of concurrent programs can either be directly modeled as threads communicating solely using locks or can be reduced to such systems either by applying standard abstract interpretation techniques or by exploiting separation of control from data. For such a framework, we show that for the commonly occurring case of threads with nested access to locks, the problem is efficiently decidable. Our technique involves reducing the analysis of a concurrent program with multiple threads to individually analyzing augmented versions of the given threads. This not only yields decidability but also avoids construction of the state space of the concurrent program at hand and thus bypasses the state explosion problem making our technique scalable. We go on to show that for programs with threads that have non-nested access to locks, the static analysis problem for programs with even two threads becomes undecidable even for reachability, thus sharpening the result of [11]. As a case study, we consider the Daisy file system [1] which is a benchmark for analyzing the efficacy of different methodologies for debugging concurrent programs and provide results for the detection of several bugs.

Vineet Kahlon, Aarti Gupta: "An Automata-Theoretic Approach for Model Checking Threads for LTL Properties"

In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads. However, we exploit the observation that, in practice, a large fraction of concurrent programs can either be modeled as pushdown systems communicating solely using locks or can be reduced to such systems by applying standard abstract interpretation techniques or by exploiting separation of data from control. Moreover, standard programming practice guidelines typically recommend that programs use locks in a nested fashion. In fact, in languages like Java and C#, locks are guaranteed to be nested. For such a framework, we show, by using the new concept of Lock Constrained Multi-Automata Pair (LMAP), that pre*-closures of regular sets of states can be computed efficiently. This is accomplished by reducing the pre*-closure computation for a regular set of states of a concurrent program with nested locks to those for its individual threads. Leveraging this new technique then allows us to formulate a fully automatic, efficient and exact (sound and complete) decision procedure for model checking threads communicating via nested locks for indexed linear-time temporal logic formulae

Erica Melis: "Proof Planning with Multiple Strategies"

This paper addresses the integration of several planning strategies as a way to cope with otherwise intractable search spaces in proof planning. It discusses why it is reasonable to employ several refinement strategies and shows that it can be even necessary in order to find a proof plan at all. Motivated by our experiences in proof planning, the paper introduces new refinement strategies. Since choosing among strategies requires additional control some exemplary control knowledge that can be employed in proof planning is presented.

Reading last week

2009-02-22T16:36:00.000-08:00

Vineet Kahlon: "Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs"

Dataflow analysis for concurrent programs is a problem of critical importance but, unfortunately, also an undecidable one. A key obstacle is to determine precisely how dataflow facts at a location in a given thread could be affected by operations of other threads.This problem, in turn, boils down to pairwise reachability, i.e., given program locations c₁ and c₂ in two threads T₁ and T₂, respectively, determining whether c1 and c2 are simultaneously reachable in the presence of constraints imposed by synchronization primitives. Unfortunately, pairwise reachability is undecidable for most synchronization primitives. However, we leverage the surprising result that the closely related problem of parameterized pairwise reachability of c₁ and c₂, i.e., whether for some n₁ and n₂, c₁ and c₂ are simultaneously reachable in the program T₁ n_1||T₂ n₂ comprised of n₁ copies of T₁ and n₂ copies of T₂,is not only decidable for many primitives, but efficiently so. Although parameterization makes pairwise reachability tractable it may over-approximate the set of pairwise reachable locations and can, therefore, be looked upon as an abstraction technique.Where as abstract interpretation is used for control and data abstractions, we propose the use of parameterization as an abstraction for concurrency. Leveraging abstract interpretation in conjunction with parameterization allows us to lift two desirable properties of sequential dataflow analysis to the concurrent domain, i.e., precision and scalability.

Ravi Chugh, Jan W. Voung, Ranjit Jhala, Sorin Lerner: "Dataflow Analysis for Concurrent Programs using Datarace Detection"

Dataflow analyses for concurrent programs differ from their single-threaded counterparts in that they must account for shared memory locations being overwritten by concurrent threads. Existing dataflow analysis techniques for concurrent programs typically fall at either end of a spectrum: at one end, the analysis conservatively kills facts about all data that might possibly be shared by multiple threads; at the other end, a precise thread-interleaving analysis determines which data may be shared, and thus which dataflow facts must be invalidated. The former approach can suffer from imprecision, whereas the latter does not scale.
We present RADAR, a framework that automatically converts a dataflow analysis for sequential programs into one that is correct for concurrent programs. RADAR uses a race detection engine to kill the dataflow facts, generated and propagated by the sequential analysis, that become invalid due to concurrent writes. Our approach of factoring all reasoning about concurrency into a race detection engine yields two benefits. First, to obtain analyses for code using new concurrency constructs, one need only design a suitable race detection engine for the constructs. Second, it gives analysis designers an easy way to tune the scalability and precision of the overall analysis by only modifying the race detection engine. We describe the RADAR framework and its implementation using a pre-existing race detection engine. We show how RADAR was used to
generate a concurrent version of a null-pointer dereference analysis, and we analyze the result of running the generated concurrent analysis on several benchmarks.

Alan Bundy: "The Use of Explicit Plans to Guide Inductive Proofs"

We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs. We illustrate this technique by building a proof plan based on a simple subset of the implicit proof plan embedded in the Boyer-Moore theorem prover, [Boyer & Moore 79].

Manfred Kerber: "Proof Planning: A Practical Approach to Mechanized Reasoning in Mathemtics"

The attempt to mechanize mathematical reasoning belongs to the first experiments in artificial intelligence in the 1950 (Newell et al., 1957). However, the idea to automate or to support deduction turned out to be harder than originally expected. This can not at least be seen in the multitude of approaches that were pursued to model different aspects of mathematical reasoning. There are different dimension according to which these systems can be classified: input language (e.g., order-sorted first-order logic), calculus (e.g., resolution), interaction level (e.g., batch mode), proof output (e.g., refutation graph), and the purpose (e.g., automated theorem proving) as well as many more subtle points concerning the fine tuning of the proof search.
In this contribution the proof planning approach will be presented. Since it is not the mainstream approach to mechanized reasoning, it seems to be worth to look at it in a more principled way and to contrast it to other approaches. In order to do so I categorize the systems according to their purpose. The different attempts can be roughly categorized into three classes: machine-oriented automated theorem provers, interactive proof checkers, and human-oriented theorem provers. In the rest of the introduction we shall take a closerlook at these different categories.

Reading last week

2009-02-10T10:49:00.001-08:00

Thomas Reps, Susan Horwitz, and Mooly Sagiv: "Precise Interprocedural Dataflow Analysis via Graph Reachability"

The paper shows how a large class of interprocedural dataflow-analysis problems can be solved precisely in polynomial time by transforming them into a special kind of graph-reachability problem. The only restrictions are that the set of dataflow facts must be a finite set, and that the dataflow functions must distribute over the confluence operator (either union or intersection). This class of problems includes—but is not limited to—the classical separable problems (also known as “gen/kill” or “bit-vector” problems)—e.g., reaching definitions, available expressions, and live variables. In addition, the class of problems that our techniques handle includes many non-separable problems, including truly-live variables, copy constant pro pagation, and possibly-uninitialized variables.
Results are reported from a preliminary experimental study of C programs (for the problem of finding possibly-uninitialized variables).

Jorg Hoffmann, Berhard Nebel: "The FF Planning System: Fast Plan Generation Through Heuristic Search"

We describe and evaluate the algorithmic techniques that are used in the FF planning system. Like the HSP system, FF relies on forward state space search, using a heuristic that estimates goal distances by ignoring delete lists. Unlike HSP's heuristic, our method does not assume facts to be independent. We introduce a novel search strategy that combines hill-climbing with systematic search, and we show how other powerful heuristic information can be extracted and used to prune the search space. FF was the most successful automatic planner at the recent AIPS-2000 planning competition. We review the results of the competition, give data for other benchmark domains, and investigate the reasons for the runtime performance of FF compared to HSP

Checked out the first chapter of "Proofs and Types" by Jean-Yves Girard; "Programming in Martin-Lof's Type Theory: An Introduction" by Bengt Nordstrom, Kent Petersson, and Jan M. Smith; "Rippling: Meta-level Guidance for Mathematical Reasoning" by Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland; "Interactive Theorem Proving and Program Development" by Yves Bertot and Pierrre Castéran; and "Isabelle/HOL: A Proof Assistant for Higher Order Logic" by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. I decided that I'm going to read "Proofs and Types", "Rippling", and "Isabelle/HOL" - the rest are going back to the library (for now).

Reading last week

2009-02-08T09:01:00.000-08:00

Alan Bundy: "A Science of Reasoning"

"This paper addresses the question of how we can understand reasoning in general and mathematical proofs in particular. It argues the need for a high-level understanding of proofs to complement the low-level understanding provided by Logic. It proposes a role for computation in providing this high-level understanding, namely by the association of proof plans with proofs. Proof plans are defined and examples are given for two families of proofs. Criteria are given for assessing the association of a proof plan with a proof."

Alessandro Armando, Alan Smaill, Ian Green: "Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm"

"We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This plan makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate the plan with parts of a substantial example-the synthesis of a unification algorithm."

Jens Knoop, Bernhard Steffen, Jurgen Vollmer: "Parallelism for Free: Efficient and Optimal Bitvector Analyses for Parallel Programs"

"We consider parallel programs with shared memory and interleaving semantics, for which we show how to construct for unidirectional bitvector problems optimal analysis algorithms that are as efficient as their purely sequential counterparts and that can easily be implemented. Whereas the complexity result is rather obvious, our optimality result is a consequence of a new Kam/Ullman-style Coincidence Theorem. Thus using our method, the standard algorithms for sequential programs computing liveness, availability, very busyness, reaching definitions, definition-use chains, or the analyses for performing code motion, assignment motion, partial dead-code elimination or strength reduction, can straightforward be transferred to the parallel setting at almost no cost."

Azadeh Farzan, P. Madhusudan: "Causal Dataflow Analysis for Concurrent Programs"

"We define a novel formulation of dataflow analysis for con-current programs, where the flow of facts is along the causal dependencies of events. We capture the control flow of concurrent programs using a Petri net (called the control net), develop algorithms based on partially-ordered unfoldings, and report experimental results for solving causal dataflow analysis problems. For the subclass of distributive problems, we prove that complexity of checking data flow is linear in the number of facts and in the unfolding of the control net."

Robert Cartwright, Mike Fagan: "Soft Typing"

"Type systems are designed to prevent the improper use of program operations. They can be classified as either static or dynamic. Static type systems detect "ill-typed" programs at compile-time and prevent their execution. Dynamic type systems detect "ill-typed" programs at run-time. Static type systems have two important advantages over dynamic type systems. First, they provide important feedback to the programmer by detecting a large class of program errors before execution. Second, they extract information that a compiler can exploit to produce more efficient code. The price paid for these advantages, however, is a loss of expressiveness, modularity, and semantic simplicity. This paper presents a soft type systems that retains the expressiveness of dynamic typing, but offers the early error detection and improved optimization capabilities of static typing. The key idea underlying soft typing is that a type checker need not reject programs containing "ill-typed" phrases. Instead, the type checker can insert explicit run-time checks, transforming "ill-typed" programs into type-correct ones."

Daniel Bryce, Subbarao Kambhampati: "A Tutorial on Planning Graph-Based Reachability Heuristics"

"The primary revolution in automated planning in the last decade has been the very impressive scale-up in planner performance. A large part of the credit for this can be attributed squarely to the invention and deployment of powerful reachability heuristics. Most, if not all, modern reachability heuristics are based on a remarkably extensible data structure called the planning graph, which made its debut as a bit player in the success of GraphPlan, but quickly grew in prominence to occupy the center stage. Planning graphs are a cheap means to obtain informative look-ahead heuristics for search and have become ubiquitous in state-of-the-art heuristic search planners. We present the foundations of planning graph heuristics in classical planning and explain how their flexibility lets them adapt to more expressive scenarios that consider action costs, goal utility, numeric resources, time, and uncertainty."

Difference lists

2008-12-07T09:26:00.000-08:00

I posed a question in my tutorial hour a couple weeks ago: how do we append two lists in Prolog? It's not too hard to come up with something that works:

append([], Ys, Ys).
append([X|Xs], Ys, [X|As]) :- append(Xs, Ys, As).

Ok. Fine. Linear in the length of the first list. I can probably live with that. But what if I want to write a parser in Prolog, and I want to be able to append a lot of lists quickly? I need to represent my data differently. Difference lists are a solution to this problem - they're a logical data structure that's capable of constant time appends.

We can represent a list L as a pair of lists (L1, L2) such that L1 = L++L2 (writing ++ for append). Recall that - (minus symbol) is just an ordinary binary infix function symbol in Prolog, so we can write (L1, L2) more intuitively as the Prolog term L1-L2 (the difference between L1 and L2). The power of difference lists comes from the fact that we need not instantiate L2. That is, we represent L as the difference list [L|X]-X. Ok, that's pretty fancy I guess. Where do the constant-time appends come from?
append_dl(Xs-X, Ys-Y, Xs-Y) :- X = Ys.What is append_dl doing?

Suppose our goal is append_dl([1,2,3|A]-A, [4,5|B]-B, D). Let's do some unifications.


unify(Xs-X, [1,2,3|A]-A) => Xs = [1,2,3|A] and X = A
unify(Ys-Y, [4,5|B]-B) => Ys = [4,5|B] and Y = B
unify(X, Ys) => X = [4,5|B]
unify(D, Xs-Y) => D = [1,2,3|A]-B = [1,2,3|X]-B = [1,2,3|[4,5|B]]-B = [1,2,3,4,5|B]-B

So D = [1,2,3,4,5|B]-B, which is a difference list representing [1,2,3,4,5]. Fancy.

How do we represent an empty list? Well, just L-L. Sure, that makes sense. Then we can check emptiness with empty_dl(L-L). , right? Well... not quite. Prolog's unification algorithm doesn't do an occurs check by default, so empty_dl will succeed on a nonempty list (with a nonsensical unification L=[elements,of,the,list|L]). So we need to check emptiness with
empty_dl(X, Y) :- unify_with_occurs_check(X, Y).

... which isn't as nice. But on the upside, it actually works (always a plus). The purpose of writing this was to talk about definite clause grammars, which I haven't even started doing. So maybe next time.

Notes on "Sketching Concurrent Data Structures"

2008-12-06T07:03:00.000-08:00

by Armando Solar-Lezama, Christopher Grand Jones, Rastislav Bodik

The abstract got me very excited about this paper. The basic idea is to turn high level descriptions (sketches) of concurrent data structures into full-blown, efficient, and correct implementations. That's awesome. I think that's more or less the future of programming.

The rest of the paper left me much less excited. It turns out that the sketches aren't really high-level descriptions - they're more like grammars for generating lists of commands that the programmer thinks might be involved in a correct implementation. Then their algorithm just searches the space of programs generated by the grammar, trying to find one that's actually correct. Still kinda neat, but I think this is far less interesting than what I understood from the abstract. Now it seems less like a tool for helping programmers be more productive by not making them fill in all the gory details of their data structure, and more like a tool for helping students cheat on their homework. I know that a sketch tool like this for Prolog would certainly help some of the people in the class I'm TAing with the latest assignment ("I know it has to be recursive, and I know it has to use this and this... but how do I do it?").

Theoretically, I think it's kinda interesting. The search space is huge, but finite - so it isn't too impressive from a computability standpoint. From a complexity standpoint, it's hard to say. The author's don't give a complexity analysis of their algorithm (my guess: at best in NP, at worst, probably still in PSPACE). I also don't have a sense for a lower bound on this kind of problem. But their experimental results are reasonable.

It's not clear to me exactly what assumptions they are making as far as verifying whether a candidate solution is correct. But even if the algorithm requires a correct sequential implementation, I'm OK with that - that seems like a reasonable thing to have on hand in some situations. But generally, I think that genetic programming people do more interesting things with fewer assumptions.

That said, this could potentially be useful if it were much faster. I could see myself using the tool if it took a few seconds (rather than ~ 1 hour) to get a correct implementation. Basically, if the tool isn't significantly faster than my brain (on realistic tasks, not homework assignments where you're told what kind of constructs you should use), then I'm not sure what practical use this has.

So the verdict: kinda neat. Wouldn't mind hearing a talk about it at a conference. Wouldn't want to work on it myself. If I was a professor, I would keep my eye on this project - "your implementation should use an atomic swap operation"-style hints for homework assignments may not be a good idea anymore.

Pragmatism

2008-11-25T18:52:00.001-08:00

No one has ever accused me of being pragmatic.

This afternoon, I decided to take another look at tomboy for my note-taking needs. I tried it once before, when I first heard that it had a latex plugin, which is pretty much essential for what I intend to do with tomboy. This was maybe a year ago. The latex plugin was pretty buggy back then and I didn't really like the idea of losing all of my notes, so I went back to my old system of just writing everything up in .tex files and then promptly forgetting where I put them. For some reason, I looked up tomboy again this afternoon, and I discovered that the latex plugin "can now be considered stable". Sweet. I tried it out, and it seems stable enough. Well... seemed stable enough. Until I tried to copy and paste something. It didn't crash - it just mutated my documents in exciting ways that I hadn't thought possible. Oh well... I guess I can just disable the plugin on the rare occasion that I need to copy and paste latex formulas. Except that's even worse. That's... much worse. Disabling and re-enabling the plugin makes every subsequent keystroke in the note double every single equation. The equations are also strangely difficult to delete. So I ruined a couple of hours of work.

So clearly, the first step towards fixing this problem is design (and write a compiler for) an extensible programming language. What? Oh right -- pragmatism. Not a quality I typically possess. I'm a bottom-up kind of guy. Of course, my first instinct was to just fix the problem. But then I thought about what happened the last time I did that (a year ago). I decided the code was too weird and I might as well rewrite the whole thing from scratch. But I'm probably going to have to learn C# anyway if I'm going to write the plugin from scratch, so I might as well fix all the problems I had with tomboy. But if I'm going to do all that, wouldn't it be simpler to just write my own note taking program that's better suited to my needs? Yeah - that makes sense. That's what I started doing last year. I got surprisingly far (and learned a bit of python in the process), but eventually the semester started, classes+thesis got in the way and I put the project down. Probably for the best.

My opinions have changed since then - now they're even less practical. Clearly, my mistake last time was trying to write the thing in python. Python, and almost every other language in popular use for that matter, is complete unsuitable for GUI development. So before I write my notes program, I will have to write a compiler for a DSL for GUI development (I think JavaFX has the right idea, but it has Java right in the name, and frankly... I have principles).

Not so fast! I can't just go off writing a compiler every time I think that there aren't any languages suitable for my particular task! That's just crazy. Obviously, my first step must be to design an extensible language so that I can churn out DSLs effortlessly.

This is something I was seriously considering until a couple of hours ago. Sometimes I don't even stop there. I can't believe that we're still using operating systems that haven't been formally verified. I don't like the way processors are currently designed. I don't think Turing machines are a particularly good formalism. I will occasionally have a day or two where I decide that I am going to be a constructivist. If left to my own devices, I would never accomplish anything. Ever.

But somehow, today, I bit the bullet. Tomboy-LaTeX, featuring copy+paste that won't ruin your afternoon, a fix that took (maybe) 10 lines. At some point, I promise that I will alert the maintainer of Tomboy-LaTeX. (I frequently break my promises).

Notes on "Applications of Craig Interpolants in Model Checking"

2008-11-10T13:14:00.000-08:00

by K. L. McMillan

Given a pair $(A,B)$ inconsistent formulas, an interpolant for $(A,B)$ is a formula $\hat{A}$ such that

$A \Rightarrow \hat{A}$
$\hat{A} \land B$ is unsatisfiable
$\hat{A}$ refers only to the common (extra-logical) symbols of $A$ and $B$.

(I've also seen a Craig interpolant for $A, B$ with $A \Rightarrow B$ defined as a formula $\hat{A}$ over the common symbols of $A,B$ with $A \Rightarrow \hat{A}$ and $\hat{A} \Rightarrow B$, but it's the same concept - just negate $B$). The idea of an interpolant is that $A$ may contain information that is not needed to contradict $B$, and we should be able to remove this extra information to obtain a simpler description of $A$. In fact, we can remove the extra information (that is, compute the interpolant) efficiently from a refutation proof of $A \land B$ (in some proof systems, at least). In the main algorithm proposed in this paper, these refutations are already being computed, so the interpolants essentially come "for free".

There are three applications for Craig interpolants proposed in the paper in model checking: approximate image computation, predicate abstraction, and approximating the transition relation. I'm only going to write about approximate image computation for now, but in all cases, we're working in the magical world of symbolic model checking.

The basic idea of symbolic model checking is to avoid the cost of computing all the states of a system by representing and manipulating sets of states symbolically. Typically, this means representing sets of states and transitions as formulas in first order logic (this paper is not an exception).

Fix a vocabulary $S$ of variable, function, and proposition symbols. A state formula $\phi$ is a first order forrmula over $S$ that represents a set of states (namely, the first-order models of $\phi$). Now that we can encode sets of states, how can we encode the transition relation? We define a vocabulary $S'$ that is the image of $S$ under a transformation that takes each symbol in $s \in S$ to a symbol $s'$ (we assume $\nexists s$ such that $s' \in S$, so $S$ and $S'$ are disjoint). A transition formula is just a first-order formula over $S \cup S'$. Intuitively, the $S$ symbols are used to represent what is true in the "current" state, and the $S'$ symbols are used to represent what is true in the "next" state. Now we have the tools to define our entire system: a transition system is a pair $(I, T)$ consisting of an initial state formula $I$ and a transition formula $T$.

In most of the following, we're actually interested in checking reachability (or safety) properties. A formula $\psi$ is $T$-reachable from a formula $\phi$ if there is a sequence of models $\sigma_1, \ldots \sigma_k$ such that $\sigma_1 \vDash \phi$, $\sigma_k \vDash \psi$, and $\forall 1 \leq i < k. [\sigma_i \cup \sigma_{i+1}' \vDash T]$. A formula $\phi$ is reachable in a transition $(I, T)$ if it is $T$-reachable from $\phi$, and is an invariant if $\lnot \phi$ is not $T$-reachable from $I$.

Now that we have a bunch of fancy definitions, let's see if we can actually do anything useful with them. Safety properties are usually phrased as "starting from the initial state, an error state is not reachable". So we want an algorithm that, given a transition system $(I,T)$ and a formula $\psi$, either proves that $\psi$ is not $T$-reachable from $I$ or provides a counter-example.

The image (strongest postcondition) $im_T(\phi)$ of a state formula $\phi$ with respect to transition formula $T$ is the strongest proposition $\psi$ such that $\phi \land T \Rightarrow \psi'$ (strongest in the sense that for all $\varphi$, if $\phi \land T \Rightarrow \varphi'$ then $\psi \Rightarrow \varphi$). The image of a formula captures the idea of "if the system is currently in state $\phi$, what can we prove about the next state?". We can actually compute $im_T(\phi)$ with the formula $im_T(\phi)' = \exists S.\phi \land T$ (just existentially quantify the free variables of $\phi \land T$).

OK - almost to the computationally useful stuff.

A state formula $\phi$ is an invariant when $\lnot \phi$ is not reachable from $I$ by $T$. $\phi$ is an inductive invariant when $I \Rightarrow \phi$ and $im_T(\phi) \Rightarrow \phi$. The strongest invariant of an $(I, T)$ is an invariant that implies all other invariants of $(I,T)$. It turns out that strongest inductive invariants are inductive invariants, and we can compute the strongest inductive invariant using the image operator (it's the fixed point $\mu Q. I \lor sp_T(Q)$). The models of the strongest inductive invariant of $(I, T)$ are exactly the reachable states of the system.

Finally, back to the problem at hand: we can verify that some formula $\psi$ is unreachable in $(I, T)$ by showing that it is inconsistent with the strongest inductive invariant.

Whew. Now let's start on the real contents of the paper.

Approximate image based on interpolation

An over-approximate image operator $\bar{sp}$ is an operator such that for all predicates $\phi$, $sp(\phi) \Rightarrow \bar{sp}(\phi)$. Unreachability analyses based on over-approximations are sound: the states reachable from $I$ by $\bar{sp}$ is a superset of those reached by $sp$. We say that $\bar{sp}$ is adequate with respect to $\psi$ when, for any $\phi$, if $\phi$ can't reach $\psi$ with $sp$, then it can't reach $\psi$ with $\overline{sp}$. Thus, unreachability analyses based on adequate over-approximate image operators are both sound and complete. So the basic idea is to compute an adequate over-approximate image operator $\bar{sp}$, compute its strongest invariant $R$, and then prove that $\psi$ is unreachable by refuting $\psi \land R$. But we haven't really saved anything because we've replaced our image operator (which we know how to compute) with an approximate image operator (which we don't). So how do we compute an adequate $\bar{sp}$? The solution is to bound our notion of adequacy.

A $k$-adequate image operator is an $\bar{sp}$ such that, for any $\phi$ that cannot reach $\psi$, $\bar{sp}_T(\phi)$ cannot reach $\psi$ within $k$ steps. This is looking to be more tractable - we can reuse the ideas of bounded model checking.

Once again, we are trying to prove that $\psi$ is unreachable. Define

$A = \phi_0 \land T_0$

$B = T_1 \land \dotsi \land T_k \land (\psi_1 \lor \dotsi \lor \psi_{k+1})$

If $A \land B$ is satisfiable, then $\psi$ is reachable, and we're done. Otherwise, we compute an interpolant $\hat{A}$ of $(A,B)$ (computationally inexpensive because we already have a refutation of $A \land B$). $\hat{A}$ is taken to be the over-approximate image of $\phi$. So by the definition of interpolants: $\hat{A}$ is over the symbols in $A_1$ (so $\hat{A}$ is a well-defined state formula), $A \Rightarrow \hat{A}$ (whence $\hat{A}$ is an over-approximation of $sp(\phi)$), $\hat{A}$ cannot reach $\psi$ in $k$-steps (by the structure of $B$ and the fact that $B \land \hat{A}$ is unsatisfiable, whence $\hat{A}$ is $k$-adequate).

In summary, the algorithm goes something like this (I think):


def unreachable(I, T, psi):
 for k <- 1 to infinity
   R <- true
   R' <- I
   while (R != R'):
     R <- R'
     B <-T_1 /\ ... /\ T_k /\ (psi_1 \/ ... \/ psi_k)
     if (R' /\ T_0) /\ B is satisfiable:
       if R = I: (* this is the first iteration of the invariant computation *)
         return false (* psi is reachable from I in k steps *)
       else:
         goto next (* sorry, Dijkstra *)
     R' <- I \/ interp(R' /\ psi) (* interpolant from refutation of R' /\ psi *)
   if R /\ psi is unsatisfiable:
     return true
   next: skip

When $k$ is the diameter of the state space, $k$-adequacy coincides with adequacy, so if psi is reachable). So in finite systems, this method is complete. This method works for infinite state systems, too, but it isn't guaranteed to terminate.

Thoughts:

The author mentions that the properties of the benchmark suite are localizable, which likely improves the performance of the interpolation-based method. What happens with other benchmark suites? How does the interpolating model checker compare with other (symbolic) model checkers? (although the paper does mention that the SMV model checker (based on BDDs) is unable to verify any of the properties. Only compared to proof-based abstraction (another method co-developed by McMillan)
I wonder if we efficiently compute the diameter of a state space (so we can bound the run-time of the algorithm)? And how can we efficiently test the equivalence of two formulas (needed in fixed point calculation)? Double implication? That doesn't seem to be efficient. Am I even correct in thinking that this is how the strongest invariant is calculated?

Notes on ``Symbolic Model Checking without BDDs''

2008-11-09T15:13:00.000-08:00

By Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu

Wow. It has been over a month since I last wrote on this blog. That is... not so good. Also, I need to figure out how to use latex in blogger - my current solution, which is an incredibly ugly mixture of sed and awk scripts that I wrote earlier today, badly needs to be replaced.

In the 1970's, a couple of people made a connection between temporal logics and automata, and started to use logic to analyze reactive systems. People were pretty excited about it. A few years after that, someone said that we're wasting a whole lot of time building these automata, and we could verify more stuff if we knocked it off and just represented it implicitly using BDDs. People were, once again, pretty excited about it. A few years after that, a few other people said that we're wasting a lot of time building these BDD's, and we could verify more stuff if we knocked it off and just represented everything as a propositional formula and left all the hard issues to SAT solvers. These last people were Biere, Cimatti, Clarke, and Zhu. I'm not sure how exciting other people found it, but I think it's pretty neat.

Bounded model checking

First, the authors restrict themselves to the existential model checking problem (an LTL formula f is existentially valid in a Kripke structure M iff there exists a path in M (starting from an initial state) that satisfies f). This corresponds to model checking the formula Ef (We get universal model checking for free by duality). The idea behind bounded model checking is that we can "solve'' existential model checking problems by looking at finite prefixes of infinite paths.

Soundness and completeness are the obvious desirable properties for bounded model checking. That is, we want to show:
1) If we can prove Ef in bounded semantics, it should hold in the unbounded semantics
2) If Ef can be proved in the unbounded semantics, then we should be able to prove it in the bounded semantics.

How can we say that a finite path satisfies an LTL formula? Having GP hold on a finite path doesn't mean that it holds on an infinite path (it could be the case that every infinite extension of any finite path that satisfies GP does not satisfy GP). The trick is to consider finite paths that terminate at a node that has a transition back to a previous state in the path. We can view these paths as describing the infinite path formed by traversing this loop forever (that is, we can identify a finite path p with the infinite path $uv^\omega$ (where p = uv)). With this in mind, it isn't too hard to develop sound semantics for bounded model checking.

The really interesting issue, I think, is completeness. Not every infinite path over a finite automaton can be written as $uv^\omega$, and it isn't clear that every formula f that is satisfied "complex" path is also satisfied by a "simple" path (we need f to be satisfied by a path of the form $uv^\omega$ for completeness to hold). We are saved by the fact that LTL isn't a very powerful language - it can't express properties that can't be satisfied by simple paths.

So what have we gained from switching to bounded model checking? Well, now that we're only considering finite paths, we can express paths, transition functions, and LTL formulas in finite propositional logic. Basically, we just reduce bounded model checking to SAT. But wait! Why would we reduce a problem to an NP-complete problem? Well, it turns out that (unbounded) model checking is PSPACE-complete, so NP isn't that bad. And there are some pretty good SAT solvers out there.

So now we know the basic method for bounding model checking. We know that for any formula that is provable in the unbounded semantics is provable in k bounded semantics for some k. So if a formula Ef is true in a Kripke structure, we can prove it using bounded model checking by first using 1-bounded model checking, then 2 bounded, then 3, and so on until we prove Ef. But what if Ef isn't provable? Then our algorithm doesn't terminate. So we need to find a bound for the largest k such that k-bounded model checking lets us prove more things than (k-1)-bounded model checking. The authors present bounds for various fragments of temporal logic, the worst of which is exponential (LTL), the best of which is linear (ECTL).

Thoughts:
- The efficiency of BDD-based approaches depends heavily on the choice of variable ordering. Finding an optimal variable ordering is NP-complete. Are there good approximation algorithms? Maybe. I don't know. I'm sure that a lot of effort has gone into finding nice heuristics, but I am unaware of approximation hardness results.
- The authors suggest that SAT solvers could be specialized to the domain of model checking. I wonder if anyone has actually done anything in this direction - it seems interesting.
- The authors derive different bounds (and thus, time complexities) for different fragments of temporal logic. I wonder if there has been much work on automatically finding the minimal fragment of temporal logic to which a formula belongs and specializing the bound accordingly.

Reversible Debugging Using Program Instrumentation

2008-10-06T12:47:00.000-07:00

by Shyh-Kwei Chen, W. Kent Fuchs, and Jen-Yao Chung.

Reversible execution allows a program to be executed backwards so that we can observe a previous state of execution. It is particularly useful as a debugging tool: imagine a "step backwards" button in your debugger (or a "step backwards" series of finger-mangling keystrokes, if that's your thing) that allows you to find the cause of an error by "undoing" previously executed commands.

Loops are a pretty good justification for reversible debuggers. Suppose we are interested in the last execution of a loop, because, well, that's where the bug probably occurs. With a forward-executing debugger, we have to step through the entire loop to see what we're interested in. Manually. (Ok... in most cases we could also set a condition on the breakpoint - but not always). Another interesting use case is when we just make a mistake while using our debugger (well, interesting in the sense that this happens to me all the time).

One way to implement a reversible debugger is a checkpointing system, where the system state is periodically saved so that we can undo operations by reverting to the last checkpoint and then running the program forward until we get to the state just before the last instruction was executed. The approach of the paper is a little more fine grained - more checkpoints, but less information stored at each checkpoint. This speeds up forward execution at the price of not being able to undo across irreversible function calls.

The "program instrumentation" part of this paper is that the reversible debugger is implemented by inserting instructions into the program to be debugged that record checkpoint information to a history buffer (but do not affect the semantics of the program). In particular, the authors use assembly-level instrumentation (so no source code analysis needs to take place to determine which variables need to be saved). Every procedure has an instrumented (reversible) and non-instrumented (irreversible) version, and the user of the debugger can choose which procedures they would like to be able to reverse ("recorded areas").

I have a problem with the idea of recorded areas. Basically, to speed up the debugger, the authors insist that only recorded areas be available for backwards execution. This is pretty odd, because it means that the programmer needs to mark these areas ahead of time, so that they can be computed backwards. If we get to the end of a recorded region, we can't go back - we have to run everything forwards again. I think this negates some of the effects of having a reversible debugger.

Another issue is that we can't undo across irreversible function calls - this (in my opinion) severely limits the practicality of the approach. On the other hand - there isn't really anything that can be done. It is unsound to undo "past" an irreversible function call in a language with side effects. Consider the following:


int f() /* reversible */
{
  int x = 0;
  if (x == 1)
      return;
  g(&x); /* do we save x here? */
  while(1);
}

int g(int * x) /* irreversible */
{
  *x = 1;
}

What if g modifies some element of a globally visible data structure -- do we make a copy of the entire data structure? That's very expensive. What if we just can't prove that a function doesn't modify a particular shared resource? Do we need to make a copy? I don't have a good solution (other than to use a language without mutable storage... but I don't really want to end all of my blog posts with "this would be way easier if you were using Haskell").

Notes on "Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs"

2008-09-28T11:23:00.000-07:00

by Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke.

I managed to avoid doing any work whatsoever while I was in Japan, so this is the first paper off the stack that Greg gave me that I've gotten around to reading. Due to the long name of the paper, I'll refer to it as SE+MC.

The idea of SE+MC is to combine symbolic execution and model checking to prove that a parallel program is (extensionally) equivalent to its sequential specification (two programs are equivalent if they produce the same output for a given input). The method applies to numerical programs (taking a vector of ints/floats as input and producing a vector of ints/floats as output) without side-effects (no IO, no randomness). So essentially, we build a sequential program that we assume is correct (after all, reasoning about sequential programs is easy), and we prove that our parallel program is correct by showing that it is equivalent to the sequential one. The authors claim that in practice, a sequential version of a program will often be created as a prototype for the parallel version, so it isn't unreasonable to require both versions.

Symbolic execution is a way to avoid losing information during the execution of a program. Whenever we encounter an expression that we can't compute exactly (such as expressions involving unknown values, or floating point operations), we replace the numeric operation with a symbolic one. While a numeric operation evaluates to a numeric value, its corresponding symbolic operation forms a symbolic expression tree, rooted at a node corresponding to the numeric operation, with children corresponding to its operands (thus, a symbolic expression tree is a tree where leaves are literals or symbolic constants and each internal node is associated with a numeric operation).

It's pretty clear why we would want to model expressions like (x + 1) symbolically - we just can't do better (assuming we don't have a value for x). The idea of using symbolic expressions to model floating point operations is more interesting. Floating point arithmetic doesn't have all the nice properties of real arithmetic. If we use a computer to verify a program that uses floats, that verification will have a bias for the particular implementation of floating point arithmetic on the computer. For instance, if the correctness of my program relies on the associativity of floating point addition (which need not hold in IEEE fp arithmetic), and my laptop happens to actually have associative floating point addition, an analysis running on my laptop would miss the error. If we use symbolic operations, the expression trees for, say, (1.0 + (2.0 + 3.0)) and ((1.0 + 2.0) + 3.0) are distinct, so we don't make this mistake. And of course we can add special rules for the equivalence properties that we actually can count on (like x + 0.0 = x).

Given a sequential and a parallel program, the method of SE+MC is to construct models for each of these programs in which symbolic operations replace numeric ones wherever it is appropriate (unfortunately, these models are built by hand at the moment). The models are then checked by Spin, a linear temporal logic model checker (which I'll probably write about later, because I'm taking a class in it). These models are then combined into a single model that first executes the sequential program, then executes the parallel program. Spin is responsible for exploring all the possible paths of this combined model and making sure that the outputs of the sub-models match.

One interesting issue is programs that branch on conditions that depend on inputs (which is probably almost every program). We need some way to say that we only need outputs to match if the programs had the "same" branch conditions - otherwise, a program as simple as


def f(x):
if x < 0:
  return -1
else:
  return 1

wouldn't even be equivalent to itself. For this reason, the authors introduce a path condition, which is a conjunction of boolean-valued symbolic expressions that determine the path that was taken through the model. This path condition is built during the execution of the sequential model: whenever a branch is encountered, if the path condition contains enough information to determine the value of the condition of the branch, the the appropriate branch is taken. Otherwise, a branch should be chosen non-deterministically the branch condition (or its negation) should be added to the path condition. During the execution of the part of the model corresponding to the parallel program, we hope to have enough information built up in the path condition that we don't explore paths that are inconsistent with the path taken in the sequential model. So we have changed our equivalence condition slightly: two programs are equivalent if for every input and path condition, they produce the same output.

Now there is an issue with how accurate we really need to be when determining whether a branch condition is a logical consequence of a path condition. The most accurate thing to do would be to defer to a theorem prover, but that may slow down the analysis. The authors use a much weaker reasoning facilities. It would be interesting to see how much longer it would take to use a more powerful prover. It's possible that using a powerful prover could actually decrease running time because it would cause fewer paths to be explored by Spin.

The authors also discuss methods to reduce the number of paths that Spin explores. What we're really interested in for this analysis is the final state of the model. Program equivalence is defined in terms of outputs - we don't need to know every detail about the executions that produced those outputs. It is not necessary to explore all possible paths through a model in order to explore all possible terminal states. There are often many equivalent paths that terminate in the same state, and it would be inefficient to explore all of them. So we would like some theorems that allow us to reduce the number of paths explored while maintaining the full set of possible final states.

By default, Spin will explore every path through the model - this corresponds to a scheduling policy that allows any (non-blocked) instruction to executed in any order. The authors prove a partial order reduction theorem that essentially states that we will explore the same set of terminal states if we restrict this scheduling policy (through the use of atomic blocks in Promela, Spin's modeling language). They also prove a reduction theorem about symmetric input vectors, but it seems like it would not be very general.

Another optimization that is briefly mentioned is that it is sometimes possible to refactor code to remove nondeterminism (and thus decrease the number of paths explored by Spin). The example given by the authors is something that arose when analyzing a Monte Carlo algorithm to estimate the value of pi:


if x*x + y*y < 1.0:
 in++
else:
 out++

can be refactored into something like:


in += delta(x*x + y*y, 1.0)
out += 1.0 - delta(x*x + y*y, 1.0)

where delta is defined like


def delta(a, b):
if a < b:
 return 1
else:
 return 0

The authors add delta as an symbolic operation so it isn't analyzed (otherwise, we would have just moved the nondeterminism to another place). The natural limit of this kind of refactoring, I think, is to allow any pure function (referentially transparent, side-effect free, whatever), to be a symbolic operation. I believe this would dramatically speed up analysis time. For instance, one of the examples that was analyzed by the authors was parallel matrix multiplication. The method of matrix multiplication is basically to have a master process that doles out column and row vectors to slave processes to compute the dot product. Dot product can be represented as a pure function, so we can represent the slave processes with very few states (just receive, dot product, send). We also end up with a much smaller expression table. The additional cost would be in analyzing which functions are actually free of side-effects (which, of course, we could avoid if we were using a better language).

Another difficulty is that, all though pure functions guarantee that for any input they will always produce the same output, the converse is obviously not true. Adding more operations to symbolic expressions makes for a coarser analysis. Thus, if we apply the aforementioned optimization, we may report that two programs are not equivalent when they really are. To compensate, we may have to introduce some more powerful reasoning to determine if outputs are actually equivalent. Unfortunately, this won't solve our problems, either: our path condition reasoning facilities also need to account for the function calls. In practice, however, I suspect that it would be easy to refactor code so that the bulk of the code lies in pure functions and we wouldn't have to worry too much about this.

All in all, not a bad paper. I don't know enough about the area to know which of the authors' ideas are really original, but at least it was a good read. I'd say the only real problems are the lack of automated model construction and that the approach doesn't seem to be scalable. It appears to work, however - the authors ran the analysis on 4 sample programs and found an error in one of them.