A formal semantics for debugging synchronous message passing-based concurrent programs

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.