Abstract
In this paper, we propose a semantic framework to debug synchronous message passing-based concurrent programs, which are increasingly useful as parallel computing and distributed systems become more and more pervasive. We first design a concurrent programming language model to uniformly represent existing concurrent programming languages. Compared to sequential programming languages, this model contains communication statements, i.e., sending and receiving statements, and a concurrent structure to represent communication and concurrency. We then propose a debugging process consisting of a tracing and a locating procedure. The tracing procedure re-executes a program with a failed test case and uses specially designed data structures to collect useful execution information for locating bugs. We provide for the tracing procedure a structural operational semantics to represent synchronous communication and concurrency. The locating procedure backward locates the ill-designed statement by using information obtained in the tracing procedure, generates a fix equation, and tries to fix the bug by solving the fix equation. We also propose a structural operational semantics for the locating procedure. We supply two examples to test our proposed operational semantics.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Hailpern B, Santhanam P. Software debugging, testing and verification. IBM Syst J, 2002, 41: 4–12
Zeller A. Why Programs Fail. 2nd ed. Oxford: Elsevier Inc., 2009. 10–15
Petri C A, Reisig W. Petri net. Scholarpedia, 2008, 3: 64–77
Hewitt C, Bishop P, Steiger R. A universal modular ACTOR formalism for artificial intelligence. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, San Francisco, 1973. 235–245
Milner R. A Calculus of Communicating Systems. Berlin: Springer Verlag, 1980. 65–83
Hoare C A R. Communicating sequential processes. Commun ACM, 1978, 21: 666–677
Zhou C C, Wang J, Anders P R. A formal description of hybrid systems. Hybrid Syst, 1996, 1066: 511–530
Hennessy M, Lin H M. Proof systems for message-passing process algebras. Form Asp Comput, 1996, 8: 379–407
Mrinal N D K C, Jamatia A. A review and analysis of software complexity metrics in structural testing. Int J Comput Commun Eng, 2013, 2: 129–133
Souza S R S, Vergilio S R, Souza P S L, et al. Structural testing criteria for message passing parallel programs. Concurr Comput Pract Exp, 2008, 20: 1893–1916
Taylor R N, Levine D L, Kelly C. Structural testing of concurrent programs. IEEE Trans Softw Eng, 1992, 18: 206–215
Yang R D, Chung C G. Path analysis testing of concurrent programs. Inf Softw Technol, 1992, 34: 43–56
Yu L, Carver R H. Reachability testing of concurrent programs. IEEE Trans Softw Eng, 2006, 32: 382–403
Carver R H, Tai K C. Replay and testing for concurrent programs. IEEE Softw, 1991, 8: 66–74
Leblanc T J, Mellor J M. Debugging parallel programs with instant replay. IEEE Trans Comput, 1987, 36: 471–482
Netzer R H B, Miller B P. Optimal tracing and replay for debugging message-passing parallel programs. In: Proceedings of the 1992 ACM/IEEE Conference on Supercomputing, Los Alamitos, 1992. 502–511
Beguelin A L. XAB: a tool for monitoring PVM programs. In: Proceedings of Workshop on Heterogeneous Processing. New York: IEEE, 1993. 92–97
Vetter J S, Supinski B R. Dynamic software testing of MPI applications with Umpire. In: Proceedings of the 2000 ACM/IEEE Conference on Supercomputing. Piscataway: IEEE, 2000. 1–10
Plotkin G D. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. 1981
Li W, Li N. A formal semantics for program debugging. Sci China Inf Sci, 2012, 55: 133–148
Li W. R-calculus: an inference system for belief revision. Comput J, 2007, 50: 378–390
Li W. Mathematical Logic: Foundations for Information Science. Basel: Birkhäuser Publisher, 2010. 173–192
Zhang Y K. Software Debugging. Beijing: Publishing House of Electronics Industry, 2009. 93–110
Lewis B. Debugging backwards in time. In: Proceedings of the 5th International Workshop on Automated and Algorithmic Debugging, Ghent, 2003. 1–15
Weiser M. Program slicing. IEEE Trans Softw Eng, 1984, 10: 352–357
Misherghi G, Su Z. HDD: hierarchical delta debugging. In: Proceedings of the 28th International Conference on Software Engineering, Shanghai, 2006. 142–151
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Li, H., Luo, J. & Li, W. A formal semantics for debugging synchronous message passing-based concurrent programs. Sci. China Inf. Sci. 57, 1–18 (2014). https://doi.org/10.1007/s11432-014-5150-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11432-014-5150-4