A CSP model of Eiffel's SCOOP

The current informal semantics of the simple concurrent object-oriented programming (SCOOP) mechanism for Eiffel is described. We construct and discuss a model using the process algebra CSP. This model gives a more formal semantics for SCOOP than existed previously. We implement the model mechanical...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2007-11, Vol.19 (4), p.487-512
Main Authors: BROOKE, Phillip J, PAIGE, Richard F, JACOB, Jeremy L
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Geometry
Global analysis, analysis on manifolds
Mathematics
Miscellaneous
Sciences and techniques of general use
Theoretical computing
Topology. Manifolds and cell complexes. Global analysis and analysis on manifolds
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The current informal semantics of the simple concurrent object-oriented programming (SCOOP) mechanism for Eiffel is described. We construct and discuss a model using the process algebra CSP. This model gives a more formal semantics for SCOOP than existed previously. We implement the model mechanically via a new tool called CSPsim. We examine two semantic variations of SCOOP: when and how far to pass locks, and when to wait for child calls to complete. We provide evidence that waiting for child calls to complete both unnecessarily reduces parallelism without any increase in safety and increases deadlocks involving callbacks. Through the creation and analysis of the model, we identify a number of ambiguities relating to reservations and the underlying run-time system and propose means to resolve them.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-007-0033-8