Please use this identifier to cite or link to this item: http://buratest.brunel.ac.uk/handle/2438/13188
Title: Towards linking correctness conditions for concurrent objects and contextual trace refinement
Authors: Dongol, B
Groves, L
Issue Date: 2016
Citation: Electronic Proceedings in Theoretical Computer Science, 209: pp. 107 - 111, (2016)
Abstract: Correctness conditions for concurrent objects describe how atomicity of an abstract sequential object may be decomposed. Many different concurrent objects and proof methods for them have been developed. However, arguments about correctness are conducted with respect to an object in isolation. This is in contrast to real-world practice, where concurrent objects are often implemented as part of a programming language library (e.g., java.util.concurrent) and are instantiated within a client program. A natural question to ask, then is: How does a correctness condition for a concurrent object ensure correctness of a client program that uses the concurrent object? This paper presents the main issues that surround this question and provides some answers by linking different correctness conditions with a form of trace refinement.
URI: http://bura.brunel.ac.uk/handle/2438/13188
DOI: http://dx.doi.org/10.4204/EPTCS.209.8
ISSN: 2075-2180
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
FullText.pdf153.9 kBAdobe PDFView/Open


Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.