Igarashi: Created page with "Loop fusion—a program transformation to merge multiple consecutive loops into a single one—has been studied mainly for compiler optimization. In this paper, we propose a n..."

2018-05-21T00:39:48Z

Created page with "Loop fusion—a program transformation to merge multiple consecutive loops into a single one—has been studied mainly for compiler optimization. In this paper, we propose a n..."

New page

Loop fusion—a program transformation to merge multiple
consecutive loops into a single one—has been studied mainly
for compiler optimization. In this paper, we propose a new
loop fusion strategy, which can fuse any loops—even loops
with data dependence—and show that it is useful for program
verification because it can simplify loop invariants.

The crux of our loop fusion is the following observation: if
the state after the first loop were known, the two loop bodies
could be computed at the same time without suffering from
data dependence by renaming program variables. Our loop
fusion produces a program that guesses the unknown state
after the first loop nondeterministically, executes the fused
loop where variables are renamed, compares the guessed
state and the state actually computed by the fused loop,
and, if they do not match, diverges. The last two steps of
comparison and divergence are crucial to preserve partial
correctness. We call our approach “guess-and-assume” be-
cause, in addition to the first step to guess, the last two steps
can be expressed by the pseudo-instruction assume, used in
program verification.

We formalize our loop fusion for a simple imperative lan-
guage and prove that it preserves partial correctness. We
further extend the “guess-and-assume” technique to revers-
ing loop execution, which is useful to verify a certain type of
consecutive loops. Finally, we confirm by experiments that
our transformation techniques are indeed effective for state-
of-the-art model checkers to verify a few small programs
that they could not.

WG211/M18Igarashi - Revision history

Igarashi: Created page with "Loop fusion—a program transformation to merge multiple consecutive loops into a single one—has been studied mainly for compiler optimization. In this paper, we propose a n..."