Making Lock-free Data Structures Verifiable with Artificial Transactions

Created by W.Langdon from gp-bibliography.bib Revision:1.3973

@InProceedings{Yuan:2015:PLOS,
  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, 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}",
}

Genetic Programming entries for Xinhao Yuan David Williams-King Junfeng Yang Simha Sethumadhavan

Citations