Memory Usage Verification for OO Programs

Memory Usage Verification for OO Programs,10.1007/11547662_7,Wei-ngan Chin,Huu Hai Nguyen,Shengchao Qin,Martin C. Rinard

Memory Usage Verification for OO Programs   (Citations: 32)
BibTex | RIS | RefWorks Download
We present a new type system for an object-oriented (OO) language that characterizes the sizes of data structures and the amount of heap memory required to successfully execute methods that operate on these data structures. Key components of this type system include type assertions that use symbolic Presburger arithmetic expressions to capture data structure sizes, the effect of methods on the data structures that they manipulate, and the amount of memory that methods allocate and deallocate. For each method, we conservatively capture the amount of memory required to execute the method as a function of the sizes of the method's inputs. The safety guarantee is that the method will never attempt to use more memory than its type expressions specify. We have implemented a type checker to verify memory usages of OO programs. Our experience is that the type system can precisely and effectively capture memory bounds for a wide range of programs. Memory management is a key concern for many applications. Over the years researchers have developed a range of memory management approaches; examples include explicit allocation and deallocation, copying garbage collection, and region-based memory al- location. However, an important aspect that has been largely ignored in past work is the safe estimation of memory space required for program execution. Overallocation of memory may cause inefficiency, while underallocation may cause software failure. In this paper, we attempt to make memory usage more predictable by static verification on the memory usage of each program. We present a new type system, based on dependent type(21), that characterizes the amount of memory required to execute each program component. The key components of this type system include: - Data Structure Sizes and Size Constraints: The type of each data structure in- cludes index parameters to characterize its size properties, which are expressed in terms of the sizes of data structures that it contains. In many cases the sizes of these data structures are correlated; our approach uses size constraints expressed using symbolic Presburger arithmetic terms to precisely capture these correlations.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: