Towards modular verification of concurrent object-oriented programs

Speaker: Marieke Huisman

Abstract:

Modular static verification of concurrent object-oriented programs remains a challenge. This talk discusses the impact of concurrency on the use of standard program-logic-based verification techniques.

Atomicity of methods is often advocated as a solution to the problem of verification of multithreaded programs. However, we show that in a design-by-contract framework atomicity in itself is not sufficient, because it does not consider specifications. Instead, we propose to use the notion of stability of method contracts, to allow sound modular reasoning about method calls. A contract is stable if it cannot be broken by interferences from concurrent threads.

We explain why stability of contracts cannot always be shown directly, and we speculate about different approaches to prove stability. One approach that we will detail further is the use of an annotation system to describe object capacities and locking policies. The annotation system can be used to specify how many threads simultaneously can access an object. The annotation system distinguishes between read-write accesses and read-only accesses, thus offering fine-grained concurrency control. The locking policy of an object describes which locks must be held, before accessing it. The annotation system can express how ownership may be transferred or split between different threads.

The information that is given by the annotations can be exploited to verify other properties of the application. In particular, if an object is known to be local to a thread, sequential verification techniques can be used to verify functional correctness of its methods. We finish by outlining how a proof obligation generator for sequential programs can be extended to one for concurrent programs by using stability information.

This talk does not present a full technical solution to the problem, but instead describes work in progress. It shows how the verification problem can be decomposed into several smaller subproblems. For each subproblem, a solution is sketched, but the technical details still need to be worked out.