Non-interference and local correctness in transactional memory

DOI10.1016/J.TCS.2016.06.021MaRDI QIDQ2357153zbMATH OpenOpenAlexFDO

Authors Petr Kuznetsov, Sathya Peri

Publication date 19 June 2017

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2016.06.021

zbMATH Keywords

correctness criterionnon-interferenceopacitypermissivenesssoftware transactional memory

Mathematics Subject Classification ID

Distributed systems (68M14) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Correctness of concurrent executions of closed nested transactions in transactional memory systems
• scientific article; zbMATH DE number 7075928
• Privatization-safe transactional memories
• Towards formally specifying and verifying transactional memory
• Transactional Memory: Glimmer of a Theory

Cites work

• A theory of reliability in database systems
• A Versatile STM Protocol with Invisible Read Operations That Satisfies the Virtual World Consistency Condition
• Defining liveness
• Disjoint-access-parallel implementations of strong shared memory primitives
• Inherent limitations on disjoint-access parallel implementations of transactional memory
• Permissiveness in Transactional Memories
• The serializability of concurrent database updates

Cited in

(8)

• An efficient approach to achieve compositionality using optimized multi-version object based transactional systems
• Last-use opacity: a strong safety property for transactional memory with prerelease support
• An Abort-Aware Model of Transactional Programming
• Correctness of concurrent executions of closed nested transactions in transactional memory systems
• Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)
• On avoiding spare aborts in transactional memory
• scientific article; zbMATH DE number 7075928 (Why is no real title available?)
• Achieving starvation-freedom with greater concurrency in multi-version object-based transactional memory systems

Describes a project that uses

Uses Software

• NOrec

This page was built for publication: Non-interference and local correctness in transactional memory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2357153)