Reducing loads and stores in stack architectures

The stack model of execution uses a stack to hold temporary results during evaluation of a program. Systems such as Java virtual machines that use this model can be implemented so that they have more efficient access to the stack than to local variables. Thus, converting local variable accesses into stack accesses can improve the performance of stack-based programs, as suggested by the experiments of Koopman [1994], Maierhofer and Ertl [1998], Vallée-Rai et al. [2000], and Shpeisman and Tikir [1999]. In this paper we provide a foundation for these experiments by formalizing and generalizing various known transformations for reducing the number of loads and stores, and by proving their correctness.