PDF《Beyond Contracts for Concurrency》

Under consideration for publication in Formal Aspects of Computing Beyond Contracts for Concurrency Jonathan S.

Ostro?1 , Faraz Ahmadi Torshizi1 , Hai Feng Huang1 and Bernd Schoeller2 1Dept. of Computer Science and Engineering, York University,

4700 Keele Street, Toronto, Canada M3J 1P3

2 Software Engineering ETH Zurich Clausiusstrasse

59 CH-8092 Zurich Abstract. SCOOP is a concurrent programming language with a new semantics for contracts that applies equally well in concurrent and sequential contexts. SCOOP eliminates race conditions and atomicity viola- tions by construction. However, it is still vulnerable to deadlocks. In this paper we describe how far contracts can take us in verifying interesting properties of concurrent system using modular Hoare rules and show how theorem proving methods developed for sequential Ei?el can be extended to the concurrent case. However, some safety and liveness properties depend upon the environment and cannot be proved using the Hoare rules. To deal with such system properties, we outline a SCOOP Virtual Machine (SVM) as a fair transition system. The SVM makes it feasible to use modelchecking and theorem proving methods for checking global temporal logic properties of SCOOP programs. The SVM uses the Hoare rules where applicable to reduce the number of steps in a computation. Keywords: SCOOP (Simple Concurrent Object Oriented programming), Concurrent Contracts, Opera- tional Semantics, Veri?cation, Temporal Logic. 1. Introduction Sequential programming has a widely accepted set of ideas such as standard control and data structuring techniques, modularity, and information hiding constructs that now appear in object-oriented languages such as Java and C#. There is also an increasing recognition that Design by Contract (DbC) plays an important role in documenting the contracts between classes [Mey97, BLS02]. In DbC, each class is described by a class invariant as well as preconditions and postconditions for each feature (i.e. method or attribute). DbC is part of the Ei?el language and DbC extensions to Java (e.g. JML) and C# (e.g. Spec#) have now been developed so as to make use of this speci?cation facility for class interfaces [LLM06, BCD+ 05, BDF+ 04, BDJ+ 05, BLS04, BCC+ 03, FLL+ 02, JLPS05, LLP+ 00, LM99, LM06]. Correspondence and o?print requests to: {jonathan, faraz, hhuang}@cse.yorku.ca, bernd.schoeller@inf.ethz.ch. This work was conducted under an NSERC Discovery grant.

2 Jonathan S. Ostro?, Faraz Ahmadi Torshizi, Hai Feng Huang and Bernd Schoeller The advantage of object-oriented information hiding and contracting mechanisms is that they allow developers to reason statically about the code without the need to consider a vast number of program executions that can occur at run-time. With DbC, developers can reason about code modularly. Furthermore, contracts are checked dynamically at runtime (via runtime assertion checking) and are therefore useful for testing the correctness of code. The authors of [BLS02] study the use of contracts in practice in order to assess the bene?ts of doing so for the isolation of faults. Their study shows that instrumenting code with contracts is a powerful lightweight method for detecting bugs and isolating faults. Concurrency The situation is somewhat di?erent when it comes to object-oriented concurrent programming. Increasingly, software developers use some variant of concurrency (multithreading, multiprocessing, distributed computing, and web services). But the techniques commonly used to produce concurrent applications are still elementary and often haphazard. The explicit speci?cation and control of low-level parallelism in multithreading models such as Java is a source of new programming errors. Concurrency introduces problems such as data races, atomicity violations and deadlock that make the development and debugging of such software di?cult and the resulting products are much more error prone than sequential products. The release of new multi-core CPUs has also stimulated software companies to seek new concurrent languages. Adding more cores to a chip is only half the battle. As stated in [Bie07], the next tricky stage is for software developers to ?gure out how to program quad cores concurrently so as to avoid the deadlock bug and solve another type of parallel-programming problem called a race bug . In addition, there is the challenge of extending DbC to the concurrent setting. The standard Hoare rules may fail to apply and more complex calculi are often non-modular making it di?cult for use by the developers. A suitable concurrency model is clearly needed that provides basic safety and liveness guarantees and that shields programmers from common mistakes and errors, or at the very least detects data races, atomicity violations and deadlocks. One approach is to extend DbC to the concurrent setting as has been done by JML and Spec#. In [RDF+ 05], JML is extended to allow for the speci?cation of multi-threaded Java programs. Method guards are speci?ed using the when keyword. If a feature is called in a state where the guard does not hold, the feature is supposed to block until the guard holds. The new constructs rely on the non-interference notion of method atomicity, and allow developers to specify locking and other non-interference properties of methods. Atomicity enables the speci?cation of method pre- and postconditions and supports Hoare-style modular reasoning about methods. The above keyword is useful in static veri?cation but programmers are still forced to write the synchronization keyword by hand. As pointed out in [JLPS05], developing safe multithreaded software systems is di?cult due to the potential unwanted interference among concurrent threads. In [JLPS05], the Spec# boogie methodology is extended to the concurrent case. The paper presents a method that protects object structures against inconsistency due to race conditions, where developers de?ne aggregate object structures using an ownership system and declare invariants over them. The methodology is supported by a set of language elements and by both a sound modular static veri?cation method and run-time checking support. The method thus ensures freedom from data races and atomicity violations but does not yet treat properties such as freedom from deadlock and other liveness properties. The JML and Spec# approaches are both based on DbC. Java PathFinder (JPF) [HP00] takes a di?erent approach. JPF takes Java programs (no contracts) as input and provides an impressive veri?cation environ- ment for detecting deadlocks and assertion violations integrating program analysis and model checking. The following quote from [VHB+ 03] is instructive: Although it is hard to quantify the exact size of program that JPF can currently handle C small programs might have large state-spaces C we are routinely analyzing programs in the 1,000 to 5,000 line range ... it is naive to believe that model checking will be capable of analyzing programs of 100,000 lines or more ... Further progress has been made in the mean time and, undoubtedly, these new methods will be scaled up to handle larger and more realistic examples. Even the ability to analyze small critical chunks of realistic code is a welcome addition to bug detection. Nevertheless, it appears that we will still need to rely on testing for the foreseeable future, with formal veri?cation as a helpful technique for ?nding additional bugs. Beyond Contracts for Concurrency