×

zbMATH — the first resource for mathematics

Model checking concurrent programs. (English) Zbl 1392.68251
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 573-611 (2018).
Summary: Concurrent programs are in widespread use for harnessing the computing power of multi-core hardware. However, it is very challenging to develop correct concurrent programs. In practice, concurrency-related bugs such as data races, deadlocks, and atomicity violations are very common. In this chapter, we describe efforts based on model-checking for automatic verification and debugging of concurrent programs. The emphasis is on core ideas for reasoning about synchronizations and communication between threads and processes, while considering all possible behaviors due to their interactions.
For the entire collection see [Zbl 1390.68001].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 1. Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models (extended version). Form. Methods Syst. Des. 40(2), 170-205 (2012) · Zbl 1247.68155
[2] 2. Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR. LNCS, vol. 5201, pp. 356-371 (2008) · Zbl 1160.68451
[3] 3. Atig, M.F., Touili, T.: Verifying parallel programs with dynamic communication structures. In: Maneth, S. (ed.) CIAA. LNCS, vol. 5642, pp. 145-154. Springer, Heidelberg (2009) · Zbl 1248.68138
[4] 4. Bonnet, R., Chadha, R., Madhusudan, P., Viswanathan, M.: Reachability under contextual locking. Log. Methods Comput. Sci. 9(3), 1-17 (2013) · Zbl 1274.68064
[5] 5. Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. 16(2), 127-146 (2014) · Zbl 1352.68057
[6] 6. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Marzurkiewicz, A., Winkowski, J. (eds.) CONCUR. LNCS, vol. 1243, pp. 135-150. Springer, Heidelberg (1997)
[7] 7. Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujan, R., Sen, S. (eds.) FSTTCS. LNCS, vol. 3821, pp. 348-359. Springer, Heidelberg (2005) · Zbl 1172.68422
[8] 8. Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp. 62-73. ACM, New York (2003) · Zbl 1321.68185
[9] 9. Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. Int. J. Found. Comput. Sci. 14(4), 551-582 (2003) · Zbl 1101.68457
[10] 10. Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded model checking of concurrent data types on relaxed memory models: a case study. In: Ball, T., Jones, R.B. (eds.) CAV. LNCS, vol. 4144, pp. 489-502. Springer, Heidelberg (2006)
[11] 11. 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, New York (2007)
[12] 12. Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV. LNCS, vol. 5123, pp. 107-120. Springer, Heidelberg (2008) · Zbl 1155.68428
[13] 13. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011) · Zbl 1281.68155
[14] 14. Cerný, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV. LNCS, vol. 8044, pp. 951-967. Springer, Heidelberg (2013)
[15] 15. Chadha, R., Madhusudan, P., Viswanathan, M.: Reachability under contextual locking. In: Flanagan, C., König, B. (eds.) TACAS. LNCS, vol. 7214, pp. 437-450. Springer, Heidelberg (2012) · Zbl 1352.68059
[16] 16. Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS. LNCS, vol. 3920, pp. 334-349. Springer, Heidelberg (2006) · Zbl 1180.68109
[17] 17. Chen, F., Rosu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV. LNCS, vol. 4590, pp. 240-253. Springer, Heidelberg (2007) · Zbl 1135.68468
[18] 18. Cherem, S., Chilimbi, T.M., Gulwani, S.: Inferring locks for atomic sections. In: PLDI, pp. 304-315. ACM, New York (2008)
[19] 19. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52-71. Springer, Heidelberg (1981)
[20] 20. Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Form. Methods Syst. Des. 34(2), 104-125 (2009) · Zbl 1176.68118
[21] 21. Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2-15. ACM, New York (2009) · Zbl 1315.68087
[22] 22. Emmi, M., Fischer, J.S., Jhala, R., Majumdar, R.: Lock allocation. In: POPL, pp. 291-296. ACM, New York (2007)
[23] 23. Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Common, N., Finkel, A. (eds.) CAV. LNCS, vol. 2102, pp. 324-336. Springer, Heidelberg (2001) · Zbl 0991.68539
[24] 24. Farzan, A., Kincaid, Z.: Compositional bitvector analysis for concurrent programs with nested locks. In: Cousot, R., Martel, M. (eds.) SAS. LNCS, vol. 6337, pp. 253-270. Springer, Heidelberg (2010) · Zbl 1306.68013
[25] 25. Farzan, A., Madhusudan, P., Sorrentino, F.: Meta-analysis for atomicity violations under nested locking. In: Bonajjani, A., Maler, O. (eds.) CAV. LNCS, vol. 5643, pp. 248-262. Springer, Heidelberg (2009) · Zbl 1242.68065
[26] 26. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110-121. ACM, New York (2005) · Zbl 1369.68135
[27] 27. Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in BMC. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN. LNCS, vol. 5156, pp. 114-133. Springer, Heidelberg (2008)
[28] 28. Ganai, M.K., Kundu, S.: Reduction of verification conditions for concurrent system using mutually atomic transactions. In: Păsăreanu, C. (ed.) SPIN. LNCS, vol. 5578, pp. 68-87. Springer, Heidelberg (2009)
[29] 29. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996) · Zbl 1293.68005
[30] 30. Godefroid, P.: Model checking for programming languages using Verisoft. In: POPL, pp. 174-186. ACM, New York (1997)
[31] 31. Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp. 266-277. ACM, New York (2007)
[32] 32. Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bošnački, D., Edelkamp, S. (eds.) SPIN Workshop on Model Checking Software. LNCS, vol. 4595, pp. 95-112. Springer, Heidelberg (2007)
[33] 33. Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, pp. 331-344. ACM, New York (2011) · Zbl 1284.68427
[34] 34. Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI, pp. 1-13. ACM, New York (2004)
[35] 35. Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: ESEC/SIGSOFT FSE, pp. 31-40. ACM, New York (2005)
[36] 36. Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt, W.A. Jr., Somenzi, F. (eds.) CAV. LNCS, vol. 2725, pp. 262-274. Springer, Heidelberg (2003) · Zbl 1278.68175
[37] 37. Holzmann, G.J.: Software model checking with SPIN. Adv. Comput. 65, 78-109 (2005)
[38] 38. Kahlon, V.: Boundedness vs. unboundedness of lock chains: characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In: LICS, pp. 27-36. IEEE, Piscataway (2009)
[39] 39. Kahlon, V.: Reasoning about threads with bounded lock chains. In: Katoen, J., König, B. (eds.) CONCUR. LNCS, vol. 6901, pp. 450-465. Springer, Heidelberg (2011) · Zbl 1343.68154
[40] 40. Kahlon, V., Gupta, A.: An automata-theoretic approach for model checking threads for LTL properties. In: LICS, pp. 101-110. IEEE, Piscataway (2006)
[41] 41. Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL, pp. 303-314. ACM, New York (2007) · Zbl 1295.68159
[42] 42. Kahlon, V., Ivančić, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV. LNCS, vol. 3576, pp. 505-518. Springer, Heidelberg (2005) · Zbl 1081.68623
[43] 43. Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS. LNCS, vol. 5505, pp. 124-138. Springer, Heidelberg (2009)
[44] 44. Kahlon, V., Wang, C.: Universal causality graphs: a precise happens-before model for detecting bugs in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. LNCS, vol. 6174, pp. 434-449. Springer, Heidelberg (2010)
[45] 45. Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol. 5643, pp. 398-413. Springer, Heidelberg (2009) · Zbl 1242.68166
[46] 46. Kidd, N., Lammich, P., Touili, T., Reps, T.W.: A decision procedure for detecting atomicity violations for communicating processes with locks. Int. J. Softw. Tools Technol. Transf. 13(1), 37-60 (2011)
[47] 47. Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. SIGACT News 43(2), 108-123 (2012)
[48] 48. Lahiri, S.K., Qadeer, S., Rakamaric, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol. 5643, pp. 509-524. Springer, Heidelberg (2009)
[49] 49. Lal, A., Balakrishnan, G., Reps, T.: Extended weighted pushdown systems. In: Ekessami, K., Rajamani, S.K. (eds.) CAV. LNCS, vol. 3576, pp. 434-448. Springer, Heidelberg (2005) · Zbl 1081.68625
[50] 50. Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV. LNCS, vol. 5123, pp. 37-51. Springer, Heidelberg (2008) · Zbl 1155.68368
[51] 51. Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol. 5643, pp. 525-539. Springer, Heidelberg (2009) · Zbl 1242.68058
[52] 52. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558-565 (1978) · Zbl 0378.68027
[53] 53. Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Advances in Petri Nets. LNCS, vol. 255, pp. 279-324. Springer, Heidelberg (1986)
[54] 54. Miné, A.: Static analysis of run-time errors in embedded critical parallel C programs. In: Barté, G. (ed.) ESOP. LNCS, vol. 6602. Springer, Heidelberg (2011)
[55] 55. Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing Heisenbugs in concurrent programs. In: OSDI, pp. 267-280. USENIX Association, Berkeley (2008)
[56] 56. O’Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR. LNCS, vol. 3170, pp. 49-67. Springer, Heidelberg (2004)
[57] 57. Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV. LNCS, vol. 697, pp. 409-423. Springer, Heidelberg (1993)
[58] 58. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L. (eds.) TACAS. LNCS, vol. 3440, pp. 93-107. Springer, Heidelberg (2005) · Zbl 1087.68598
[59] 59. Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV. LNCS, vol. 3576, pp. 82-97. Springer, Heidelberg (2005) · Zbl 1081.68633
[60] 60. Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. In: TOPLAS, pp. 416-430. ACM, New York (2000)
[61] 61. Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS. LNCS, vol. 2694, pp. 189-213. Springer, Heidelberg (2003) · Zbl 1067.68051
[62] 62. Sen, K., Rosu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: ESEC/SIGSOFT FSE, pp. 337-346. ACM, New York (2003)
[63] 63. Singh, R., Giannakopoulou, D., Pasareanu, C.S.: Learning component interfaces with may and must abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. LNCS, vol. 6174, pp. 527-542. Springer, Heidelberg (2010)
[64] 64. Sinha, A., Malik, S., Gupta, A.: Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. In: FMCAD, pp. 6-15. IEEE, Piscataway (2012)
[65] 65. Sinha, N., Wang, C.: Staged concurrent program analysis. In: SIGSOFT FSE, pp. 47-56. ACM, New York (2010)
[66] 66. Sinha, N., Wang, C.: On interference abstractions. In: POPL, pp. 423-434. ACM, New York (2011) · Zbl 1284.68203
[67] 67. Solar-Lezama, A., Jones, C.G., Bodík, R.: Sketching concurrent data structures. In: PLDI, pp. 136-148. ACM, New York (2008)
[68] 68. Stoller, S.D.: Model-checking multi-threaded distributed Java programs. Int. J. Softw. Tools Technol. Transf. 4(1), 71-91 (2002)
[69] 69. Touili, T., Atig, M.F.: Verifying parallel programs with dynamic communication structures. Theor. Comput. Sci. 411(38-39), 3460-3468 (2010) · Zbl 1209.68114
[70] 70. Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. LNCS, vol. 6174, pp. 450-464. Springer, Heidelberg (2010)
[71] 71. Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets. LNCS, vol. 483, pp. 491-515. Springer, Heidelberg (1989)
[72] 72. Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203-232 (2003)
[73] 73. Vo, A., Vakkalanka, S.S., Delisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. In: PPOPP, pp. 261-270. ACM, New York (2009)
[74] 74. Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FSTTCS. LNCS, vol. 1974, pp. 127-138. Springer, Heidelberg (2000) · Zbl 1044.68111
[75] 75. Wang, C., Kundu, S., Ganai, M.K., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: Cavalcanti, A., Dams, D. (eds.) FM. LNCS, vol. 5850, pp. 256-272. Springer, Heidelberg (2009) · Zbl 1242.68187
[76] 76. Wang, C., Limaye, R., Ganai, M.K., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS. LNCS, vol. 6015, pp. 328-342. Springer, Heidelberg (2010) · Zbl 1284.68418
[77] 77. Wang, C., Said, M., Gupta, A.: Coverage guided systematic concurrency testing. In: ICSE, pp. 221-230. ACM, New York (2011)
[78] 78. Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. LNCS, vol. 4963, pp. 382-396. Springer, Heidelberg (2008) · Zbl 1134.68421
[79] 79. Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS. LNCS, vol. 6014, pp. 94-108. Springer, Heidelberg (2010) · Zbl 1284.68419
[80] 80. Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schutte, W., Barnett, M. (eds.) ICFEM. LNCS, vol. 3308, pp. 30-45 (2004)
[81] 81. Yi, J., Sadowski, C., Flanagan, C.: SideTrack: generalizing dynamic atomicity analysis. In: PADTAD, pp. 8:1-8:10. ACM, New York (2009)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.