2011 | OriginalPaper | Chapter
Verification of Scalable Synchronous Queue
Authors : Jinjiang Lei, Zongyan Qiu
Published in: Certified Programs and Proofs
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Lock-free algorithms are extremely hard to be built correct due to their fine-grained concurrency natures. Formal techniques for verifying them are crucial. We present a framework for verification of CAS-based lock-free algorithms, and prove a nontrivial lock-free algorithm
Scalable Synchronous Queue
that is practically adopted in Java 6. The strength of our approach lies on that it relieves the dependence on auxiliary variables/commands, thus is relatively easier to conduct and comprehend, comparing to existing works.