Advertisement

Detecting MPI Zero Buffer Incompatibility by SMT Encoding

  • Yu HuangEmail author
  • Eric Mercer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

A prevalent asynchronous message passing standard is the Message Passing Interface (MPI). There are two runtime semantics for MPI: zero buffer (messages have no buffering) and infinite buffer (messages are copied into a runtime buffer on the API call). A problem in any MPI program, intended or otherwise, is zero buffer incompatibility. A zero buffer incompatible MPI program deadlocks. This problem is difficult to predict because a developer does not know if the deadlock is based on the buffering semantics or a bad program. This paper presents an algorithm that encodes a single-path MPI program as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible schedule, such that it proves the program is zero buffer compatible. This encoding is also adaptable to checking assertion violation for correct computation. To support MPI semantics, this algorithm correctly defines the point-to-point communication and collective communication with respective rules for both infinite buffer semantics and zero buffer semantics. The novelty in this paper is considering only the schedules that strictly alternate sends and receives leading to an intuitive zero buffer encoding. This paper proves that the set of all the strictly alternating schedules is capable of covering all the message communication that may occur in any execution under zero buffer semantics. Experiments demonstrate that the SMT encoding is correct and highly efficient for a set of benchmarks compared with two state-of-art MPI verifiers.

Keywords

MPI SMT Message Passing 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
  2. 2.
    Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The satisfiability modulo theories library (smt-lib). www.SMT-LIB.org (2008)
  3. 3.
  4. 4.
    Clarke, E., Kroning, 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) CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC, pp. 368–371. ACM (2003)Google Scholar
  6. 6.
    Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991). http://doi.acm.org/10.1145/115372.115320 CrossRefGoogle Scholar
  7. 7.
    Elwakil, M., Yang, Z.: Debugging support tool for MCAPI applications. In: Lourenço, J. (ed.) PADTAD, pp. 20–25. ACM (2010)Google Scholar
  8. 8.
    Elwakil, M., Yang, Z., Wang, L.: CRI: symbolic debugger for MCAPI applications. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 353–358. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  9. 9.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 110–121. ACM (2005)Google Scholar
  10. 10.
    Forejt, V., Kroening, D., Narayanaswamy, G., Sharma, S.: Precise predictive analysis for discovering communication deadlocks in MPI programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 263–278. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  11. 11.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Huang, Y., Mercer, E., McCarthy, J.: Proving MCAPI executions are correct using SMT. In: ASE, pp. 26–36 (2013)Google Scholar
  13. 13.
    de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  14. 14.
    MPICH: High-Performance Portable MPI. http://www.mpich.org
  15. 15.
    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) CrossRefGoogle Scholar
  16. 16.
    Sharma, S., Gopalakrishnan, G., Bronevetsky, G.: A sound reduction of persistent-sets for deadlock detection in MPI applications. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, pp. 194–209. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  17. 17.
    Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC: A runtime verification tool for MCAPI user applications. In: FMCAD, pp. 41–44. IEEE (2009)Google Scholar
  18. 18.
    Siegel, S.F.: Model checking nonblocking MPI programs. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 44–58. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  19. 19.
    Siegel, S.F.: Verifying parallel programs with MPI-Spin. In: PVM/MPI, pp. 13–14 (2007)Google Scholar
  20. 20.
    Vakkalanka, S.S., Sharma, S., Gopalakrishnan, G., Kirby, R.M.: ISP: a tool for model checking MPI programs. In: PPOPP, pp. 285–286 (2008)Google Scholar
  21. 21.
    Vakkalanka, S.S., Vo, A., Gopalakrishnan, G., Kirby, R.M.: Reduced execution semantics of MPI: From theory to practice. In: FM, pp. 724–740 (2009)Google Scholar
  22. 22.
    Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., de Supinski, B.R., Schulz, M., Bronevetsky, G.: A scalable and distributed dynamic formal verifier for MPI programs. In: SC, pp. 1–10. IEEE (2010)Google Scholar
  23. 23.
    Vo, A., Gopalakrishnan, G., Kirby, R.M., de Supinski, B.R., Schulz, M., Bronevetsky, G.: Large scale verification of MPI programs using Lamport clocks with lazy update. In: Rauchwerger, L., Sarkar, V. (eds.) PACT, pp. 330–339. IEEE Computer Society (2011)Google Scholar
  24. 24.
    Xue, R., Liu, X., Wu, M., Guo, Z., Chen, W., Zheng, W., Zhang, Z., Voelker, G.M.: MPIWiz: subgroup reproducible replay of mpi applications. In: Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2009, Raleigh, NC, USA, February 14–18, 2009, pp. 251–260 (2009), http://doi.acm.org/10.1145/1504176.1504213

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Brigham Young UniversityProvoUtah

Personalised recommendations