Advertisement

Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models

  • Tatsuya AbeEmail author
  • Tomoharu Ugawa
  • Toshiyuki Maeda
  • Kousuke Matsumoto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)

Abstract

Software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons for state explosion in model checking with multiple memory consistency models, provides some optimizations intended to mitigate the problem, and applies them to McSPIN, a model checker for memory consistency models that we are developing. The effects of the optimizations and the usefulness of McSPIN are demonstrated experimentally by verifying copying protocols of concurrent copying garbage collection algorithms. To the best of our knowledge, this is the first model checking of the concurrent copying protocols under relaxed memory consistency models.

Keywords

Software model checking Relaxed memory consistency models State explosion Reordering of instructions Integration of states Concurrent copying garbage collection 

Notes

Acknowledgments

The authors thank the anonymous reviewers for several comments to improve the final version of the paper. This research partly used computational resources under Collaborative Research Program for Young Scientists provided by Academic Center for Computing and Media Studies, Kyoto University. This work was supported by JSPS KAKENHI Grant Numbers 25871113, 25330080, and 16K21335.

References

  1. 1.
    Abe, T., Maeda, T.: Model checking with user-definable memory consistency models. In: Proceedings of PGAS, short paper, pp. 225–230 (2013)Google Scholar
  2. 2.
    Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. In: Proceedings of HIPS, pp. 332–341 (2014)Google Scholar
  3. 3.
    Abe, T., Maeda, T.: Optimization of a general model checking framework for various memory consistency models. In: Proceedings of PGAS (2014)Google Scholar
  4. 4.
    Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. J. Inform. Process. (2016, to appear)Google Scholar
  5. 5.
    Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. Int. J. Softw. Tools Technol. Transf. (2016, to appear)Google Scholar
  6. 6.
    Abe, T., Maeda, T.: Observation-based concurrent program logic for relaxed memory consistency models. In: Proceedings of APLAS (2016, to appear)Google Scholar
  7. 7.
    Abe, T., Maeda, T., Sato, M.: Model checking with user-definable abstraction for partitioned global address space languages. In: Proceedings of PGAS (2012)Google Scholar
  8. 8.
    Abe, T., Maeda, T., Sato, M.: Model checking stencil computations written in a partitioned global address space language. In: Proceedings of HIPS, pp. 365–374 (2013)Google Scholar
  9. 9.
    Abe, T., Maeda, T., Ugawa, T.: McSPIN. https://bitbucket.org/abet/mcspin/
  10. 10.
    Abe, T., Ugawa, T., Maeda, T., Matsumoto, K.: Reducing state explosion for software model checking with relaxed memory consistency models (2016). arXiv:1608.05893
  11. 11.
    Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66–76 (1996)CrossRefGoogle Scholar
  12. 12.
    Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of PLDI, pp. 68–78 (2008)Google Scholar
  13. 13.
    Cavada, R., Cimatti, A., Jochim, C.A., Olivetti, G.K.E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV User Manual. 2.5 edn. (2002)Google Scholar
  14. 14.
    Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 84–104. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38856-9_7 CrossRefGoogle Scholar
  15. 15.
    Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Proceedings of POPL, pp. 70–83 (1994)Google Scholar
  16. 16.
    Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267–286. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-11957-6_15 CrossRefGoogle Scholar
  17. 17.
    Gammie, P., Hosking, T., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Proceedings of PLDI, pp. 99–109 (2015)Google Scholar
  18. 18.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). doi: 10.1007/3-540-63166-6_10 CrossRefGoogle Scholar
  19. 19.
    Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)Google Scholar
  20. 20.
    Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. Softw. Eng. 28(4), 364–377 (2002)CrossRefGoogle Scholar
  21. 21.
    IBM: PowerPC Architechture Book, Version 2.02 (2005)Google Scholar
  22. 22.
    Intel: A Formal Specification of Intel Itanium Processor Family Memory Ordering (2002)Google Scholar
  23. 23.
    Intel: Intel 64 and IA-32 Architectures Software Developer’s Manual (2016)Google Scholar
  24. 24.
    ISO/IEC 14882: 2011: Programming Language C++ (2011)Google Scholar
  25. 25.
    Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36(5), 65–71 (2008)CrossRefGoogle Scholar
  26. 26.
    Kroening, D., Tautschnig, M.: CBMC – C bounded model checker (Competition Contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54862-8_26 CrossRefGoogle Scholar
  27. 27.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_47 CrossRefGoogle Scholar
  28. 28.
    Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-16164-3_16 CrossRefGoogle Scholar
  29. 29.
    Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in relaxed memory systems. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 144–160. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22306-8_10 CrossRefGoogle Scholar
  30. 30.
    Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 339–353. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-36742-7_24 CrossRefGoogle Scholar
  31. 31.
    Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL, pp. 378–391 (2005)Google Scholar
  32. 32.
    McCloskey, B., Bacon, D.F., Cheng, P., Grove, D.: Staccato: a parallel and concurrent real-time compacting garbage collector for multiprocessors. Report RC24504, IBM (2008)Google Scholar
  33. 33.
    Oracle: The Java Language Specification. Java SE 8 edn. (2015)Google Scholar
  34. 34.
    Pizlo, F., Frampton, D., Petrank, E., Steensgaard, B.: Stopless: a real-time garbage collector for multiprocessors. In: Proceedings of ISMM, pp. 159–172 (2007)Google Scholar
  35. 35.
    Pizlo, F., Petrank, E., Steensgaard, B.: A study of concurrent real-time garbage collectors. In: Proceedings of PLDI, pp. 33–44 (2008)Google Scholar
  36. 36.
    Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55–70. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15057-9_4 CrossRefGoogle Scholar
  37. 37.
    Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of PLDI, pp. 175–186 (2011)Google Scholar
  38. 38.
    SPARC International Inc: The SPARC Architecture Manual, Version 9 (1994)Google Scholar
  39. 39.
    SV-COMP: Competition on Software Verification. https://sv-comp.sosy-lab.org/
  40. 40.
    The UPC Consortium: UPC Language Specifications Version 1.3 (2013)Google Scholar
  41. 41.
    Travkin, O., Mütze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311–326. Springer, Heidelberg (2013). doi: 10.1007/978-3-319-03077-7_21 CrossRefGoogle Scholar
  42. 42.
    Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: Proceedings of OOPSLA, pp. 867–884 (2013)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Tatsuya Abe
    • 1
    Email author
  • Tomoharu Ugawa
    • 2
  • Toshiyuki Maeda
    • 1
  • Kousuke Matsumoto
    • 2
  1. 1.STAIR LabChiba Institute of TechnologyNarashinoJapan
  2. 2.Kochi University of TechnologyKamiJapan

Personalised recommendations