CSR----SMA Modular Pluggable Program Analyses

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

Developers of program analyses today face an uncomfortable choice: produce a precise analysis that can extract or verify quite sophisticated properties (but fails to scale to large programs) or produce an efficient analysis that scales well (but extracts or verifies only very basic properties). The unfortunate consequence is that the potential benefits of precise program analysis (detecting programming errors, verifying that the program preserves its data structure consistency properties, enhanced ability to extract meaningful design information, etc.) are currently denied to the large programs that need them the most. The project will pursue a new approach that enables the focused application of multiple analyses to different instantiable modules in the same program, with each analysis applied to the modules for which it is most appropriate. Each module encapsulates one or more data structures and uses membership in abstract sets to specify how the actions of each module affect the participation of objects in its data structures. Each analysis verifies that the implementation of the analyzed module 1) preserves important internal data structure representation invariants and 2) conforms to a specification that uses formulas in a set algebra to characterize the effects of operations on the data structure. Each analysis will use an abstraction function to establish the connection between the concrete data structure implementation and abstract set membership. This abstraction function enables the analysis to translate the set membership properties of objects that cross module boundaries back into concrete data structure properties within the module. These properties are crucial to verifying that the data structures remain consistent and that each module correctly implements its abstract set interface. Systems often have consistency properties that involve multiple modules. For example, a system may require the sets of objects that participate in two given modules to be disjoint. Because these properties involve objects shared across multiple modules, different analyses must somehow interoperate if they are to successfully verify the property. In the approaches pursued here , these kinds of invariants are expressed using a boolean algebra of abstract set inclusion properties and locally verified at the appropriate program points by each analysis. This approach therefore eliminates the need to apply complex (and potentially unscalable) analyses across large regions of the program.