Assaad, Medhat G. and Leavens, Gary T. (2001) Alias-free Parameters in C for Better Reasoning and Optimization. Technical Report 01-11, Computer Science, Iowa State University.
Aliasing among formal parameters and among formals and globals causes problems for both reasoning and optimization. Whole-program static analysis could provide some knowledge about such aliasing, but this is not usually done, and in any case would have to be conservative. All aliasing patterns that are not ruled out by an analysis have to be considered possible both by a person reasoning about correctness and by a compiler trying to optimize code. For compilers, the conservative nature of the static analysis leads to missed optimization opportunities.
We have designed and implemented a small extension to C that partially solves the reasoning problem and leads to significantly better optimization. The extension guarantees that there will be no direct aliasing among arguments and globals inside procedure bodies, and yet allows aliasing among arguments and globals at the call site. This is done by having multiple bodies for each procedure, up to one for each aliasing pattern. Procedure calls are automatically dispatched to the body that matches the run-time aliasing pattern among the actual parameters and the globals.
We present experimental evidence that this approach is practical. It is easy to convert existing C code, because not every procedure in a program has to be converted, and because converted code can call code that has not been converted and vice versa. By following simple guidelines, one can convert a program in a way that usually makes it run faster than before. In our experiments with 6 of the SPEC 2000 integer benchmarks we found an average speedup of about 5%. In one case, we had a speedup of about 29%.
|Keywords:||Aliasing, multibody procedures, dynamic dispatch, static dispatch, program verification, alias-free programs, compiler optimizations, ACL approach, C/ACL language, C language|
|Subjects:||Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)|
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Software: PROGRAMMING LANGUAGES: Processors
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
|Deposited by:||Gary T. Leavens on 19 November 2001|
|Alternative Locations:||ftp://ftp.cs.iastate.edu/pub/techreports/TR01-11/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR01-11/TR.ps.gz |
Contact site administrator at: firstname.lastname@example.org