@inproceedings{lockit:plos15,
    author = "Yuan, Xinhao and Williams-King, David and Yang, Junfeng and Sethumadhavan, Simha",
    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 TXIT, 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.",
    ids = "xinhao:plos15",
    title = "Making Lock-free Data Structures Verifiable with Artificial Transactions",
    booktitle = "Proceedings of the 8th Workshop on Programming Languages and Operating Systems (PLOS)",
    pages = "39--45",
    doi = "10.1145/2818302.2818309",
    pdfurl = "https://dl.acm.org/doi/pdf/10.1145/2818302.2818309",
    month = "October",
    year = "2015"
}