Equivalence of two basic blocks

Question

My questions:

• What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for searching equivalence"?)
• what algorithms do you know solving this kind of problems?
• What papers/books do you recommend?

Problem

I'm interested in approaches of finding, whether two computations are equivalent?

I try to find my way between rewriting systems, automated theorem proving, logic programming, varieties, or just visiting graph of all possible basic block transformations (in order to find corresponding vertices (with some luck ;) ) ).

Of course. In finite domains, I could enumerate all possible inputs for all possible symbols permutations, check whether computations gives same results, and do this in finite time. I am looking for other approaches.

Computations

Computations are given as basic blocks represented in SSA - static single assignment form. We can assume finite number integer arithmetic (for example 64bit numbers). Computations run in RAM model.

For those not familiar with compilers theory and design, Basic Block has no jumps, no loops, no function call, one exit, and one entry etc. So we can say, that each execution of BB has O(1) complexity.

SSA - static single assignment form of basic block is DAG (Direct Acyclic Graph). In that sense, there is similar question on TCS.SE about unification theory and DAG isomorphism, while my context, focus, purpose and approach is different.

Equivalence

Let me be more specific what I mean by equivalence of computations. Let's take following setup:

• two computations $f$ and $g$ and treat them as functions.
• $P$ is a vector of $f$'s parameters $p_1, p_2, \ldots, p_n$
• $P' = \operatorname{perm}(P)$ is permutation of parameters.

By equivalence, I mean, there exist permutation $P'$ that for any inputs $P$ , we have $f(P) = g(P')$ same (vector of) results in both computations.

Another equivalence definition

I've just found, definition of basic block equivalence, very similar to mine. I hope it might clarify, what I mean by that.

Let me cite from C Decompilation: Is It Possible? by Katerina Troshina, Alexander Chernov and Yegor Derevenets:

