Peizhao Ou
Skip Abstract Section
Abstract
Concurrent data structures often provide better performance on multi-core processors but are significantly more difficult to design and test than their sequential counterparts. The C/C++11 standard introduced a weak memory model with support for low-level atomic operations such as compare and swap (CAS). While low-level atomic operations can significantly improve the performance of concurrent data structures, they introduce non-intuitive behaviors that can increase the difficulty of developing code.
In this paper, we develop a correctness model for concurrent data structures that make use of atomic operations. Based on this correctness model, we present CDSSPEC, a specification checker for concurrent data structures under the C/C++11 memory model. We have evaluated CDSSPEC on 10 concurrent data structures, among which CDSSPEC detected 3 known bugs and 93% of the injected bugs.
- ISO/IEC 14882:2011, Information technology -- programming languages -- C++.Google Scholar
- ISO/IEC 9899:2011, Information technology -- programming languages -- C.Google Scholar
- M. Abadi and L. Lamport. The existence of refinement mapping. Theoretical Computer Science, 82(2):253--284, May 1991. Google ScholarDigital Library
- P. A. Abdulla, S. Aronis, M. F. Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. Stateless model checking for TSO and PSO. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015. Google ScholarDigital Library
- S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. Computer, 29:66--76, 1996. Google ScholarDigital Library
- J. Alglave, D. Kroening, and M. Tautschnig. Partial orders for efficient bounded model checking of concurrent software. In Proceedings of the 25th International Conference on Computer Aided Verification, 2013. Google ScholarDigital Library
- J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: modelling, simulation, testing, and data-mining for weak memory. In Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014.Google Scholar
- D. Amit, N. Rinetzky, T. Reps, M. Sagiv, and E. Yahav. Comparison under abstraction for verifying linearizability. In Proceedings of the 19th International Conference on Computer Aided Verification, 2007. Google ScholarCross Ref
- M. Batty. The C11 and C++11 concurrency model. Ph.D. thesis, University of Cambridge, 2014.Google Scholar
- M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C++ concurrency. In Proceedings of the Symposium on Principles of Programming Languages, 2013. Google ScholarDigital Library
- M. Batty, A. F. Donaldson, and J. Wickerson. Overhauling SC atomics in C11 and OpenCL. In Proceedings of the Symposium on Principles of Programming Languages, 2016. Google ScholarDigital Library
- M. Batty, K. Memarian, K. Nienhuis, J. Pichon-Pharabod, and P. Sewell. The problem of programming language concurrency semantics. In Proceedings of the 2015 European Symposium on Programming, 2015. Google ScholarCross Ref
- M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In Proceedings of the Symposium on Principles of Programming Languages, 2011. Google ScholarDigital Library
- J. Berdine, T. Lev-Ami, R. Manivich, G. Ramalingam, and M. Sagiv. Thread quantification for concurrent shape analysis. In Proceedings of the 20th International Conference on Computer Aided Verification, 2008. Google ScholarDigital Library
- H. Boehm and B. Demsky. Outlawing Ghosts: Avoiding out-of-thin-air results. In Proceedings of the 2014 ACM SIGPLAN Workshop on Memory Systems Performance and Correctness, 2014. Google ScholarDigital Library
- S. Burckhardt, R. Alur, and M. M. K. Martin. CheckFence: Checking consistency of concurrent data types on relaxed memory models. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007. Google ScholarDigital Library
- S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan. Line-up: A complete and automatic linearizability checker. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010. Google ScholarDigital Library
- S. Burckhardt and M. Musuvathi. Effective program verification for relaxed memory models. In Proceedings of the 20th International Conference on Computer Aided Verification, 2008. Google ScholarDigital Library
- J. Burnim, T. Elmas, G. Necula, and K. Sen. NDetermin: Inferring nondeterministic sequential specifications for parallelism correctness. In Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2012. Google ScholarDigital Library
- J. Burnim, K. Sen, and C. Stergiou. Sound and complete monitoring of sequential consistency for relaxed memory models. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2011. Google ScholarCross Ref
- J. Burnim, K. Sen, and C. Stergiou. Testing concurrent programs on relaxed memory models. In Proceedings of the 2011 International Symposium on Software Testing and Analysis, 2011. Google ScholarDigital Library
- R. Colvin, L. Groves, V. Luchangco, and M. Moir. Formal verification of a lazy concurrent list-based set algorithm. In Proceedings of the 18th International Conference on Computer Aided Verification, 2006. Google ScholarDigital Library
- K. E. Coons, S. Burckhardt, and M. Musuvathi. GAMBIT: Effective unit testing for concurrency libraries. In Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2010. Google ScholarDigital Library
- M. Desnoyers, P. E. McKenney, A. S. Stern, M. R. Dagenais, and J. Walpole. User-level implementations of read-copy up- date. IEEE Transactions on Parallel and Distributed Systems, 2012. Google ScholarDigital Library
- C. Drăgoi, A. Gupta, and T. Henzinger. Automatic lineariz- ability proofs of concurrent objects with cooperating updates. In Proceedings of the 25th International Conference on Computer Aided Verification, 2013. Google ScholarDigital Library
- T. Elmas, J. Burnim, G. Necula, and K. Sen. CONCURRIT: A domain specific language for reproducing concurrency bugs. In Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013. Google ScholarDigital Library
- T. Elmas, S. Tasiran, and S. Qadeer. VYRD: Verifying con- current programs by runtime refinement-violation detection. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005. Google ScholarDigital Library
- C. Flanagan. Verifying commit-atomicity using model- checking. In Proceedings of the 11th International SPIN Workshop on Model Checking Software, 2004. Google ScholarCross Ref
- A. Haas, C. M. Kirsch, M. Lippautz, and H. Payer. How FIFO is your concurrent FIFO queue? In Proceedings of the 2012 ACM Workshop on Relaxing Synchronization for Multicore and Manycore Scalability, 2012. Google ScholarDigital Library
- N. Hemed, N. Rinetzky, and V. Vafeiadis. Modular verification of concurrency-aware linearizability. In Proceedings of the 29th International Symposium on Distributed Computing, 2015. Google ScholarDigital Library
- T. A. Henzinger, C. M. Kirsch, H. Payer, A. Sezgin, and A. Sokolova. Quantitative relaxation of concurrent data structures. In Proceedings of the 40th Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages 2013. Google ScholarDigital Library
- M. Herlihy and J. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463--492, July 1990. Google ScholarDigital Library
- G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 1st edition, 2003.Google ScholarDigital Library
- N. M. Lê, A. Pop, A. Cohen, and F. Zappa Nardelli. Correct and efficient work-stealing for weak memory models. In Proceedings of the 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2013. Google ScholarDigital Library
- D. Lea. util.concurrent.ConcurrentHashMap in java.util.concurrent the Java Concurrency Package. http://docs.oracle.com/javase/8/docs/api/java/util/concurrent/ConcurrentHashMap.html.Google Scholar
- L. Maranget, S. Sarkar, and P. Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf, 2012.Google Scholar
- Y. Meshman, N. Rinetzky, and E. Yahav. Pattern-based synthesis of synchronization for the C++ memory model. In Formal Methods in Computer-Aided Design, 2015.Google Scholar
- M. M. Michael and M. L. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, 1996. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, P. A. Nainar, T. Ball, G. Basler, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation, 2008.Google ScholarDigital Library
- B. Norris and B. Demsky. CDSChecker: Checking concurrent data structures written with C/C++ atomics. In Proceeding of the 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2013. Google ScholarDigital Library
- P. Ou and B. Demsky. AutoMO: Automatic inference of memory order parameters for C/C++11. In Proceeding of the 30th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015. Google ScholarDigital Library
- D. P. Reed and R. K. Kanodia. Synchronization with eventcounts and sequencers. Communications of the ACM, 22(2):115--123, 1979. Google ScholarDigital Library
- A. Shipilëv. https://shipilev.net/. Oct. 2016.Google Scholar
- A. Shipilëv. Java memory model pragmatics. https://shipilev.net/blog/2014/jmm-pragmatics/. Sep. 2016.Google Scholar
- J. Tassarotti, D. Dreyer, and V. Vafeiadis. Verifying read-copy-update in a logic for weak memory. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015. Google ScholarDigital Library
- V. Vafeiadis. Shape-value abstraction for verifying lineariz-ability. In Proceedings of the 2009 Conference on Verification, Model Checking, and Abstract Interpretation, 2009. Google ScholarDigital Library
- V. Vafeiadis. Automatically proving linearizability. In Proceedings of the 22th International Conference on Computer Aided Verification, 2010. Google ScholarDigital Library
- V. Vafeiadis and C. Narayan. Relaxed separation logic: A program logic for c11 concurrency. In Proceeding of the 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2013. Google ScholarDigital Library
- M. Vechev, E. Yahav, and G. Yorsh. Experience with model checking linearizability. In International SPIN Workshop on Model Checking Software, 2009. Google ScholarDigital Library
- D. Vyukov. Relacy race detector. http://relacy.sourceforge.net/, 2011 Oct.Google Scholar
- J. M. Wing and C. Gong. Testing and verifying concurrent objects. Journal of Parallel and Distributed Computing - Special issue on parallel I/O systems, 17(1-2):164--182, Jan./Feb. 1993.Google ScholarDigital Library
Index Terms
- Checking Concurrent Data Structures Under the C/C++11 Memory Model
Recommendations
Checking Concurrent Data Structures Under the C/C++11 Memory Model
PPoPP '17: Proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel ProgrammingConcurrent data structures often provide better performance on multi-core processors but are significantly more difficult to design and test than their sequential counterparts. The C/C++11 standard introduced a weak memory model with support for low-...
Concurrent tries with efficient non-blocking snapshots
PPoPP '12: Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel ProgrammingWe describe a non-blocking concurrent hash trie based on shared-memory single-word compare-and-swap instructions. The hash trie supports standard mutable lock-free operations such as insertion, removal, lookup and their conditional variants. To ensure ...
Concurrent tries with efficient non-blocking snapshots
PPOPP '12We describe a non-blocking concurrent hash trie based on shared-memory single-word compare-and-swap instructions. The hash trie supports standard mutable lock-free operations such as insertion, removal, lookup and their conditional variants. To ensure ...
Comments