×

Stateless model checking for TSO and PSO. (English) Zbl 1380.68265

Summary: We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Chronological traces induce a partial order relation on relaxed memory executions, capturing dependencies that are needed to represent the interaction via shared variables. They are optimal in the sense that they only distinguish computations that are inequivalent under the widely-used representation by Shasha and Snir. This allows an optimal dynamic partial order reduction algorithm to explore a minimal number of executions while still guaranteeing full coverage. We apply our techniques to check, under the TSO and PSO memory models, LLVM assembly produced for C/pthreads programs. Our experiments show that our technique reduces the verification effort for relaxed memory models to be almost that for the standard model of sequential consistency.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

Checkfence; veriSoft
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL, pp. 373-384. ACM (2014) · Zbl 1284.68377
[2] Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Tools and algorithms for the construction and analysis of systems, pp. 353-367. Springer, Heidelberg (2015) · Zbl 1380.68265
[3] Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: TACAS, vol. 7214 of LNCS, pp. 204-219. Springer (2012) · Zbl 1352.68047
[4] Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66-76 (1996) · doi:10.1109/2.546611
[5] Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: ESOP, vol. 7792 of LNCS, pp. 512-532. Springer (2013) · Zbl 1381.68143
[6] Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: CAV, vol. 8044 of LNCS, pp. 141-157. Springer (2013)
[7] Alglave, J., Maranget, L.: Stability in weak memory models. In: CAV, vol. 6806 of LNCS, pp. 50-66. Springer (2011) · Zbl 1114.68369
[8] Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: ESOP, vol. 7792 of LNCS, pp. 533-553. Springer (2013) · Zbl 1381.68039
[9] Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12-21. ACM (2007)
[10] Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: CAV, vol. 5123 of LNCS, pp. 107-120. Springer (2008) · Zbl 1155.68428
[11] Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: TACAS, pp. 11-25. LNCS 6605, Springer (2011) · Zbl 1315.68084
[12] Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: ICST, pp. 154-163. IEEE (2013)
[13] Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2(3), 279-287 (1999) · Zbl 1065.68506 · doi:10.1007/s100090050035
[14] Demsky, B., Lam, P.: SATCheck: SAT-directed stateless model checking for SC and TSO. In: OOPSLA (2015)
[15] Dijkstra, E.W.: Cooperating sequential processes. Springer, Heidelberg (2002)
[16] Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110-121. ACM (2005) · Zbl 1369.68135
[17] Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem, vol. 1032 of LNCS. Springer (1996) · Zbl 1293.68005
[18] Godefroid, P.: Model checking for programming languages using VeriSoft. In: POPL, pp. 174-186. ACM Press (1997)
[19] Godefroid, P.: Software model checking: the VeriSoft approach. Formal Methods Syst. Des. 26(2), 77-101 (2005) · doi:10.1007/s10703-005-1489-x
[20] Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: PLDI, pp. 165-174. New York, NY, USA, ACM (2015)
[21] Krishnamurthy, A., Yelick, K.A.: Analyses and optimizations for shared address space programs. J. Parallel Distrib. Comput. 38(2), 130-144 (1996) · Zbl 1114.68369 · doi:10.1006/jpdc.1996.0136
[22] Lauterburg, S., Karmani, R., Marinov, D., Agha, G.: Evaluating ordering heuristics for dynamic partial-order reduction techniques. In: FASE, pp 308-322. LNCS 6013 (2010)
[23] Lee, J., Padua, D.A.: Hiding relaxed memory consistency with a compiler. IEEE Trans. Comput. 50(8), 824-833 (2001) · doi:10.1109/12.947002
[24] Lei, Y., Carver, R.: Reachability testing of concurrent programs. IEEE Trans. Softw. Eng. 32(6), 382-403 (2006) · doi:10.1109/TSE.2006.56
[25] Liu, F., Nedev, N., Prisadnikov, N., Vechev, M.T., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI, pp. 429-440. ACM (2012)
[26] The LLVM compiler infrastructure. http://llvm.org
[27] Mazurkiewicz, A.: Trace theory. In: Advances in Petri Nets (1986) · Zbl 0633.68051
[28] Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI, pp. 267-280. USENIX (2008)
[29] Park, S., Dill, D.L: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA, pp. 34-41. ACM (1995)
[30] Peled, D.: All from one, one for all, on model-checking using representatives. In: CAV, vol. 697 of LNCS, pp. 409-423. Springer (1993)
[31] Peterson, G., Stickel, M.: Myths about the mutal exclusion problem. Inf. Process. Lett. 12(3), 115-116 (1981) · Zbl 0474.68031 · doi:10.1016/0020-0190(81)90106-X
[32] Saarikivi, O., Kähkönen, K., Heljanko, K.: Improving dynamic partial order reductions for concolic testing. In: ACSD, IEEE (2012)
[33] Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Haifa Verification Conference, pp. 166-182. LNCS 4383 (2007)
[34] Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Comm. ACM 53(7), 89-97 (2010) · doi:10.1145/1785414.1785443
[35] Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282-312 (1988) · doi:10.1145/42190.42277
[36] SPARC International, Inc. The SPARC Architecture Manual Version 9, (1994) · Zbl 0474.68031
[37] Tasharofi, S. et al.: TransDPOR: A novel dynamic partial-order reduction technique for testing actor programs. In: FMOODS/FORTE, pp. 219-234. LNCS 7273 (2012)
[38] Valmari, A.: Stubborn sets for reduced state space generation. In: Advances in Petri Nets, vol. 483 of LNCS, pp. 491-515. Springer (1989)
[39] Wang, C., Said, M., Gupta, A.: Coverage guided systematic concurrency testing. In: ICSE, pp. 221-230. ACM (2011)
[40] Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: IPDPS, IEEE (2004)
[41] Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, pp. 250-259. ACM (2015) · Zbl 1114.68369
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.