Please use this identifier to cite or link to this item: http://bura.brunel.ac.uk/handle/2438/14970
Full metadata record
DC FieldValueLanguage
dc.contributor.authorDerrick, J-
dc.contributor.authorDoherty, S-
dc.contributor.authorDongol, B-
dc.contributor.authorSchellhorn, G-
dc.contributor.authorTravkin, O-
dc.contributor.authorWehrheim, H-
dc.date.accessioned2017-07-27T12:22:02Z-
dc.date.available2017-07-27T12:22:02Z-
dc.date.issued2017-
dc.identifier.citationFormal Aspects of Computing, (2017)en_US
dc.identifier.issn0934-5043-
dc.identifier.urihttp://bura.brunel.ac.uk/handle/2438/14970-
dc.description.abstractSoftware transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as atomic blocks. This atomicity property is captured by a correctness criterion called opacity, which relates the behaviour of an STM implementation to those of a sequential atomic specification. In this paper, we prove opacity of a recently proposed STM implementation: the Transactional Mutex Lock (TML) by Dalessandro et al. For this, we employ two different methods: the first method directly shows all histories of TML to be opaque (proof by induction), using a linearizability proof of TML as an assistance; the second method shows TML to be a refinement of an existing intermediate specification called TMS2 which is known to be opaque (proof by simulation). Both proofs are carried out within interactive provers, the first with KIV and the second with both Isabelle and KIV. This allows to compare not only the proof techniques in principle, but also their complexity in mechanization. It turns out that the second method, already leveraging an existing proof of opacity of TMS2, allows the proof to be decomposed into two independent proofs in the way that the linearizability proof does not.en_US
dc.language.isoenen_US
dc.publisherSpringeren_US
dc.subjectSoftware transactional memoryen_US
dc.subjectOpacityen_US
dc.subjectVerificationen_US
dc.subjectRefinementen_US
dc.subjectKIVen_US
dc.subjectIsabelleen_US
dc.titleMechanized proofs of opacity: A comparison of two techniquesen_US
dc.typeArticleen_US
dc.relation.isPartOfFormal Aspects of Computing-
pubs.publication-statusAccepted-
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf1.51 MBAdobe PDFView/Open


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