Inference of reference immutability

Download: PDF, Quinonez thesis, Javarifier implementation.

“Inference of reference immutability” by Jaime Quinonez, Matthew S. Tschantz, and Michael D. Ernst. In ECOOP 2008 — Object-Oriented Programming, 22nd European Conference, (Paphos, Cyprus), July 9-11, 2008, pp. 616-641.
An extended version appeared as “Inference of Reference Immutability in Java” by Jaime Quinonez. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2008.
A tool description appeared as “Tools for enforcing and inferring reference immutability in Java” by Telmo Luis Correa Jr., Jaime Quinonez, and Michael D. Ernst. In Companion to Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2007), (Montréal, Canada), October 23-25, 2007, pp. 866-867.

Abstract

Javari is an extension of Java that supports reference immutability constraints. Programmers write readonly type qualifiers and other constraints, and the Javari type-checker detects mutation errors (incorrect side effects) or verifies their absence. While case studies have demonstrated the practicality and value of Javari, a barrier to usability remains. A Javari program will not typecheck unless all the references in the APIs of libraries it uses are annotated with Javari type qualifiers. Manually converting existing Java libraries to Javari is tedious and error-prone.

We present an algorithm for inferring reference immutability in Javari. The flow-insensitive and context-sensitive algorithm is sound and produces a set of qualifiers that typecheck in Javari. The algorithm is precise in that it infers the most readonly qualifiers possible; adding any additional readonly qualifiers will cause the program to not typecheck. We have implemented the algorithm in a tool, Javarifier, that infers the Javari type qualifiers over a set of class files.

Javarifier automatically converts Java libraries to Javari. Additionally, Javarifier eases the task of converting legacy programs to Javari by inferring the mutability of every reference in a program. In case studies, Javarifier correctly inferred mutability over Java programs of up to 110 KLOC.

Download: PDF, Quinonez thesis, Javarifier implementation.

BibTeX entry:

@inproceedings{QuinonezTE2008,
   author = {Jaime Quinonez and Matthew S. Tschantz and Michael D. Ernst},
   title = {Inference of reference immutability},
   booktitle = {ECOOP 2008 --- Object-Oriented Programming, 22nd European
	Conference},
   pages = {616--641},
   address = {Paphos, Cyprus},
   month = {July~9--11,},
   year = {2008}
}

(This webpage was created with bibtex2web.)

Back to Program Analysis Group publications.