Hdl Handle:
http://hdl.handle.net/10149/58317
Title:
A CSP model of Eiffel's SCOOP
Authors:
Brooke, P. J. (Phillip); Paige, R. F. (Richard); Jacob, J. L. (Jeremy)
Affiliation:
University of Teesside. School of Computing; University of York. Department of Computer Science.
Citation:
Brooke, P. J., Paige, R. F. and Jacob, J. L. (2007) 'A CSP model of Eiffel's SCOOP', Formal Aspects of Computing, 19 (4), pp.487-512.
Publisher:
Springer Verlag
Journal:
Formal Aspects of Computing
Issue Date:
Nov-2007
URI:
http://hdl.handle.net/10149/58317
DOI:
10.1007/s00165-007-0033-8
Abstract:
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.
Type:
Article
Keywords:
concurrency; formal methods; programming languages; Eiffel; SCOOP
ISSN:
0934-5043
Rights:
Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 4/12/09]
Citation Count:
4 [Scopus, 4/12/209]

Full metadata record

DC FieldValue Language
dc.contributor.authorBrooke, P. J. (Phillip)-
dc.contributor.authorPaige, R. F. (Richard)-
dc.contributor.authorJacob, J. L. (Jeremy)-
dc.date.accessioned2009-04-01T10:48:52Z-
dc.date.available2009-04-01T10:48:52Z-
dc.date.issued2007-11-
dc.identifier.citationFormal Aspects of Computing; 19(4): 487-512-
dc.identifier.issn0934-5043-
dc.identifier.doi10.1007/s00165-007-0033-8-
dc.identifier.urihttp://hdl.handle.net/10149/58317-
dc.description.abstractThe 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.-
dc.publisherSpringer Verlag-
dc.rightsAuthor can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 4/12/09]-
dc.subjectconcurrency-
dc.subjectformal methods-
dc.subjectprogramming languages-
dc.subjectEiffel-
dc.subjectSCOOP-
dc.titleA CSP model of Eiffel's SCOOP-
dc.typeArticle-
dc.contributor.departmentUniversity of Teesside. School of Computing; University of York. Department of Computer Science.-
dc.identifier.journalFormal Aspects of Computing-
ref.assessmentRAE 2008-
ref.citationcount4 [Scopus, 4/12/209]-
or.citation.harvardBrooke, P. J., Paige, R. F. and Jacob, J. L. (2007) 'A CSP model of Eiffel's SCOOP', Formal Aspects of Computing, 19 (4), pp.487-512.-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.