NDLI: Verifying linearizability with hindsight

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

Transactional predication: high-performance concurrent sets and maps for STM

The k-bakery: local-spin k-exclusion using non-atomic reads and writes

Brief announcement: view transactions: transactional model with relaxed consistency checks

Verifying linearizability with hindsight

Brief announcement: towards robust medium access in multi-hop networks

Non-blocking binary search trees

Adaptive system anomaly prediction for large-scale hosting infrastructures

Efficient distributed random walks with applications

Brief announcement: the price of anarchy for distributed network formation in an adversary model

Meeting the deadline: on the complexity of fault-tolerant continuous gossip

Brief announcement: on the quest of optimal service ordering in decentralized queries

Finding mobile data under delay constraints with searching costs

Broadcasting in unreliable radio networks

Distributed algorithms for edge dominating sets

Brief announcement: asynchronous bounded expected delay networks

Deterministic distributed vertex coloring in polylogarithmic time

The inherent complexity of transactional memory and what to do about it

On maintaining multiple versions in STM

Group mutual exclusion in O(log n) RMR

Brief announcement: single-version permissive STM

Eventually linearizable shared objects

Brief announcement: routing with obstacle avoidance mechanism with constant approximation ratio

Adaptive randomized mutual exclusion in sub-logarithmic expected time

Efficient threshold detection in a distributed environment: extended abstract

On the theoretical gap between synchronous and asynchronous MPC protocols

Brief announcement: swarming secrets

A new technique for distributed symmetry breaking

Brief announcement: network traffic can optimize consolidation during transformation to virtualization

On utilizing speed in networks of mobile agents

Discrete load balancing is (almost) as easy as continuous load balancing

Fast flooding over Manhattan

Brief announcement: locally-accessible implementations for distributed shared memory multiprocessors

Breaking the $O(n^{2})$ bit barrier: scalable byzantine agreement with an adaptive adversary

Distributed computational complexities: are you volvo-addicted or nascar-obsessed?

The multiplicative power of consensus numbers

On asymmetric progress conditions

Brief announcement: NUMA-aware transactional memory

The topology of shared-memory adversaries

Brief announcement: ART--sub-logarithmic decentralized range query processing with probabilistic guarantees

Distributed data classification in sensor networks

Forbidden-set distance labels for graphs of bounded doubling dimension

Hybrid-secure MPC: trading information-theoretic robustness for computational privacy

Brief announcement: distributed trust management and revocation

On the computational power of oblivious robots: forming a series of geometric patterns

Brief announcement: distributed almost stable marriage

Expansion and the cover time of parallel random walks

Locating a target with an agent guided by unreliable local advice: how to beat the random walk when you have a clock?

Bayesian ignorance

Brief announcement: capacity of byzantine agreement with finite link capacity - complete characterization of four-node networks

Optimal gradient clock synchronization in dynamic networks

A certain freedom: thoughts on the CAP theorem

Brief announcement: actions in the twilight - concurrent irrevocable transactions and inconsistency repair

Brief announcement: pan and scan

Partial information spreading with application to distributed maximum coverage

Brief announcement: realizing secure multiparty computation on incomplete networks

Brief announcement: decentralized construction of multicast trees embedded into P2P overlay networks based on virtual geometric coordinates

Rapid randomized pruning for fast greedy distributed algorithms

Brief announcement: a framework for building self-stabilizing overlay networks

Online set packing and competitive scheduling of multi-part tasks

Brief announcement: on enhancing concurrency in distributed transactional memory

Brief announcement: complexity and solution of the send-receive correlation problem

Brief announcement: anonymity and trust in distributed systems

Brief announcement: deterministic dominating set construction in networks with bounded degree

Brief announcement: revisiting the power-law degree distribution for social graph analysis

How to meet when you forget: log-space rendezvous in arbitrary graphs

Brief announcement: queuing or priority queuing? on the design of cache-coherence protocols for distributed transactional memory

Brief announcement: distributed contention resolution in wireless networks

Brief announcement: secret sharing based on the social behaviors of players

Brief announcement: tree decomposition for faster concurrent data structures

Brief announcement: collusion free protocol for rational secret sharing

A modular approach to shared-memory consensus, with applications to the probabilistic-write model

Brief announcement: k-shot distributed broadcasting in radio networks

Brief announcement: sources of instability in data center multicast

Brief announcement: improving social-network-based sybil-resilient node admission control

Brief announcement: efficient graph algorithms without synchronization

Brief announcement: leader election vs pattern formation

Constant RMR solutions to reader writer synchronization

Brief announcement: a shared disk on distributed storage

Brief announcement: superpeer formation amidst churn and rewiring

Brief announcement: communication efficient asynchronous byzantine agreement

Brief announcement: the accuracy of tree-based counting in dynamic networks

Brief announcement: monotonic stabilization

Brief announcement: on L-resilience, hitting sets, and colorless tasks

Brief announcement: self-monitoring in dynamic wireless networks

Brief announcement: perfectly secure message transmissiontolerating mobile mixed adversary with reduced phase complexity

Brief announcement: adaptive content placement for peer-to-peer video-on-demand systems

Brief announcement: modelling MapReduce for optimal execution in the cloud

Brief announcement: an efficient failure detector for omission environments

Brief announcement: exponential speed-up of local algorithms using non-local communication

Verifying linearizability with hindsight

Content Provider	ACM Digital Library
Author	O'Hearn, Peter W. Yahav, Eran Yorsh, Greta Rinetzky, Noam Vechev, Martin T.
Abstract	We present a proof of safety and linearizability of a highly-concurrent optimistic set algorithm. The key step in our proof is the Hindsight Lemma, which allows a thread to infer the existence of a global state in which its operation can be linearized based on limited local atomic observations about the shared state. The Hindsight Lemma allows us to avoid one of the most complex and non-intuitive steps in reasoning about highly concurrent algorithms: considering the linearization point of an operation to be in a different thread than the one executing it. The Hindsight Lemma assumes that the algorithm maintains certain simple invariants which are resilient to interference, and which can themselves be verified using purely thread-local proofs. As a consequence, the lemma allows us to unlock a perhaps-surprising intuition: a high degree of interference makes non-trivial highly-concurrent algorithms in some cases much easier to verify than less concurrent ones.
Starting Page	85
Ending Page	94
Page Count	10
File Format	PDF
ISBN	9781605588889
DOI	10.1145/1835698.1835722
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-07-25
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Hindsight Optimistic concurrency Linearizability Wait-freedom
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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