Enforcing resource bounds via static verification of dynamic checks

Abstract

We classify existing approaches to resource-bounds checking as static or dynamic. Dynamic checking performs checks during program execution, while static checking performs them before execution. Dynamic checking is easy to implement but incurs runtime cost. Static checking avoids runtime overhead but typically involves difficult, often incomplete program analyses. In particular, static checking is hard in the presence of dynamic data and complex program structure. We propose a new resource management paradigm that offers the best of both worlds. We present language constructs that let the code producer optimize dynamic checks by placing them either before each resource use, or at the start of the program, or anywhere in between. We show how the code consumer can then statically verify that the optimized dynamic checks enforce his resource bounds policy. We present a practical language that is designed to admit decidable yet efficient verification and prove that our procedure is sound and optimal. We describe our experience verifying a Java implementation of tar for resource safety. Finally, we outline how our method can improve the checking of other dynamic properties. © Springer-Verlag Berlin Heidelberg 2005.