SPLASH 2011
Fri 21 - Thu 27 October 2011 Portland, Oregon, United States

Although existing annotation checker based on Fractional Permissions is powerful, it causes great space and runtime overhead. To address this issue, we propose to use a multi-layered approach for checking annotations. In addition to the heavyweight permission checker, we use two lightweight checkers: a conservative checker for those obviously correct cases, and a liberal checker for those obviously wrong cases. The type system for the conservative checker is more high-level, albeit less precise. To prove its soundness, we piggy-pack its proof to that of fractional permission, which is already proven sound. We also plan to implement both checkers on Fluid, an analysis framework for Java programs, and use various benchmarks to compare the performance of both approach.