Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
Proving Linearizability of Concurrent Queues
View through CrossRef
<p>Linearizability is a commonly accepted correctness criterion for concurrent data structures. Concurrent queues are among the most fundamental concurrent data structures. In this paper, we present necessary and sufficient conditions for proving linearizability of concurrent queues, which make use of linearization of dequeue operations. The verification conditions intuitively express the “FIFO” semantics of concurrent queues and can be verified just by reasoning about the happened-before order of operations. We have successfully applied the proof technique to prove several challenging concurrent queues. We believe that our proof technique can be extended to the concurrent data structures which have the ordering requirements when their elements are removed.</p>
<p> </p>
Computer Society of the Republic of China
Title: Proving Linearizability of Concurrent Queues
Description:
<p>Linearizability is a commonly accepted correctness criterion for concurrent data structures.
Concurrent queues are among the most fundamental concurrent data structures.
In this paper, we present necessary and sufficient conditions for proving linearizability of concurrent queues, which make use of linearization of dequeue operations.
The verification conditions intuitively express the “FIFO” semantics of concurrent queues and can be verified just by reasoning about the happened-before order of operations.
We have successfully applied the proof technique to prove several challenging concurrent queues.
We believe that our proof technique can be extended to the concurrent data structures which have the ordering requirements when their elements are removed.
</p>
<p> </p>.
Related Results
Proving Linearizability Using Linearizations of Delete Operations
Proving Linearizability Using Linearizations of Delete Operations
Abstract
Linearizability is a commonly accepted correctness criterion for concurrent data structures. Concurrent queues and stacks are among themost fundamental concurrent ...
Linearizability on hardware weak memory models
Linearizability on hardware weak memory models
Abstract
Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for p...
Linearizability with Ownership Transfer
Linearizability with Ownership Transfer
Linearizability is a commonly accepted notion of correctness for libraries of
concurrent algorithms. Unfortunately, it assumes a complete isolation between a
library and its client...
A double blind placebo controlled homoeopathic proving of Malus domestica 30CH, with a subsequent comparative analysis according to the doctrine of signatures
A double blind placebo controlled homoeopathic proving of Malus domestica 30CH, with a subsequent comparative analysis according to the doctrine of signatures
The purpose of this research study was to determine any therapeutic significance of Malus domestica (domestic apple) in the potentised, homoeopathic form and to contribute this inf...
A homoeopathic drug proving of Bitis atropos with a subsequent comparison to venom toxicology and related remedies
A homoeopathic drug proving of Bitis atropos with a subsequent comparison to venom toxicology and related remedies
This study was a homoeopathic drug proving of Bitis atropos 30CH (derived from Berg adder venom) with a subsequent comparison of the proving symptoms to known venom toxicology and ...
Understanding the Missing Links in Hahnemann's Posology for Drug Proving
Understanding the Missing Links in Hahnemann's Posology for Drug Proving
AbstractHahnemannian drug proving has been reproved and clinically verified in multiple geographical locations in the last two centuries. They continue to be the most reliable and ...
A homoeopathic drug proving of Bitis atropos and a subsequent comparison of results with that of existing proven remedies of the Genus Bitis
A homoeopathic drug proving of Bitis atropos and a subsequent comparison of results with that of existing proven remedies of the Genus Bitis
Introduction The aim of this study was to investigate the homeopathic potential of Bitis atropos 30CH (Homoeopathically prepared Berg adder venom) and to compare the materia medica...
Concurrent dengue infections: Epidemiology & clinical implications
Concurrent dengue infections: Epidemiology & clinical implications
Multiple dengue virus (DENV) serotypes circulating in a geographical area most often lead to simultaneous infection of two or more serotypes in a single individual. The occurrence ...