Xinhao Yuan
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.
- Boost::Lockfree. http://www.boost.org/doc/libs/1_55_0/doc/html/lockfree.html.Google Scholar
- Folly C++ library. http://github.com/facebook/folly.Google Scholar
- Java's lock-free concurrency. http://www.pwendell.com/2012/08/13/java-lock-free-deepdive.html.Google Scholar
- liblfds. http://liblfds.org.Google Scholar
- Lock-free code: A false sense of security. http://www.drdobbs.com/cpp/lock-free-code-a-false-sense-of-security/210600279.Google Scholar
- Are all of the new concurrent collections lock-free? http://blogs.msdn.com/b/pfxteam/archive/2010/01/26/9953725.aspx.Google Scholar
- nbds. http://nbds.googlecode.com.Google Scholar
- Pyevolve. http://pyevolve.sourceforge.net/.Google Scholar
- Aba problem on wikipedia. http://en.wikipedia.org/wiki/ABA_problem.Google Scholar
- Transactional synchronization in haswell. https://software.intel.com/en-us/blogs/2012/02/07/transactional-synchronization-in-haswell, 2012.Google Scholar
- C. Blundell, E. C. Lewis, and M. M. Martin. Subtleties of transactional memory atomicity semantics. Computer Architecture Letters, 5(2):17--17, 2006. Google ScholarDigital Library
- S. Burckhardt, R. Alur, and M. M. Martin. Checkfence: checking consistency of concurrent data types on relaxed memory models. In ACM SIGPLAN Notices, volume 42, pages 12--21. ACM, 2007. Google ScholarDigital Library
- S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan. Line-up: a complete and automatic linearizability checker. In ACM Sigplan Notices, volume 45, pages 330--340. ACM, 2010. Google ScholarDigital Library
- L. Ceze, J. Tuck, P. Montesinos, and J. Torrellas. Bulksc: Bulk enforcement of sequential consistency. In Proceedings of the 34th Annual International Symposium on Computer Architecture, ISCA '07, pages 278--289, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-706-3. URL http://doi.acm.org/10.1145/1250662.1250697. Google ScholarDigital Library
- C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '05, pages 110--121, New York, NY, USA, 2005. ACM. ISBN 1-58113-830-X. URL http://doi.acm.org/10.1145/1040305.1040315. Google ScholarDigital Library
- P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996. ISBN 3540607617. Google ScholarCross Ref
- P. Godefroid. Model checking for programming languages using verisoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '97, pages 174--186, New York, NY, USA, 1997. ACM. ISBN 0-89791-853-3. URL http://doi.acm.org/10.1145/263699.263717. Google ScholarDigital Library
- H. Guo, M. Wu, L. Zhou, G. Hu, J. Yang, and L. Zhang. Practical software model checking via dynamic interface reduction. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, SOSP '11, pages 265--278, New York, NY, USA, 2011. ACM. ISBN 978-1-4503-0977-6. URL http://doi.acm.org/10.1145/2043556.2043582. Google ScholarDigital Library
- D. Hendler, N. Shavit, and L. Yerushalmi. A scalable lock-free stack algorithm. In Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures, pages 206--215. ACM, 2004. Google ScholarDigital Library
- M. Herlihy and J. E. B. Moss. Transactional memory: Architectural support for lock-free data structures, volume 21. ACM, 1993. Google ScholarDigital Library
- Intel. Intel 64 and IA-32 Architectures Software Developer's Manual Volume 1: Basic Architecture, June 2014.Google Scholar
- Intel. Intel 64 and IA-32 Architectures Optimization Reference Manual, March 2014.Google Scholar
- C. Killian, J. W. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the 4th USENIX Conference on Networked Systems Design & Implementation, NSDI'07, pages 18--18, Berkeley, CA, USA, 2007. USENIX Association. URL http://dl.acm.org/citation.cfm?id=1973430.1973448. Google ScholarDigital Library
- C. Lattner and V. Adve. Llvm: A compilation framework for life-long program analysis & transformation. In Code Generation and Optimization, 2004. CGO 2004. International Symposium on, pages 75--86. IEEE, 2004. Google ScholarDigital Library
- B. Lucia, J. Devietti, K. Strauss, and L. Ceze. Atom-aid: Detecting and surviving atomicity violations. In Proceedings of the 35th Annual International Symposium on Computer Architecture, ISCA '08, pages 277--288, Washington, DC, USA, 2008. IEEE Computer Society. ISBN 978-0-7695-3174-8. URL http://dx.doi.org/10.1109/ISCA.2008.4. Google ScholarDigital Library
- M. M. Michael. Aba prevention using single-word instructions. IBM Research Division, RC23089 (W0401-136), Tech. Rep, 2004.Google Scholar
- M. M. Michael. Scalable lock-free dynamic memory allocation. ACM Sigplan Notices, 39(6):35--46, 2004. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '07, pages 446--455, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-633-2. URL http://doi.acm.org/10.1145/1250734.1250785. Google ScholarDigital Library
- M. Musuvathi, D. Y. W. Park, A. Chou, D. R. Engler, and D. L. Dill. Cmc: A pragmatic approach to model checking real code. SIGOPS Oper. Syst. Rev., 36(SI):75--88, Dec. 2002. ISSN 0163-5980. URL http://doi.acm.org/10.1145/844128.844136. Google ScholarDigital Library
- C. Norris IP and D. L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1-2):41--75, 1996. ISSN 0925-9856. URL http://dx.doi.org/10.1007/BF00625968. Google ScholarDigital Library
- J. Simsa, R. Bryant, and G. Gibson. dbug: Systematic evaluation of distributed systems. In Proceedings of the 5th International Conference on Systems Software Verification, SSV'10, pages 3--3, Berkeley, CA, USA, 2010. USENIX Association. URL http://dl.acm.org/citation.cfm?id=1929004.1929007. Google ScholarDigital Library
- N. Sinha and C. Wang. Staged concurrent program analysis. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, pages 47--56. ACM, 2010. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engineering, 10(2):203--232, 2003. ISSN 0928-8910. URL http://dx.doi.org/10.1023/A%3A1022920129859. Google ScholarDigital Library
- M. Yabandeh, N. Knezevic, D. Kostic, and V. Kuncak. Crystalball: Predicting and preventing inconsistencies in deployed distributed systems. In NSDI, volume 9, pages 229--244, 2009. Google ScholarDigital Library
- J. Yang, C. Sar, and D. Engler. Explode: A lightweight, general system for finding serious storage system errors. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7, OSDI '06, pages 10--10, Berkeley, CA, USA, 2006. USENIX Association. URL http://dl.acm.org/citation.cfm?id=1267308.1267318. Google ScholarDigital Library
- J. Yang, P. Twohey, D. Engler, and M. Musuvathi. Using model checking to find serious file system errors. ACM Trans. Comput. Syst., 24(4):393--423, Nov. 2006. ISSN 0734-2071. URL http://doi.acm.org/10.1145/1189256.1189259. Google ScholarDigital Library
- J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long, L. Zhang, and L. Zhou. Modist: Transparent model checking of unmodified distributed systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI'09, pages 213--228, Berkeley, CA, USA, 2009. USENIX Association. URL http://dl.acm.org/citation.cfm?id=1558977.1558992. Google ScholarDigital Library
Index Terms
- Making lock-free data structures verifiable with artificial transactions
Recommendations
Making Lock-free Data Structures Verifiable with Artificial Transactions
Special TopicsAmong 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 ...
Lock-free Transactions without Rollbacks for Linked Data Structures
SPAA '16: Proceedings of the 28th ACM Symposium on Parallelism in Algorithms and ArchitecturesNon-blocking data structures allow scalable and thread-safe accesses to shared data. They provide individual operations that appear to execute atomically. However, it is often desirable to execute multiple operations atomically in a transactional ...
Lock-Free Transactional Transformation for Linked Data Structures
Special Issue on SPAA 2016Nonblocking data structures allow scalable and thread-safe access to shared data. They provide individual operations that appear to execute atomically. However, it is often desirable to execute multiple operations atomically in a transactional manner. ...
Comments