Leveraging garbage collection to dynamically infer heap invariants
First Claim
1. A method of inferring heap invariants for program objects maintained by a program in heap memory, comprising:
- causing the program to execute over a period in an execution environment having a heap memory managed using garbage collection;
creating meta data to track a set of invariants to be inferred about the program objects created by the program in the heap memory, wherein the invariants are properties of the program objects which do not vary during execution of the program;
upon a vitality check of the program objects in a garbage collection pass and during the garbage collection pass;
traversing objects in the heap memory to determine, for each object which is traversed, whether the object is reachable;
for each object in the heap memory that is traversed, as the object is traversed to determine if it is reachable, checking whether the set of invariants to be inferred about the object remain satisfied, and updating the meta data based on results of the checking;
producing data reporting the invariants satisfied by the program objects in the heap memory during the period of execution of the program;
generating an annotated program, wherein generating the annotated program comprises writing static annotations to the source code for the program specifying the invariants reported to be satisfied by at least some of the program objects in the heap memory;
compiling the annotated program with edits to the source code into an edited program; and
reporting occurrences of anomalies in which the invariants are violated by the edited program in a period of execution of the edited program at least by comparing the invariants specified by the static annotations in the source code and invariants reported in the period of execution of the edited program.
2 Assignments
0 Petitions
Accused Products
Abstract
A program analysis tool leverages the garbage collection process to dynamically infer invariants of objects or data structures created by a program on the heap during execution. During execution of the program in a garbage-collected execution environment, the program analysis tool tracks object allocations made by the program, and records some meta data relating to invariants tracked for the type of the object, which are initially assumed satisfied by the object. Whenever a garbage collection pass visits the object, the tool checks whether the object still satisfies the invariants, and updates the meta data accordingly. The tool finally reports the invariants reflected by the meta data upon the object'"'"'s death or at termination of the program. The invariants can then be used to annotate the program source code and/or detect bugs that violate the invariants.
-
Citations
15 Claims
-
1. A method of inferring heap invariants for program objects maintained by a program in heap memory, comprising:
-
causing the program to execute over a period in an execution environment having a heap memory managed using garbage collection; creating meta data to track a set of invariants to be inferred about the program objects created by the program in the heap memory, wherein the invariants are properties of the program objects which do not vary during execution of the program; upon a vitality check of the program objects in a garbage collection pass and during the garbage collection pass; traversing objects in the heap memory to determine, for each object which is traversed, whether the object is reachable; for each object in the heap memory that is traversed, as the object is traversed to determine if it is reachable, checking whether the set of invariants to be inferred about the object remain satisfied, and updating the meta data based on results of the checking; producing data reporting the invariants satisfied by the program objects in the heap memory during the period of execution of the program; generating an annotated program, wherein generating the annotated program comprises writing static annotations to the source code for the program specifying the invariants reported to be satisfied by at least some of the program objects in the heap memory; compiling the annotated program with edits to the source code into an edited program; and reporting occurrences of anomalies in which the invariants are violated by the edited program in a period of execution of the edited program at least by comparing the invariants specified by the static annotations in the source code and invariants reported in the period of execution of the edited program. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10)
-
-
11. Computer-readable computer program-carrying physical storage having instructions which, when executed by a computer, cause the computer to perform the actions of a program analysis tool by performing analysis of a program under test to infer heap invariants of program objects maintained by said program under test in heap memory, the performing analysis of a program under test comprising:
-
performing the actions of a heap executive by providing a heap allocator application programming interface service to allocate memory space in heap memory upon request from said program under test; performing the actions of a garbage collector by; periodically performing a garbage collection pass over program objects created by said program under test in heap memory; and testing liveness of the program objects; and performing the actions of an invariant inference service operating across and outside of an execution of said program under test by; maintaining meta data tracking a set of invariant inferences per program object, wherein the invariant inferences are inferences that an invariant property of the respective object does not vary during execution of the program; at the time the garbage collector tests liveness of a program object, checking that the program object continues to satisfy the invariant inferences tracked for the respective object; and producing a report indicating the invariant properties satisfied by the program objects across the execution of said program under test; and
reporting occurrences of anomalies in which the invariants are violated by the program with edited source code in a subsequent execution of the edited program at least by comparing the reported invariant properties satisfied by the program objects and invariant properties reported in the subsequent period of execution of the edited program. - View Dependent Claims (12, 13, 14)
-
-
15. A computer implementing a dynamic program analysis system for inferring heap invariants of program objects maintained by a program in heap memory, the system comprising:
-
one or more physical computer processors; and computer memory containing computer-executable instructions executing on the one or more computer processors causing the computer to perform a method, the method comprising; causing the program to execute over a period in an execution environment having a heap memory managed using garbage collection; creating meta data to track a set of invariants to be inferred about the program objects created by the executing program in the heap memory, wherein the meta data is created based on the types of the program objects; holding the metadata in an area of memory that is not managed by the garbage collection; when creating the meta data, initializing the meta data of the program objects to indicate the invariants are satisfied by the program objects; responsive to a vitality check of the program objects during a garbage collection pass; traversing objects in the heap memory to determine, for each object which is traversed, whether the object is reachable; for each object that is traversed, as the object is traversed to determine if it is reachable, checking whether the set of invariants to be inferred about the program object remain satisfied and updating the meta data based on results of the checking; updating the meta data to indicate the invariant was not satisfied by a program object, when the checking determines that an invariant is not satisfied by the program object; and if the object is no longer reachable, as the object is reclaimed, performing a final update of the meta data based on results of said checking; responsive to termination of the program execution; updating the meta data of the objects that remain on the heap; logging the final state of the invariant inferences for each object remaining on the heap; producing data, based on the logging, reporting the invariants satisfied by the program objects over the period of execution of the program; and adding static annotations to the source code of the program specifying the invariants reported to be satisfied by at least some of the program objects in the heap memory of the executing program; compiling an annotated program with edits to the source code into an edited program; and reporting occurrences of anomalies in which invariants are violated by the edited program in a period of execution of the compiled edited program, by comparing the invariants specified by the static annotations in the source code and the invariants reported in the period of execution of the compiled edited program.
-
Specification