Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1275497.1275503 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
dynamic,static verifier,static,dynamic check,resource bounds,static verification,efficient static verifier,hoisting reserve operation,reserve operation,enforcing resource bound,resource usage,dynamic checking,combining reserve operation,static analysis,hoare logic,security,languages | Programming language,Programmer,Computer science,Hoare logic,Static analysis,Hoist (device),Resource allocation,Security policy,Boolean expression,Java | Journal |
Volume | Issue | ISSN |
29 | 5 | 0164-0925 |
ISBN | Citations | PageRank |
3-540-25435-8 | 27 | 1.56 |
References | Authors | |
22 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ajay Chander | 1 | 213 | 12.60 |
| David Espinosa | 2 | 32 | 2.07 |
| Nayeem Islam | 3 | 27 | 1.56 |
| Peter Lee 0001 | 4 | 975 | 147.71 |
| George Necula | 5 | 2427 | 180.97 |