Program Equivalence (was Interesting summary of compiler optimzation testing)

Mon, 15 Jun 87 10:00:56 EDT

          From comp.compilers

Related articles
Program Equivalence (was Interesting summary of compiler optimzation t harvard!rochester!costanzo (1987-06-15)
| List of all articles for this month |

From: harvard!rochester!costanzo
Date: Mon, 15 Jun 87 10:00:56 EDT
Newsgroups: comp.compilers
In-Reply-To: <1750@ames.UUCP>
Organization: U of Rochester, CS Dept, Rochester, NY

>From: (Rich A. Hammond)
>Subject: Testing optimizing compilers
>I'd love to have a program that could compare two assembly language
>programs and decide that they functioned identically, but I view that
>as harder than writing the optimizer to begin with.

It's not harder, it's easier. Namely because it's impossible.
Program equivalence is, in general, an unsolvable problem.
Program A outputs a 3 and halts.
Program B loops forever.

Clearly Programs A and B don't function identically, but, in general,
a program cannot be written to tell us that. In particular, we cannot
tell that Program B loops forever (this is the Halting Problem).
[It's certainly true that the halting problem is in general undecidable,
but that doesn't preclude the possibility that an interesting subset of
the problem can be solved. In the case above, for example, static analysis
might find that program B has no statement that could output a 3, and so
prove that that particular pair of programs aren't the same. The general
field of proving programs correct seems to me to consist of proving that a
program is equivalent to a specification that is considered correct by
definition. Perhaps there's some interesting stuff there. -John]
UUCP: ..!{allegra,decvax,seismo}!rochester!costanzo
USnail: CS Dept., University of Rochester, Rochester NY 14627
Phone: (716)275-7747 Spoken: Hey You!


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.