Abstract
Many multithreaded programs employ concurrent data types to safely share data among threads. However, highly-concurrent algorithms for even seemingly simple data types are difficult to implement correctly, especially when considering the relaxed memory ordering models commonly employed by today’s multiprocessors. The formal verification of such implementations is challenging as well because the high degree of concurrency leads to a large number of possible executions. In this case study, we develop a SAT-based bounded verification method and apply it to a representative example, a well-known two-lock concurrent queue algorithm. We first formulate a correctness criterion that specifically targets failures caused by concurrency; it demands that all concurrent executions be observationally equivalent to some serial execution. Next, we define a relaxed memory model that conservatively approximates several common shared-memory multiprocessors. Using commit point specifications, a suite of finite symbolic tests, a prototype encoder, and a standard SAT solver, we successfully identify two failures of a naive implementation that can be observed only under relaxed memory models. We eliminate these failures by inserting appropriate memory ordering fences into the code. The experiments confirm that our approach provides a valuable aid for desigining and implementing concurrent data types.
Supported partially by NSF awards CCR 0306352 and CNS 0524059 and donations from Intel Corporation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Sutter, H., Larus, J.: Software and the concurrency revolution. ACM Queue 3(7), 54–62 (2005)
Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124–149 (1991)
Peterson, G.L.: Concurrent reading while writing. ACM Trans. Program. Lang. Syst. 5(1), 46–55 (1983)
Lamport, L.: Concurrent reading and writing. Commun. ACM 20(11), 806–811 (1977)
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66–76 (1996)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp. C-28(9), 690–691 (1979)
Elmas, T., Tasiran, S., Qadeer, S.: VYRD: verifying concurrent programs by runtime refinement-violation detection. In: Programming Language Design and Implementation (PLDI), pp. 27–37 (2005)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 30–45. Springer, Heidelberg (2004)
Gopalakrishnan, G., Yang, Y., Sivaraj, H.: QB or not QB: An efficient execution verification tool for memory orderings. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 401–413. Springer, Heidelberg (2004)
Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Principles of Distributed Computing (PODC), pp. 267–275 (1996)
Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: Principles and Practice of Parallel Programming (PPoPP), pp. 129–136 (2006)
Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005)
Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci. 89(3) (2003)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: Symposium on Parallel Algorithms and Architectures (SPAA), pp. 34–41 (1995)
Dill, D.L., Park, S., Nowatzyk, A.G.: Formal specification of abstract memory models. In: Symposium on Research on Integrated Systems, pp. 38–52. MIT Press, Cambridge (1993)
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comp. Sys. 15(4), 391–411 (1997)
Frey, B.: PowerPC Architecture Book v2.02. International Business Machines Corporation (2005)
Weaver, D.L., Germond, T. (eds.): The SPARC Architecture Manual Version 9. Prentice-Hall, Englewood Cliffs (1994)
Compaq Computer Corporation. Alpha Architecture Reference Manual, 4th edn. (January 2002)
International Business Machines Corporation. z/Architecture Principles of Operation, 1st edn. (December 2000)
Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Analyzing the Intel Itanium memory ordering rules using logic programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 81–95. Springer, Heidelberg (2003)
Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: Logic in Computer Science (LICS), pp. 219–228 (1996)
Steinke, R.C., Nutt, G.J.: A unified theory of shared memory consistency. J. ACM 51(5), 800–849 (2004)
Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: International Parallel and Distributed Processing Symposium (IPDPS) (2004)
Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282–312 (1988)
Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: International Conference on Supercomputing (ICS), pp. 285–294 (2003)
von Praun, C., Cain, T., Choi, J., Ryu, K.: Conditional memory ordering. In: International Symposium on Computer Architecture (ISCA) (2006)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (DAC), pp. 530–535 (2001)
Martin, M., Sorin, D., Cain, H., Hill, M., Lipasti, M.: Correctly implementing value prediction in microprocessors that support multithreading or multiprocessing. In: International Symposium on Microarchitecture (MICRO), pp. 328–337 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Burckhardt, S., Alur, R., Martin, M.M.K. (2006). Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_45
Download citation
DOI: https://doi.org/10.1007/11817963_45
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)