编辑: 达达恰西瓜 | 2019-07-16 |
3 This paper In this paper, we focus on SCOOP (Simple Concurrent Object-Oriented Programming). SCOOP was origi- nally proposed by Bertrand Meyer [Mey97] with some subsequent attempts to re?ne or implement the model [Com00, FOP04]. The work of Piotr Nienaltowski [Nie07] is a signi?cant step forward in improving the com- putational model and providing and a working implementation which includes a library which implements the model (SCOOPLI ) and a compiler (scoop2scoopli) which type checks SCOOP code and translates it into pure threaded Ei?el1 . SCOOP programs are free of data races and atomicity violations by construction. However, there is no guarantee of freedom from deadlocks. Although the notion of Design by Contract is di?erent to that of sequential Ei?el, contracts in SCOOP permit the application of sequential reasoning techniques to the concurrent programs. In this paper, we explore just how far sequential reasoning takes us and what is needed for verifying arbitrary temporal logic properties of SCOOP programs beyond contracts. The paper proceeds as follows: ? In Section
2 we discuss the di?erence between sequential Ei?el and SCOOP programs and provide a simple example (class DATA) of how theorem proving would work via Hoare reasoning in the sequential case. ? In Section
3 we provide an informal discussion of the SCOOP computational model using a simple example C zero-one C to motivate the discussion. The sequential class DATA is re-used in this example without the need to make any changes to it for the concurrent case. The Hoare reasoning rule for the concurrent case as described in [Nie07] may be used to verify termination and the contracts of the controlled routines using a theorem prover already in use for sequential Ei?el. The capabilities and the limits of Hoare reasoning are presented. Temporal logic is used to express system properties that are beyond the capabilities of the Hoare rule to verify. ? In Section
4 we provide the outline of a SCOOP Virtual Machine (SVM) together with its operational semantics as a fair transition system. The SVM uses the Hoare rules where applicable to reduce the number of steps in a computation. The SVM can be used as the formal basis for expressing temporal logic properties and for building tools based on modelcheckers and theorem provers to verify safety and liveness properties. 2. Sequential and Concurrent Computation Object-oriented computation (sequential or concurrent) is performed via the mechanism of the feature call t.r(x). If target t is attached to some object obj then a processor may invoke the routine r with argument x on the object obj. In the sequential case, there is only one processor. In the concurrent case, we have two or more processors. A processor is an autonomous thread of control capable of supporting the sequential execution of instructions for one or more objects. This de?nition assumes that the processor is some device, which can be implemented either in hardware (e.g. a computer equipped with its own central processor), or as software (e.g. a thread, task or stream). Hence, a processor in this context is an abstraction and we may assume the availability of an unlimited number of processors. 2.1. A Simple Sequential Class Class DATA (Fig. 1) is a simple exa........