A CSP model of Eiffel's SCOOP

P.J. Brooke; R.F. Paige; J.L. Jacob

doi:10.1007/s00165-007-0033-8

A CSP model of Eiffel's SCOOP

P.J. Brooke, R.F. Paige, J.L. Jacob

Computer Science

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	487-512
Number of pages	25
Journal	Formal Aspects of Computing
Volume	19
Issue number	4
DOIs	https://doi.org/10.1007/s00165-007-0033-8
Publication status	Published - Nov 2007

Keywords

concurrency
formal methods
programming languages
Eiffel
SCOOP

Access to Document

10.1007/s00165-007-0033-8

http://dx.doi.org/10.1007/s00165-007-0033-8

Cite this

@article{30855425ba484ab6a41b28498cf2afd9,

title = "A CSP model of Eiffel's SCOOP",

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.",

keywords = "concurrency, formal methods, programming languages, Eiffel, SCOOP",

author = "P.J. Brooke and R.F. Paige and J.L. Jacob",

year = "2007",

month = nov,

doi = "10.1007/s00165-007-0033-8",

language = "English",

volume = "19",

pages = "487--512",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Springer",

number = "4",

}

TY - JOUR

T1 - A CSP model of Eiffel's SCOOP

AU - Brooke, P.J.

AU - Paige, R.F.

AU - Jacob, J.L.

PY - 2007/11

Y1 - 2007/11

N2 - 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.

AB - 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.

KW - concurrency

KW - formal methods

KW - programming languages

KW - Eiffel

KW - SCOOP

U2 - 10.1007/s00165-007-0033-8

DO - 10.1007/s00165-007-0033-8

M3 - Article

SN - 0934-5043

VL - 19

SP - 487

EP - 512

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 4

ER -