NDLI: The semantics of progress in lock-based transactional memory

Please wait, while we are loading the content...

Language constructs for transactional memory

A calculus of atomic actions

Static contract checking for Haskell

Modular code generation from synchronous block diagrams: modularity vs. code size

A foundation for flow-based program matching: using temporal logic and model checking

Wild control operators

Lazy evaluation and delimited control

A cost semantics for self-adjusting computation

Semi-sparse flow-sensitive pointer analysis

Equality saturation: a new approach to optimization

Linear types for computational effects

Unifying type checking and property checking for low-level code

State-dependent representation independence

The semantics of x86-CC multiprocessor machine code

Types and higher-order recursion schemes for verification of higher-order programs

Proving that non-blocking algorithms don't block

Masked types for sound object initialization

Formal certification of code-based cryptographic proofs

SPEED: precise and efficient static estimation of program computational complexity

Bidirectionalization for free! (Pearl)

Copy-on-write in the PHP language

A combination framework for tracking partition sizes

Positive supercompilation for a higher order call-by-value language

Local rely-guarantee reasoning

Modeling abstract types in modules with open existential types

Relaxed memory models: an operational approach

Verifying distributed systems: the operational approach

A model of cooperative threads

Flexible types: robust type inference for first-class polymorphism

Verifying liveness for asynchronous programs

Automatic modular abstractions for linear constraints

The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer

Feedback-directed barrier optimization in a strongly isolated STM

The theory of deadlock avoidance via discrete control

Compositional shape analysis by means of bi-abduction

Classical BI: a logic for reasoning about dualising resources

Focusing on pattern matching

The semantics of progress in lock-based transactional memory

Automated verification of practical garbage collectors

The semantics of progress in lock-based transactional memory

Content Provider	ACM Digital Library
Author	Kapalka, Michal Guerraoui, Rachid
Abstract	Transactional memory (TM) is a promising paradigm for concurrent programming. Whereas the number of TM implementations is growing, however, little research has been conducted to precisely define TM semantics, especially their progress guarantees. This paper is the first to formally define the progress semantics of lockbased TMs, which are considered the most effective in practice. We use our semantics to reduce the problems of reasoning about the correctness and computability power of lock-based TMs to those of simple try-lock objects. More specifically, we prove that checking the progress of any set of transactions accessing an arbitrarily large set of shared variables can be reduced to verifying a simple property of each individual (logical) try-lock used by those transactions. We use this theorem to determine the correctness of state-of-the-art lock-based TMs and highlight various configuration ambiguities. We also prove that lock-based TMs have consensus number 2. This means that, on the one hand, a lock-based TM cannot be implemented using only read-write memory, but, on the other hand, it does not need very powerful instructions such as the commonly used compare-and-swap. We finally use our semantics to formally capture an inherent trade-off in the performance of lock-based TM implementations. Namely, we show that the space complexity of every lock-based software TM implementation that uses invisible reads is at least exponential in the number of objects accessible to transactions.
Starting Page	404
Ending Page	415
Page Count	12
File Format	PDF
ISBN	9781605583792
DOI	10.1145/1480881.1480931
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2009-01-21
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Impossibility Lower bound Reduction Semantics Consensus number Try-lock Lock Transactional memory
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

The semantics of progress in lock-based transactional memory

The semantics of progress in lock-based transactional memory (2009)

The semantics of progress in lock-based transactional memory (2009)

The Semantics of Progress and Concurrency in Distributed Transactional Memory Systems

Against lock-based semantics for transactional memory

On obstruction-free transactions

Inherent limitations on disjoint-access parallel implementations of transactional memory

Towards Transactional Memory Semantics for C (2009)

On the correctness of transactional memory

The semantics of progress in lock-based transactional memory

Similar Documents

The semantics of progress in lock-based transactional memory

The semantics of progress in lock-based transactional memory (2009)

The semantics of progress in lock-based transactional memory (2009)

The Semantics of Progress and Concurrency in Distributed Transactional Memory Systems

Against lock-based semantics for transactional memory

On obstruction-free transactions

Inherent limitations on disjoint-access parallel implementations of transactional memory

Towards Transactional Memory Semantics for C (2009)

On the correctness of transactional memory

The semantics of progress in lock-based transactional memory