2
$\begingroup$

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).

$\endgroup$
  • 2
    $\begingroup$ I fail to understand the question. Do you say that a+b and 2*c are equivalent because you can map both a and b to c? $\endgroup$ – Tsuyoshi Ito Aug 28 '11 at 19:35
  • 3
    $\begingroup$ @Grzegorz: do you mean en.wikipedia.org/wiki/Rewriting ? The general problem you seem to be describing would then be related to the word problem and would then be undecidable. $\endgroup$ – András Salamon Aug 28 '11 at 20:19
  • 4
    $\begingroup$ I do not understand the problem at all. What do you mean by 'structures'? What do you mean by 'answer'? What do you mean by 'transformation'? Can you use rigorous mathematical definitions please? Usually an algebraic structure is a carrier set with some operations on it obeying (algebra for a signature). Are you talking about one of these? $\endgroup$ – Ohad Kammar Aug 28 '11 at 22:12
  • 2
    $\begingroup$ (1) You removed the definition of equivalence. Please do not expect that the reader reads old revisions to understand the question. $\endgroup$ – Tsuyoshi Ito Aug 29 '11 at 12:37
  • 2
    $\begingroup$ In my opinion, you have to make up your mind about how to present your question. I understand that it is sometimes difficult especially if you have many ways to choose from, but it is important. Easily giving up one formulation and moving to another seems to me like you posted a problem without thinking about it carefully, and that is why I do not like a complete rewriting. I do not have a strong opinion about edit vs repost, but keep in mind that usually posting the same question twice is frowned upon. (more) $\endgroup$ – Tsuyoshi Ito Aug 29 '11 at 14:35
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ if it's true what you've wrote, that semantics community is not joining their efforts with compiler community - is a big shame that this happened... If someone knows examples of such cooperation, please make new answer. $\endgroup$ – Grzegorz Wierzowiecki Aug 29 '11 at 20:50
  • $\begingroup$ Good, you've mentioned model checking. So far I mostly tried to apply some methods used for propositional and predicate calculus, automated theorem proving (resolution, etc). But still curious about more. :) $\endgroup$ – Grzegorz Wierzowiecki Aug 29 '11 at 20:51
  • $\begingroup$ You've said it can be done in $O(n2^k)$ time, and mentioned about need of "non-trivial reasoning". That's what I'm looking for. I'd love to see how already people tried to deal with problem (approaches, heuristics - maybe approximations), and investigate it. $\endgroup$ – Grzegorz Wierzowiecki Aug 29 '11 at 20:52
  • $\begingroup$ You've mentioned "well investigated in various forms and approaches" - I would love to see references to read (or watched if video). $\endgroup$ – Grzegorz Wierzowiecki Aug 29 '11 at 20:52
  • 1
    $\begingroup$ I think I address now these comments in the text. Feel free to replace them with new ones. I'll see whether I can think of good references, but they are more in the form of textbooks than single papers and results! $\endgroup$ – Ohad Kammar Aug 29 '11 at 23:55
6
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.