Re: Formal definitions

"Ira Baxter" <>
Sat, 10 Oct 2009 11:26:57 -0500

          From comp.compilers

Related articles
Formal definitions (Tim Frink) (2009-10-09)
Re: Formal definitions (Ira Baxter) (2009-10-10)
| List of all articles for this month |

From: "Ira Baxter" <>
Newsgroups: comp.compilers
Date: Sat, 10 Oct 2009 11:26:57 -0500
Organization: Compilers Central
References: 09-10-009
Keywords: optimize, theory
Posted-Date: 10 Oct 2009 23:08:58 EDT

"Tim Frink" <> wrote in message
> I'm looking for books/papers/websites where compiler optimizations
> are formally defined, i.e. not just textual and a code example.
> Any hints?

One answer is source-to-source program transformation systems, in
which pairs of target-language surface syntax patterns are written to
encode the transformation as a rewrite of the source text of the
program, e.g., pattern1 ==> pattern2

Stratego and TXL and Fermat are tools in
which such source-to-source transformations are entirely coded in
special rule langauges. Simple transformations that are context-free
can be coded directly. Taking into account context is harder and
requires cooperating sets of rules. Since rewrites are
generalizations of arbitrary string replaces, they are generalizations
of Post systems and thus can accomplish any transformation in theory.

Stratego and TXL can be applied to any langauge. Fermat is limited to
WSL, a language with formally defined semantics, but admits parsers
for other langauge that map to and from WSL.

Like Stratego and TXL,
has a rewrite rule language. However, it uses standard
compiler technology method to collect the context information
(symbol tables, control and data flow analyses) of
interest to transformations. Because context is so
important, as a practical matter,
many DMS transformations are written as
          pattern1 ==> pattern2 if condition
where the condition inspects some of the collected context
data. Similarly, rewrites aren't always a good
way to express transformations; DMS also
allows one to code complex transformations
procedurally (such as lambda lifting,
clone removal, ...)

Now transformations for a "compiler" are often from a programming
language level to a machine code level "langage". To the extent that
one can explicitly model both languages in the pattern language, it
can be handled directly by pattern rewriter. Stratego, TXL and DMS
can all do this easily. Stratego and TXL do this by allowing the
constructing a (joint) union grammar for source and target langauges,
with built in operators that compose grammars. DMS does this by
allowing disjoint unions of grammars so no grammer composition is
needed. One simply writes patterns in each of the languages and tags
the pattern according the grammar for which it applies.

One question that occurs over and over, is, "are the transformations
correct?" and "can you formally prove it?" Since the semantics of
the languages being transformed are not well-defined ina formal sense
(anybody seen denotational semantics for C++?) the answer to "can you
prove it" as a practical matter is outright NO. Are they correct?
Well, after rigourous testing, they are as correct as any other
program you might write. The Fermat system attempts to make
provability at least possible by insisting on the use of WSL, which is
formally defined. Of course, this simply pushes the burden on the
translator from your language X, which doesn't have formal semantics,
to WSL :-{

As an aside, I often get asked, "if you can't prove the
transformations correct, how you trust the tool?". My response is,
"if you aren't going to use a tool, then you going to use Joe to do
it, right? How can you trust Joe?".

Ira Baxter, CTO

Post a followup to this message

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