Synthesis of Resource Invariants for Concurrent Programs

Owicki and Gries have developed a proof system for conditional critical regions. In their system, logically related variables accessed by more than one process are grouped together as resources, and processes are allowed access to a resource only in a critical region for that resource. Proofs of synchronization properties are constructed by devising predicates called resource invariants which describe relationships among the variables of a resource when no process is in a critical region for the resource. In constructing proofs using the system of Owicki and Gries, the programmer is required to supply the resource invariants. Methods are developed in this paper for automatically synthesizing resource invariants. Specifically, the resource invariants of a concurrent program are characterized as least fixpoints of a functional which can be obtained from the text of the program. By the use of this fixpoint characterization and a widening operator based on convex closure, good approximations may be obtained for the resource invariants of many concurrent programs.