Let $f$ be an object renaming transformation (...) $f(C_1) = C_2$ if there exists a renaming of named objects such as registers, labels, etc, preserving program semantics and making the programs $f(C_1)$ and $C_2$ syntactically indistinguishable. Existence of such an f transformation is a sufficient condition of program equivalence. (...) Equivalence of basic blocks may be checked by reducing them to a RISC-like representation. Let $h$ be a basic block reduction transformation. Let $B_1$ and $B_2$ be basic blocks, let $B'_1 = h(B_1)$ and $B'_2 = h(B_2)$ be the corresponding basic blocks in the RISC-like representation. Let $g$ be an instruction reordering transformation preserving the program semantics. If for the basic blocks $B_1$ and $B_2$ there exist transformations $f$ , $g$ and $h$ making $g(f(h(B_1))$ and $h(B_2)$ syntactically indistinguishable, basic blocks $B_1$ and $B_2$ are equivalent.

Although, their approach is more focused on assembly code, my approach is more in direction of path-algebra for algorithm pattern matching. What it implies, I'd like to take into account, not only instruction reordering, but equations they represent as well. (Simple example : $(a + b) / 2$ is different to $a / 2 + b / 2$ on $k$-bits integer computations - modular arithmetic. When $a + b \ge 2^k$ results are different. While algorithms, authors/implementators intentions might be the same. That's why I'd like to mix approaches from different fields).

Answer 1

The actual field you seem to be talking about is formal methods, and in particular, formal semantics of programming languages. The particular programming language you have (the machine language of the processor) seems to be without recursion and with some global state involved. This kind of effectful semantics has been well investigated in various forms and approaches.

The fields involved have developed so much that a full overview is out of the question. Also, these not only contain results, but tools employed to attack the difficulties inherent in establishing eqivalences. I will try to mentionsome keywords and topics.

One famous approach is that of axiomatic semantics. In this approach one interleaves the program with formulae from a prespecified logic, used to reason about the language. For example, in your case this logic might encode statements about the state of the processor's registers: $\exists n: r_1 =n \wedge r_2 >n^2+n-5$. These combine to form a logic (rigorous reasoning system), where statements have the form $\{\phi\}C\{\psi\}$. $\phi$ is a formula in this logic representing a precondition known about the state of the world prior to the execution of the program phrase $C$. $\psi$ is a formula representing the postcondition, guaranteed to be valid in state of the world (under the assumption that the precondition held).

The semantics is then given axiomatically as a collection of pre/post-conditions and inference rules. For instance, the semantics of register addition may look like this: $\{r_1 = n \wedge r_2 = m\} {\rm addi\ r3,r1,r2}\{r_3=m+n\}$. The inference rules may include rules for using intermediate formulae to compose smaller phrases into larger ones.

So in your case, you will need to show that for all preconditions and postconditions, the statement $\{\phi\}B_1\{\psi\}$ is valid iff $\{\phi\}B_2\{\psi\}$ is valid. There are several such systems, applied academically and industrially. The keywords are Hoare logic, separation logic, invariants.

Another approach is operational semantics. In this approach the meaning is given by an implementation of the language. It is desirable to give an abstract implementation, so that rigorous reasoning is possible. Nowadays it is also reasonable to expect this semantics to be structural: the operation of the machine is directed by the structure of the languages syntax, and the meaning of a composite program is given by the meaning of its components.

The implementation is commonly given as a transition system, where each state is a configuration containing the current program phrase that awaits execution. Some keywords and tools that are useful for your problem: structural operational semantics, structural induction, small-step and big-step semantics, observational equivalence, contextual equivalence.

A third approach is denotational semantics. In this, the meaning of a program phrase is given by a mathematical function of its components. This semantics tends to give a global understanding of the mathematical structure of the semantics. As a consequence, their presentation is a lot less elementary, and tend to lag behind the other approaches. On the other hand, this global understanding may give rise to deep insights about the behaviour and structure of the language. Some keywords: domain theory, category theory, monads, call-by-push-value.

The bottom line is that program equivalence has been investigated quite a lot. It is one of the most fundamental questions in semantics. In your case, determining algorithmically and tractably whether two such computations are equivalent will probably involve tools from model checking. Indeed, if you have $n$ registers of $k$ bits then the state-space has at least $n2^k$ points. An exhaustive search of this space is then $\Omega(n2^km)$ where $k$ is the length of the program. Of course, it might even be much worse than this. So I guess you'll need to employ some non-trivial reasoning to establish such equivalences. Some keywords: the state-space explosion, abstract and symbolic interpretation, normalization by evaluation.

Some places to start looking at things. The Handbook of Theoretical Computer Science (Volume B) has some chapters covering various topics in semantics (Chapters 7, 9, 11, 12, 15 and 19). By now these topics are taught to undergraduates in various universities, they usually concentrate on operational and axiomatic semantics (as they are more elementary). There is a related question about that here at TCS@SE.

I'm sorry for speaking in such broad terms, but the body of knowledge and tools underlying this problem is quite extensive. I hope that I at least given you somewhere to start looking!

It is a pet peeve of mine that the formal semantics community, who explores these questions inherent to compiler theory, have drifted apart from the compiler community. This is not entirely the semantics' community fault: first, as usual in TCS, a big body of theory needs to be developed before a substantial application is possible. Also, Moore's law and other advances in computer science allowed compiler writers to concentrate on other problems, and dismiss formal semantics as abstract nonsense. Another observation I heard from Paul Levy is that people from outside the community take interest because of the usefulness of the problems, and then become so fascinated with the theory that they join the community.

Finally, i'll mention that the gap is closing. There are researchers around the world from both communities that take interest in each other and in closing the gap. A few local names in the semantics world: Nick Benton, Gordon Plotkin, Peter Sewell.

Answer 2

The problem as you state it is extremely general and has been around in some form since the early days of computer science. For example, language equivalence of various kinds of machines is a kind of equivalence of computational devices.

That said, your question indicates you are interested in the equivalence of imperative programs. There are several ways and approaches to do this. One specific application of such work is to prove the correctness of compiler optimizations. Translation validation is another technical term you may want to look up.

The equivalence of two programs is a semantic property. It is difficult to check directly. A core idea behind many techniques is to find a structural property of programs (or the transition graphs they generate) that is easier to check and implies equivalence. For example, one may use bisimulation, simulation or related notions in a proof. The challenge is to lift these ideas from transition systems to the program text. Here are a few recent proposals in this area.

1. Proving Optimizations Correct using Parameterized Program Equivalence, Sudipta Kundu, Zachary Tatlock, and Sorin Lerner , PLDI 2009
2. A Formally Verified Compiler Back-end, Xavier Leroy, Journal of Automated Reasoning 2008.
3. Translation validation for an optimizing compiler, George Necula, PLDI 2000
4. Translation Validation, A. Pnueli , M. Siegel , F. Singerman , TACAS 1998.

There is much more. I am not an expert. I believe the third paper was an important position statement. The work of Xavier Leroy and Sorin Lerner would give you pointers to two different but very current approaches.