Immutability specification and its applications

A location is said to be immutable if its value and the values of selected locations reachable from it are guaranteed to remain unchanged during a specified time interval. We introduce a framework for immutability specification, and discuss its application to code optimization. Compared to a final declaration, an immutability assertion in our framework can express a richer set of immutability properties along three dimensions - lifetime, reachability and context. We present a framework for processing and verifying immutability annotations in Java, as well as extending optimizations so as to exploit immutability information. Preliminary experimental results show that a significant number (82%) of read access could potentially be classified as immutable in our framework. Further, use of immutability information yields substantial reductions (33% to 99%) in the number of dynamic read accesses, and also measurable speedups in the range of 5% to 10% for certain benchmark programs.