Sat, 10 Oct 2009 11:26:57 -0500

Related articles |
---|

Formal definitions plfriko@yahoo.de (Tim Frink) (2009-10-09) |

Re: Formal definitions idbaxter@semdesigns.com (Ira Baxter) (2009-10-10) |

From: | "Ira Baxter" <idbaxter@semdesigns.com> |

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" <plfriko@yahoo.de> 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 http://en.wikipedia.org/wiki/Stratego/XT and TXL

http://en.wikipedia.org/wiki/TXL_(programming_language) and Fermat

http://en.wikipedia.org/wiki/FermaT_Transformation_System 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,

DMS http://en.wikipedia.org/wiki/DMS_Software_Reengineering_Toolkit

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

www.semanticdesigns.com

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.