ABSTRACT
Modern architectures implement relaxed memory models which may reorder memory operations or execute them non-atomically. Special instructions called memory fences are provided, allowing control of this behavior.
To implement a concurrent algorithm for a modern architecture, the programmer is forced to manually reason about subtle relaxed behaviors and figure out ways to control these behaviors by adding fences to the program. Not only is this process time consuming and error-prone, but it has to be repeated every time the implementation is ported to a different architecture.
In this paper, we present the first scalable framework for handling real-world concurrent algorithms running on relaxed architectures. Given a concurrent C program, a safety specification, and a description of the memory model, our framework tests the program on the memory model to expose violations of the specification, and synthesizes a set of necessary ordering constraints that prevent these violations. The ordering constraints are then realized as additional fences in the program.
We implemented our approach in a tool called DFence based on LLVM and used it to infer fences in a number of concurrent algorithms. Using DFence, we perform the first in-depth study of the interaction between fences in real-world concurrent C programs, correctness criteria such as sequential consistency and linearizability, and memory models such as TSO and PSO, yielding many interesting observations. We believe that this is the first tool that can handle programs at the scale and complexity of a lock-free memory allocator.
- Personal Communication with the Cilk Team, 2011.Google Scholar
- Adve, S. V., and Gharachorloo, K. Shared memory consistency models: A tutorial. IEEE Computer 29 (1995), 66--76. Google ScholarDigital Library
- Attiya, H., Guerraoui, R., Hendler, D., Kuznetsov, P., Michael, M. M., and Vechev, M. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In POPL'11 (New York, NY, USA), ACM, pp. 487--498. Google ScholarDigital Library
- Burckhardt, S., Alur, R., and Martin, M. M. K. CheckFence: checking consistency of concurrent data types on relaxed memory models. In PLDI (2007), pp. 12--21. Google ScholarDigital Library
- Burckhardt, S., and Musuvathi, M. Effective program verification for relaxed memory models. In CAV (2008), pp. 107--120. Google ScholarDigital Library
- Burnim, J., Sen, K., and Stergiou, C. Testing concurrent programs on relaxed memory models. In ISSTA (2011), pp. 122--132. Google ScholarDigital Library
- Chase, D., and Lev, Y. Dynamic circular work-stealing deque. In SPAA (2005), pp. 21--28. Google ScholarDigital Library
- Detlefs, D. L., Flood, C. H., Garthwaite, A. T., Garthwaite, E. T., Martin, P. A., Shavit, N. N., Jr., and Steele, G. L. Even better dcas-based concurrent deques. In DISC'00. Google ScholarDigital Library
- Dice, D., Lev, Y., Marathe, V. J., Moir, M., Nussbaum, D., and Oleszewski, M. Simplifying concurrent algorithms by exploiting hardware transactional memory. In SPAA'10, ACM, pp. 325--334. Google ScholarDigital Library
- Eén, N., and Sörensson, N. An extensible sat-solver. In SAT (2003), pp. 502--518.Google Scholar
- Fang, X., Lee, J., and Midkiff, S. P. Automatic fence insertion for shared memory multiprocessing. In ICS (2003), pp. 285--294. Google ScholarDigital Library
- Frigo, M., Leiserson, C. E., and Randall, K. H. The implementation of the cilk-5 multithreaded language. In PLDI '98. Google ScholarDigital Library
- Heller, S., Herlihy, M., Luchangco, V., Moir, M., Scherer, W., and Shavit, N. A lazy concurrent list-based set algorithm. In OPODIS '05, pp. 3--16. Google ScholarDigital Library
- Herlihy, M., and Shavit, N. The Art of Multiprocessor Programming. Morgan Kaufmann, Apr. 2008. Google ScholarDigital Library
- Huynh, T. Q., and Roychoudhury, A. Memory model sensitive bytecode verification. Form. Methods Syst. Des. 31, 3 (2007). Google ScholarDigital Library
- Jonsson, B. State-space exploration for concurrent algorithms under weak memory orderings. SIGARCH Comput. Archit. News 36, 5 (2008), 65--71. Google ScholarDigital Library
- Kuperstein, M., Vechev, M., and Yahav, E. Automatic inference of memory fences. In FMCAD'10. Google ScholarDigital Library
- Kuperstein, M., Vechev, M., and Yahav, E. Partial-coherence abstractions for relaxed memory models. In PLDI'11, pp. 187--198. Google ScholarDigital Library
- Lattner, C., and Adve, V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In CGO'04, pp. 75--87. Google ScholarDigital Library
- Lee, J., and Padua, D. A. Hiding relaxed memory consistency with a compiler. IEEE Trans. Comput. 50, 8 (2001), 824--833. Google ScholarDigital Library
- Michael, M. M. Scalable lock-free dynamic memory allocation. In PLDI '04 (2004), pp. 35--46. Google ScholarDigital Library
- Michael, M. M., and Scott, M. L. Correction of a memory management method for lock-free data structures. Tech. rep., 1995. Google ScholarDigital Library
- Michael, M. M., and Scott, M. L. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In PODC (1996), pp. 267--275. Google ScholarDigital Library
- Michael, M. M., Vechev, M. T., and Saraswat, V. A. Idempotent work stealing. In PPoPP (2009), pp. 45--54. Google ScholarDigital Library
- Park, S., and Dill, D. L. An executable specification and verifier for relaxed memory order. IEEE Trans. on Computers 48 (1999). Google ScholarDigital Library
- Shasha, D., and Snir, M. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10, 2 (1988), 282--312. Google ScholarDigital Library
- Sura, Z., Wong, C., Fang, X., Lee, J., Midkiff, S., and Padua, D. Automatic implementation of programming language consistency models. LNCS 2481 (2005), 172. Google ScholarDigital Library
- Sutter, H., and Larus, J. Software and the concurrency revolution. Queue 3, 7 (2005), 54--62. Google ScholarDigital Library
- Vechev, M., Yahav, E., and Yorsh, G. Experience with model checking linearizability. In SPIN'09, pp. 261--278. Google ScholarDigital Library
- Vechev, M., Yahav, E., and Yorsh, G. Abstraction-guided synthesis of synchronization. In POPL (2010). Google ScholarDigital Library
- Weeratunge, D., Zhang, X., and Jaganathan, S. Accentuating the positive: atomicity inference and enforcement using correct executions. In OOPSLA'11, pp. 19--34. Google ScholarDigital Library
Index Terms
- Dynamic synthesis for relaxed memory models
Recommendations
Dynamic synthesis for relaxed memory models
PLDI '12Modern architectures implement relaxed memory models which may reorder memory operations or execute them non-atomically. Special instructions called memory fences are provided, allowing control of this behavior.
To implement a concurrent algorithm for a ...
Partial-coherence abstractions for relaxed memory models
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present an approach for automatic verification and fence inference in concurrent programs running under relaxed memory models. Verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, ...
Testing concurrent programs on relaxed memory models
ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and AnalysisHigh-performance concurrent libraries, such as lock-free data structures and custom synchronization primitives, are notoriously difficult to write correctly. Such code is often implemented without locks, instead using plain loads and stores and low-...
Comments