ACL--Eliminating Parameter Aliasing with Dynamic Dispatch

Abstract

<p>In this article we present a method for eliminating reference parameter aliases. The goal is to allow procedure calls with parameters being aliases, and at the same time guarantees that procedure bodies are alias-free. The method is to automatically dispatch to the correct procedure body based on the particular alias combination among actual parameters. Automating finding the alias combination makes writing verifiable programs verification simpler since code to find the combination is not explicitly present in client programs. The number of necessary procedure bodies is usually small which makes th eapproach practical. Efficiency of the dispatch is estimated to be no worse than in other languages.</p>