Copenhagen Programming Language Seminar


Preconditions and Specialization: Basis for Modular Array Checks Optimization

Corneliu Popeea,
National University of Singapore

Monday, August 30, 15:15-16:15
DIKU, Universitetsparken 1, room N010


We propose a modular inference mechanism, based on an advanced type system with Presburger arithmetic, to help identify array checks that can be safely eliminated. Our proposal works for a core imperative language with assignments, and can discover symbolic program states (or postconditions) to support the elimination of redundant checks. Our inference is modular as it is able to process each method independently, and yet exploit the different contexts of its multiple callers. We achieve this by converting each partially-safe check into a precondition that is propagated up its callers' sites for further inference. This approach provides for a highly accurate interprocedural optimization. The results of our modular inference can be used by a program specialization phase that can maximise the elimination of safe checks. We have implemented a prototype inference system and have also proven its soundness. Initial experiments suggest that such an inference system can be both accurate and scalable.

Scientific host: Robert Glück. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org