- author = "Xinhao Yuan and David Williams-King and Junfeng Yang and Simha Sethumadhavan",
- title = "Making Lock-free Data Structures Verifiable with Artificial Transactions",
- booktitle = "Proceedings of the 8th Workshop on Programming Languages and Operating Systems, PLOS 2015",
- year = "2015",
- pages = "39--45",
- address = "Monterey, California, USA",
- month = "4-7 " # oct,
- publisher = "ACM",
- keywords = "genetic algorithms, genetic programming, genetic improvement, artificial transactions, lock-free data structures, software model checking, state space reduction, transactional memory, Concurrent Programming, Parallel programming, Software/Program Verification, Model checking, Performance Analysis and Design Aids, Design, Verification, Performance, Measurement",
- isbn13 = "978-1-4503-3942-1",
-
DOI = "
doi:10.1145/2818302.2818309",
-
URL = "
http://doi.acm.org/10.1145/2818302.2818309",
- acmid = "2818309",
-
abstract = "Among all classes of parallel programming
abstractions, lock-free data structures are considered
one of the most scalable and efficient thanks to their
fine-grained style of synchronization. However, they
are also challenging for developers and tools to verify
because of the huge number of possible interleavings
that result from fine-grained synchronizations.
This paper addresses this fundamental problem between performance and verifiability of lock-free data structure implementations. We present T_XIT, a system that greatly reduces the set of possible interleavings by inserting transactions into the implementation of a lock-free data structure. We leverage hardware transactional memory support from Intel Haswell processors to enforce these artificial transactions. Evaluation on six popular lock-free data structure libraries shows that TXIT makes it easy to verify lock-free data structures while incurring acceptable runtime overhead. Further analysis shows that two inefficiencies in Haswell are the largest contributors to this overhead.",
-
notes = "mysql, p40 'We implemented TXIT for C/C++ lock-free
data structures. It leverages the LLVM compiler [24] to
instrument programs and insert artificial transactions,
the Pyevolve genetic programming engine [8] to search
for an optimal transaction placement plan, the dBug
model checker [31] to systematically check schedules of
transactions, and TSX - the hardware transactional
memory support readily available in the 4th generation
Intel Core processors (codenamed Haswell) [10] -to
enforce artificial transactions (3).'
Columbia University
Also known as \cite{Yuan:2015:MLD:2818302.2818309}",
