Combining Symbolic Execution and Model Checking to Verify MPI Programs

TL;DR

This paper introduces MPI-SV, a novel tool that combines symbolic execution and model checking to efficiently verify MPI programs, especially those with non-blocking operations, significantly improving scalability and verification success rate.

Contribution

The paper presents MPI-SV, the first symbolic execution based verifier for MPI programs with non-blocking operations, integrating symbolic execution and model checking for enhanced verification capabilities.

Findings

MPI-SV verifies 90% of tasks compared to 55% by pure symbolic execution.

MPI-SV achieves 19x speedup in verifying properties.

MPI-SV verifies 100 tasks within one hour, outperforming previous methods.

Abstract

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV (footnote: https://mpi-sv.github.io) and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55\%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90\%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

Figures

Tables

Table 1. Table 1 . The programs in the experiments.

Program	LOC	Brief Description
DTG	$90$	Dependence transition group
Matmat	$105$	Matrix multiplication
Integrate	$181$	Integral computing
Diffusion2d	$197$	Simulation of diffusion equation
Gauss_elim	$341$	Gaussian elimination
Heat	$613$	Heat equation solver
Mandelbrot	$268$	Mandelbrot set drawing
Sorting	$218$	Array sorting
Image_manip	$360$	Image manipulation
DepSolver	$8988$	Multimaterial electrostatic solver
Kfray	$12728$	KF-Ray parallel raytracer
ClustalW	$23265$	Multiple sequence alignment
Total	47354	12 open source programs

Table 2. Table 2 . Experimental results.

Program (#Procs)	T	​Deadlock​	Time(s)		#Iterations
			Symbolic execution	​Our approach​	Symbolic execution	​Our approach​
DTG​ (5) ​	$o$	0	$10.12$	$9.02$	$3$	$1$
	${\text{m}}_1$	0	$13.69$	$9.50$	$10$	$2$
	${\text{m}}_2$	1	$10.02$	$8.93$	$4$	$2$
	${\text{m}}_3$	1	$10.21$	$9.49$	$4$	$2$
	${\text{m}}_4$	1	$10.08$	$9.19$	$4$	$2$
	${\text{m}}_5$	1	$9.04$	$9.29$	$2$	$2$
Matmat∗​(4)	o	0	$36.94$	$10.43$	$54$	1
Integrate​ (6/8/10)	$o$	0/0/0	$78.17/\text{to}/\text{to}$	$8.87/10.45/44.00$	​​$120/3912/3162$​​	$1/1/1$
	${\text{m}}_1$	0/0/-1	$\text{to}/\text{to}/\text{to}$	$\text{49.94}/\text{to}/\text{to}$	$4773/3712/3206$	$\text{32}/128/79$
	${\text{m}}_2$	​ 1/1/1​	$9.35/9.83/9.94$	$9.39/10.76/44.09$	$2/2/2$​	$2/2/2$
Integrate∗​ (4/6)	o	0/0	$24.18/123.55$	$9.39/32.03$	$27/125$	$1/1$
Diffusion2d​ (4/6)	$o$	0/0	$106.86/\text{to}$	9.84/13.19	90/2041	1/1
	${\text{m}}_1$	0/1	$110.25/11.95$	$\text{10.18}/13.81$	$90/2$	$\text{1}/2$
	${\text{m}}_2$	0/1	$3236.02/12.66$	$\text{17.05}/14.38$	$5850/3$	$16/2$
	${\text{m}}_3$	0/0	$\text{to}/\text{to}$	$19.26/199.95$	$5590/4923$	$16/64$
	${\text{m}}_4$	1/1	$11.35/11.52$	$\text{11.14}/14.22$	$3/2$	$\text{2}/2$
	${\text{m}}_5$	1/0	$10.98/\text{to}$	$10.85/13.44$	$2/1991$	$2/\text{1}$
Gauss_elim​ (6/8/10)	$o$	0/0/0	$\text{to}/\text{to}/\text{to}$	13.47/15.12/87.45	2756/2055/1662	1/1/1
	${\text{m}}_1$	1/1/1	$155.40/\text{to}/\text{to}$	$14.31/16.99/88.79$	$121/2131/559$	$2/2/2$
Heat​ (6/8/10)	$o$	1/1/1	$17.31/17.99/20.51$	$\text{16.75}/19.27/22.75$	$2/2/2$	$1/1/1$
	${\text{m}}_1$	1/1/1	$17.33/18.21/20.78$	$\text{17.03}/19.75/23.16$	$2/2/2$	$1/1/1$
	${\text{m}}_2$	1/1/1	$18.35/18.19/20.74$	$\text{16.36}/19.53/23.07$	$2/2/2$	$1/1/1$
	${\text{m}}_3$	1/1/1	$19.64/20.21/23.08$	$16.36/19.72/22.95$	$3/3/3$	$1/1/1$
	${\text{m}}_4$	1/1/1	$22.9/24.73/27.78$	$16.4/19.69/22.90$	$9/9/9$	$1/1/1$
	${\text{m}}_5$	1/1/1	$24.28/28.57/32.67$	$16.61/19.59/22.42$	$7/7/7$	$1/1/1$
Mandelbrot​ (6/8/10)	$o$	​0/0/-1​	$\text{to}/\text{to}/\text{to}$	$\text{117.68}/\text{831.87}/\text{to}$	$500/491/447$	$\text{9}/\text{9}/9$
	${\text{m}}_1$	​-1/-1/-1​	$\text{to}/\text{to}/\text{to}$	$\text{to}/\text{to}/\text{to}$	$1037/1621/1459$	$173/227/246$
	${\text{m}}_2$	​-1/-1/-1​	$\text{to}/\text{to}/\text{to}$	$\text{to}/\text{to}/\text{to}$	$1093/1032/916$	$178/136/90$​
	${\text{m}}_3$	1/1/1	$10.71/11.17/11.92$	$10.84/11.68/13.5$	$2/2/2$	$2/2/2$
Mandelbort∗​ (4/6)	o	0/0	$68.09/270.65$	$12.65/13.21$	$72/240$	$2/2$
Sorting∗​ (4/6)	o	0/0	$\text{to}/\text{to}$	$19.18/46.19$	$584/519$	$1/1$
Image_mani​ (6/8/10)	$o$	0/0/0	​​$97.69/118.72/141.87$​​	$18.68/23.84/27.89$	$96/96/96$	$4/4/4$
	${\text{m}}_1$	1/1/1	$12.92/15.80/15.59$	$14.15/\text{14.53}/16.86$	$2/2/2$	$2/2/2$
DepSolver​ (6/8/10)	$o$	0/0/0	​​$94.17/116.5/148.38$​​	​$97.19/123.36/151.83$​	$4/4/4$	$4/4/4$
Kfray​ (6/8/10)	$o$	0/0/0	$\text{to}/\text{to}/\text{to}$	$51.59/68.25/226.96$	$1054/981/1146$	$1/1/1$
	${\text{m}}_1$	1/1/1	$52.15/53.50/46.83$	$53.14/69.58/229.97$	$2/2/2$	$2/2/2$
	${\text{m}}_2$	​-1/-1/-1​	$\text{to}/\text{to}/\text{to}$	$\text{to}/\text{to}/\text{to}$	​​$1603/1583/1374$​​	$239/137/21$
	${\text{m}}_3$	1/1/1	$51.31/43.34/48.33$	$\text{50.40}/71.15/230.18$	$2/2/2$	$2/2/2$
Kfray∗​ (4/6)	o	0/0	$\text{to}/\text{to}$	$53.44/282.46$	$1301/1575$	$1/1$
Clustalw​ (6/8/10)	$o$	0/0/0	$\text{to}/\text{to}/\text{to}$	$47.28/79.38/238.37$	1234/1105/1162	1/1/1
	${\text{m}}_1$	0/0/0	$\text{to}/\text{to}/\text{to}$	$47.94/80.10/266.16$	$1365/1127/982$	$1/1/1$
	${\text{m}}_2$	0/0/0	$\text{to}/\text{to}/\text{to}$	$47.71/90.32/266.08$	$1241/1223/915$	$1/1/1$
	${\text{m}}_3$	1/1/1	$895.63/\text{to}/\text{to}$	$149.71/1083.95/301.99$	$175/1342/866$	$5/17/2$
	${\text{m}}_4$	0/0/0	$\text{to}/\text{to}/\text{to}$	$47.49/79.94/234.99$	$1347/1452/993$	$1/1/1$
	${\text{m}}_5$	0/0/0	$\text{to}/\text{to}/\text{to}$	$47.75/80.33/223.77$	$1353/1289/1153$	$1/1/1$

Equations

$$((cha{n}_1?a\to \text{skip}\square cha{n}_2?b\to \text{skip})\text{fatsemi}{e}_w)\underset{\{e_w\}}{\Vert }(\text{B}\text{fatsemi}{e}_w\text{fatsemi}\text{skip})$$

$$\mathcal{T}({\text{CSP}}_{static})=\mathcal{T}({\text{CSP}}_{ideal})$$

$$update(\mathcal{F}\!,\!\alpha)\!\!=\!\!\left\{\begin{array}[]{ll}\!\!\mathcal{F}{:=}\mathsf{active}\!\!&\!\!\mathcal{F}{=}\mathsf{blocked}\land\mathit{isBlocking}(\alpha)\\ \!\!\mathcal{F}{:=}\mathsf{blocked}\!\!&\!\!\mathcal{F}{=}\mathsf{active}\land\mathit{isBlocking}(\alpha)\\ \!\!\mathcal{F}{:=}\mathcal{F}\!\!&\!\!\mathit{otherwise}\end{array}\right.$$

$$\begin{array}[]{lll}\gamma&::=&\mathbf{true}\mid\gamma\vee\gamma\mid\neg\gamma\mid\mathbf{assertion}(S)\\ \varphi&::=&\mathbf{EF}\ \gamma\mid\neg\varphi\end{array}$$

$$E(S){=}\left\{\begin{array}[]{ll}\{\mathit{issue}({o})\}\!\!\!&if\ \mathit{issue}({o}){\in}enabled(S){\land}rank(o){=}\mathit{minIssue}(S)\\ \{B\}\!\!\!&if\ B{\in}enabled(S)\\ \{W\}\!\!\!&if\ W{\in}enabled(S){\land}rank_{a}(W){=}\mathit{minRank}(S)\\ \{SR\}\!\!\!&if\ SR{\in}enabled(S){\land}rank_{a}(SR){=}\mathit{minRank}(S)\\ enabled(S)\!\!\!&otherwise\\ \end{array}\right.$$

Full text

Symbolic Verification; Symbolic Execution; Model Checking; Message Passing Inteface; Synergy

††journalyear: 2020††copyright: acmcopyright††conference: ICSE ’20: 42nd International Conference on Software Engineering ; May 23-29, 2018; Seoul, South Korea††booktitle: ICSE ’20: ICSE ’20: 42nd International Conference on Software Engineering , May 23-29, 2020, Seoul, South Korea††price: 15.00††doi: XX.XXXX/XXXXXXX.XXXXXXX††isbn: xxx-x-xxxx-xxxx-x/xx/xx††ccs: Software and its engineering Software verification and validation

1. Introduction

Nowadays, an increasing number of high-performance computing (HPC) applications have been developed to solve large-scale problems (Buyya et al., 1999). The Message Passing Interface (MPI) (Snir, 1998) is the current de facto standard programming paradigm for developing HPC applications. Many MPI programs are developed with significant human effort. One of the reasons is that MPI programs are error-prone because of complex program features (such as non-determinism and asynchrony) and their scale. Improving the reliability of MPI programs is challenging  (Gopalakrishnan et al., 2011, 2017).

Program analysis (Nielson et al., 2015) is an effective technique for improving program reliability. Existing methods for analyzing MPI programs can be categorized into dynamic and static approaches. Most existing methods are dynamic, such as debugging (Laguna et al., 2015), correctness checking (Samofalov et al., 2005) and dynamic verification (Vakkalanka et al., 2008). These methods need concrete inputs to run MPI programs and perform analysis based on runtime information. Hence, dynamic approaches may miss input-related program errors. Static approaches (Siegel, 2007; López et al., 2015; Bronevetsky, 2009; Botbol et al., 2017) analyze abstract models of MPI programs and suffer from false alarms, manual effort, and poor scalability. To the best of our knowledge, existing automated verification approaches for MPI programs either do not support input-related analysis or fail to support the analysis of the MPI programs with non-blocking operations, the invocations of which do not block the program execution. Non-blocking operations are ubiquitous in real-world MPI programs for improving the performance but introduce more complexity to programming.

Symbolic execution (King, 1976; Godefroid et al., 2005) supports input-related analysis by systematically exploring a program’s path space. In principle, symbolic execution provides a balance between concrete execution and static abstraction with improved input coverage or more precise program abstraction. However, symbolic execution based analyses suffer from path explosion due to the exponential increase of program paths w.r.t. the number of conditional statements. The problem is particularly severe when analyzing MPI programs because of parallel execution and non-deterministic operations. Existing symbolic execution based verification approaches (Siegel and Zirkel, 2011b)(Fu et al., 2015) do not support non-blocking MPI operations.

In this work, we present MPI-SV, a novel verifier for MPI programs by smartly integrating symbolic execution and model checking. As far as we know, MPI-SV is the first automated verifier that supports non-blocking MPI programs and LTL (Manna and Pnueli, 1992) property verification. MPI-SV uses symbolic execution to extract path-level models from MPI programs and verifies the models w.r.t. the expected properties by model checking (Clarke et al., 1999). The two techniques complement each other: (1) symbolic execution abstracts the control and data dependencies to generate verifiable models for model checking, and (2) model checking improves the scalability of symbolic execution by leveraging the verification results to prune redundant paths and enlarges the scope of verifiable properties of symbolic execution.

In particular, MPI-SV combines two algorithms: (1) symbolic execution of non-blocking MPI programs with non-deterministic operations, and (2) modeling and checking the behaviors of an MPI program path precisely. To safely handle non-deterministic operations, the first algorithm delays the message matchings of non-deterministic operations as much as possible. The second algorithm extracts a model from an MPI program path. The model represents all the path’s equivalent behaviors, i.e., the paths generated by changing the interleavings and matchings of the communication operations in the path. We have proved that our modeling algorithm is precise and consistent with the MPI standard (Forum, 2012). We feed the generated models from the second algorithm into a model checker to perform verification w.r.t. the expected properties, i.e., safety and liveness properties in linear temporal logic (LTL) (Manna and Pnueli, 1992). If the extracted model from a path $p$ satisfies the property $\varphi$, $p$’s equivalent paths can be safely pruned; otherwise, if the model checker reports a counterexample, a violation of $\varphi$ is found. This way, we significantly boost the performance of symbolic execution by pruning a large set of paths which are equivalent to certain paths that have been already model-checked.

We have implemented MPI-SV for MPI C programs based on Cloud9 (Bucur et al., 2011) and PAT (Sun et al., 2009). We have used MPI-SV to analyze 12 real-world MPI programs, totaling 47K lines of code (LOC) (three are beyond the scale that the state-of-the-art MPI verification tools can handle), w.r.t. the deadlock freedom property and non-reachability properties. For the 111 deadlock freedom verification tasks, when we set the time threshold to be an hour, MPI-SV can complete 100 tasks, i.e., deadlock reported or deadlock freedom verified, while pure symbolic execution can complete 61 tasks. For the 100 completed tasks, MPI-SV achieves, on average, 19x speedups on verifying deadlock freedom and 5x speedups on finding a deadlock.

The main contributions of this work are:

• •

A synergistic framework combining symbolic execution and model checking for verifying MPI programs.

• •

A method for symbolic execution of non-blocking MPI programs with non-deterministic operations. The method is formally proven to preserve the correctness of verifying reachability properties.

• •

A precise method for modeling the equivalent behaviors of an MPI path, which enlarges the scope of the verifiable properties and improves the scalability.

• •

A tool for symbolic verification of MPI C programs and an extensive evaluation on real-world MPI programs.

2. Illustration

In this section, we first introduce MPI programs and use an example to illustrate the problem that this work targets. Then, we overview MPI-SV informally by the example.

2.1. MPI Syntax and Motivating Example

MPI implementations, such as MPICH (Gropp, 2002) and OpenMPI (Gabriel et al., 2004), provide the programming interfaces of message passing to support the development of parallel applications. An MPI program can be implemented in different languages, such as C and C++. Without loss of generality, we focus on MPI programs written in C. Let $\mathbb{T}$ be a set of types, $\mathbb{N}$ a set of names, and $\mathbb{E}$ a set of expressions. For simplifying the discussion, we define a core language for MPI processes in Figure 1, where $\mathbf{T}\in\mathbb{T}$, $\verb"r"\in\mathbb{N}$, and $\verb"e"\in\mathbb{E}$. An MPI program $\mathcal{MP}$ is defined by a finite set of processes $\{\textsf{Proc}_{i}\mid 0\leq i\leq n\}$. For brevity, we omit complex language features (such as the messages in the communication operations and pointer operations) although MPI-SV does support real-world MPI C programs.

The statement $\mathbf{var}\ \verb"r":\mathbf{T}$ declares a variable $\verb"r"$ with type $\mathbf{T}$. The statement $\verb"r":=\verb"e"$ assigns the value of expression $\verb"e"$ to variable $\verb"r"$. A process can be constructed from basic statements by using the composition operations including sequence, condition and loop. For brevity, we incorporate the key message passing operations in the syntax, where $\verb"e"$ indicates the destination process’s identifier. These message passing operations can be blocking or non-blocking. First, we introduce blocking operations:

• •

Ssend(e): sends a message to the eth process, and the sending process blocks until the message is received by the destination process.

• •

Send(e): sends a message to the eth process, and the sending process blocks until the message is copied into the system buffer.

• •

Recv(e): receives a message from the eth process, and the receiving process blocks until the message from the eth process is received.

• •

Recv(*): receives a message from any process, and the receiving process blocks until a message is received regardless which process sends the message.

• •

Barrier: blocks the process until all the processes have called Barrier.

• •

Wait(r): the process blocks until the operation indicated by r is completed.

A Recv(*) operation, called wildcard receive, may receive a message from different processes under different runs, resulting in non-determinism. The blocking of a Send(e) operation depends on the size of the system buffer, which may differ under different MPI implementations. For simplicity, we assume that the size of the system buffer is infinite. Hence, each Send(e) operation returns immediately after being issued. Note that our implementation allows users to configure the buffer size. To improve the performance, the MPI standard provides non-blocking operations to overlap computations and communications.

• •

ISend(e,r): sends a message to the eth process, and the operation returns immediately after being issued. The parameter r is the handle of the operation.

• •

IRecv(e,r): receives a message from the eth process, and the operation returns immediately after being issued. IRecv(*,r) is the non-blocking wildcard receive.

The operations above are key MPI operations. Complex operations, such as MPI_Bcast and MPI_Gather, can be implemented by composing these key operations. The formal semantics of the core language is defined based on communicating state machines (CSM) (Brand and Zafiropulo, 1983). We define each process as a CSM with an unbounded receiving FIFO queue. For the sake of space limit, the formal semantics can be referred to (Yu et al., 2020).

An MPI program runs in many processes spanned across multiple machines. These processes communicate by message passing to accomplish a parallel task. Besides parallel execution, the non-determinism in MPI programs mainly comes from two sources: (1) inputs, which may influence the communication through control flow, and (2) wildcard receives, which lead to highly non-deterministic executions.

Consider the MPI program in Figure 2. Processes $P_{0}$, $P_{2}$ and $P_{3}$ only send a message to $P_{1}$ and then terminate. For process $P_{1}$, if input $x$ is not equal to ‘a’, $P_{1}$ receives a message from $P_{0}$ in a blocking manner; otherwise, $P_{1}$ uses a non-blocking wildcard receive to receive a message. Then, $P_{1}$ receives a message from $P_{3}$. When $x$ is ‘a’ and IRecv(,req) receives the message from $P_{3}$, a deadlock occurs, i.e., $P_{1}$ blocks at Recv(3), and all the other processes terminate. Hence, to detect the deadlock, we need to handle the non-determinism caused by the input $x$ and the wildcard receive IRecv(,req).

To handle non-determinism due to the input, a standard remedy is symbolic execution (King, 1976). However, there are two challenges. The first one is to systematically explore the paths of an MPI program with non-blocking and wildcard operations, which significantly increase the complexity of MPI programs. A non-blocking operation does not block but returns immediately, causing out-of-order completion. The difficulty in handling wildcard operations is to get all the possibly matched messages. The second one is to improve the scalability of the symbolic execution. Symbolic execution struggles with path explosion. MPI processes run concurrently, resulting in an exponential number of program paths w.r.t. the number of processes. Furthermore, the path space increases exponentially with the number of wildcard operations.

2.2. Our Approach

MPI-SV leverages dynamic verification (Vakkalanka et al., 2008) and model checking (Clarke et al., 1999) to tackle the challenges. Figure 3 shows MPI-SV’s basic framework. The inputs of MPI-SV are an MPI program and an expected property, e.g., deadlock freedom expressed in LTL. MPI-SV uses the built-in symbolic executor to explore the path space automatically and checks the property along with path exploration. For a path that violates the property, called a violation path, MPI-SV generates a test case for replaying, which includes the program inputs, the interleaving sequence of MPI operations and the matchings of wildcard receives. In contrast, for a violation-free path $p$, MPI-SV builds a communicating sequential process (CSP) model $\Gamma$, which represents the paths which can be obtained based on $p$ by changing the interleavings and matchings of the communication operations in $p$. Then, MPI-SV utilizes a CSP model checker to verify $\Gamma$ w.r.t. the property. If the model checker reports a counterexample, a violation is found; otherwise, if $\Gamma$ satisfies the property, MPI-SV prunes all behaviors captured by the model so that they are avoided by symbolic execution.

Since MPI processes are memory independent, MPI-SV will select a process to execute in a round-robin manner to avoid exploring all interleavings of the processes. A process keeps running until it blocks or terminates. When encountering an MPI operation, MPI-SV records the operation instead of executing it and doing the message matching. When every process blocks or terminates and at least one blocked process exists, MPI-SV matches the recorded MPI operations of the processes w.r.t. the MPI standard (Forum, 2012). The intuition behind this strategy is to collect the message exchanges as thoroughly as possible, which helps find possible matchings for the wildcard receive operations. Consider the MPI program in Figure 2 and the deadlock freedom property. Figure 4 shows the symbolic execution tree, where the node labels indicate process communications, e.g., $(3,1)$ means that $P_{1}$ receives a message from $P_{3}$. MPI-SV first symbolically executes $P_{0}$, which only sends a message to $P_{1}$. The Send(1) operation returns immediately with the assumption of infinite system buffers. Hence, $P_{0}$ terminates, and the operation Send(1) is recorded. Then, MPI-SV executes $P_{1}$ and explores both branches of the conditional statement as follows.

(1) True branch ($\mathbf{x}\neq$ ‘a’). In this case, $P_{1}$ blocks at Recv(0). MPI-SV records the receive operation for $P_{1}$, and starts executing $P_{2}$. Like $P_{0}$, $P_{2}$ executes operation Send(1) and terminates, after which $P_{3}$ is selected and behaves the same as $P_{2}$. After $P_{3}$ terminates, the global execution blocks, i.e., $P_{1}$ blocks and all the other processes terminate. When this happens, MPI-SV matches the recorded operations, performs the message exchanges and continues to execute the matched processes. The Recv(0) in $P_{1}$ should be matched with the Send(1) in $P_{0}$. After executing the send and receive operations, MPI-SV selects $P_{1}$ to execute, because $P_{0}$ terminates. Then, $P_{1}$ blocks at Recv(3). Same as earlier, the global execution blocks and operation matching needs to be done. Recv(3) is matched with the Send(1) in $P_{3}$. After executing the Recv(3) and Send(1) operations, all the processes terminate successfully. Path $p_{1}$ in Figure 4 is explored.

(2) False branch ($\mathbf{x}$ =‘a’). The execution of $P_{1}$ proceeds until reaching the blocking receive Recv(3). Additionally, the two issued receive operations, i.e., IRecv(,req) and Recv(3), are recorded. Similar to the true branch, when every process blocks or terminates, we handle operation matching. Here $P_{0}$, $P_{2}$ and $P_{3}$ terminate, and $P_{1}$ blocks at Recv(3). IRecv(,req) should be matched first because of the non-overtaken policy in the MPI standard (Forum, 2012). There are three Send operation candidates from $P_{0}$, $P_{2}$ and $P_{3}$, respectively. MPI-SV forks a state for each candidate. Suppose MPI-SV first explores the state where IRecv(*,req) is matched with $P_{0}$’s Send(1). After matching and executing $P_{1}$’s Recv(3) and $P_{3}$’s Send(1), the path terminates successfully, which generates path $p_{2}$ in Figure 4.

Violation detection**.** MPI-SV continues to explore the remaining two cases. Without CSP-based boosting, the deadlock would be found in the last case (i.e., $p_{4}$ in Figure 4), where IRecv(,req) is matched with $P_{3}$’s Send(1) and $P_{1}$ blocks because Recv(3) has no matched operation. MPI-SV generates a CSP model $\Gamma$ based on the deadlock-free path $p_{2}$ where $P_{1}$’s IRecv(,req) is matched with $P_{0}$’s Send(1). Each MPI process is modeled as a CSP process, and all the CSP processes are composed in parallel to form $\Gamma$. Notably, in $\Gamma$, we collect the possible matchings of a wildcard receive through statically matching the arguments of operations in the path. Additionally, the requirements in the MPI standard, i.e., completes-before relations (Vakkalanka et al., 2008), are also modeled. A CSP model checker then verifies deadlock freedom for $\Gamma$. The model checker reports a counterexample where IRecv(*,req) is matched with the Send(1) in $P_{3}$. MPI-SV only explores two paths for detecting the deadlock and avoids the exploration of $p_{3}$ and $p_{4}$ (indicated by dashed lines).

Pruning**.** Because the CSP modeling is precise (cf. Section 4), in addition to finding violations earlier, MPI-SV can also perform path pruning when the model satisfies the property. Suppose we change the program in Figure 2 to be the one where the last statement of $P_{1}$ is a Recv(*) operation. Then, the program is deadlock free. The true branch ($x\neq$ ‘a’) has 2 paths, because the last wildcard receive in $P_{1}$ has two matchings (i.e., $P_{2}$’s send and $P_{3}$’s send, and $P_{0}$’s send has been matched by $P_{1}$’s Recv(0)). The false branch ($x=$ ‘a’) has 6 paths because the first wildcard receive has 3 matchings (send operations from $P_{0}$, $P_{2}$ and $P_{3}$) and the last wildcard receive has 2 matchings (because the first wildcard receive has matched one send operation). Hence, in total, there are 8 paths (i.e., $2+3*2=8$) if we use pure symbolic execution. In contrast, with model checking, MPI-SV only needs 2 paths to verify that the program is deadlock-free. For each branch, the generated model is verified to be deadlock-free, so MPI-SV prunes the candidate states forked for the matchings of the wildcard receives.

Properties**.** Because our CSP modeling encodes the interleavings of the MPI operations in the MPI processes, the scope of the verifiable properties is enlarged, i.e., MPI-SV can verify safety and liveness properties in LTL. Suppose we change the property to be the one that requires the Send(1) operation in $P_{0}$ should be completed before the Send(1) operation in $P_{2}$. Actually, the send operation in $P_{2}$ can be completed before the send operation in $P_{0}$, due to the nature of parallel execution. However, pure symbolic execution fails to detect the property violation. In contrast, with the help of CSP modeling, when we verify the model generated from the first path w.r.t. the property, the model checker gives a counterexample, indicating that a violation of the property exists.

3. Symbolic Verification Method

In this section, we present our symbolic verification framework and then describe MPI-SV’s symbolic execution method.

3.1. Framework

Given an MPI program $\mathcal{MP}=\{\textsf{Proc}_{i}\mid 0\leq i\leq n\}$, a state $S_{c}$ in $\mathcal{MP}$’s symbolic execution is composed by the states of processes, i.e., $(s_{0},...,s_{n})$, and each MPI process’s state is a 6-tuple $(\mathcal{M},\mathit{Stat},\mathit{PC},\mathcal{F},\mathcal{B},\mathcal{R})$, where $\mathcal{M}$ maps each variable to a concrete value or a symbolic value, $\mathit{Stat}$ is the next program statement to execute, $\mathit{PC}$ is the process’s path constraint (King, 1976), $\mathcal{F}$ is the flag of process status belonging to $\{\mathsf{active},\mathsf{blocked},\mathsf{terminated}\}$, $\mathcal{B}$ and $\mathcal{R}$ are infinite buffers for storing the issued MPI operations not yet matched and the matched MPI operations, respectively. We use $s_{i}\in S_{c}$ to denote that $s_{i}$ is a process state in the global state $S_{c}$. An element $elem$ of $s_{i}$ can be accessed by $s_{i}.elem$, e.g., $s_{i}.\mathcal{F}$ is the $i$th process’s status flag. In principle, a statement execution in any process advances the global state, making $\mathcal{MP}$’s state space exponential to the number of processes. We use variable $Seq_{i}$ defined in $\mathcal{M}$ to record the sequence of the issued MPI operations in $\textsf{Proc}_{i}$, and $\mathsf{Seq}(S_{c})$ to denote the set $\{Seq_{i}\mid 0\leq i\leq n\}$ of global state $S_{c}$. Global state $S_{c}$’s path condition (denoted by $S_{c}.PC$) is the conjunction of the path conditions of $S_{c}$’s processes, i.e., $\bigwedge\limits_{s_{i}\in S_{c}}s_{i}.PC$.

Algorithm 1 shows the details of MPI-SV. We use $\mathit{worklist}$ to store the global states to be explored. Initially, $\mathit{worklist}$ only contains $S_{init}$, composed of the initial states of all the processes, and each process’s status is $\mathsf{active}$. At Line 1, Select picks a state from $\mathit{worklist}$ as the one to advance. Hence, Select can be customized with different search heuristics, e.g., depth-first search (DFS). Then, Scheduler selects an active process $\textsf{Proc}_{i}$ to execute. Next, Execute (cf. Algorithm 2) symbolically executes the statement $Stat_{i}$ in $\textsf{Proc}_{i}$, and may add new states into $\mathit{worklist}$. This procedure continues until $\mathit{worklist}$ is empty (i.e., all the paths have been explored), detecting a violation or time out (omitted for brevity). After executing $Stat_{i}$, if all the processes in the current global state $S_{c}$ terminate, i.e., a violation-free path terminates, we use Algorithm 4 to generate a CSP model $\Gamma$ from the current state (Line 1). Then, we use a CSP model checker to verify $\Gamma$ w.r.t. $\varphi$. If $\Gamma$ satisfies $\varphi$ (denoted by $\Gamma\models\varphi$), we prune the global states forked by the wildcard operations along the current path (Line 1), i.e., the states in $\mathit{worklist}$ whose path conditions imply $S_{c}$’s path condition; otherwise, if the model checker gives a counterexample, we report the violation and exit (Line 1).

Since MPI processes are memory independent, we employ partial order reduction (POR) (Clarke et al., 1999) to reduce the search space. Scheduler selects a process in a round-robin fashion from the current global state. In principle, Scheduler starts from the active MPI process with the smallest identifier, e.g., $\textsf{Proc}_{0}$ at the beginning, and an MPI process keeps running until it is blocked or terminated. Then, the next active process will be selected to execute. Such a strategy significantly reduces the path space of symbolic execution. Then, with the help of CSP modeling and model checking, MPI-SV can verify more properties, i.e., safety and liveness properties in LTL. The details of such technical improvements will be given in Section 4.

3.2. Blocking-driven Symbolic Execution

Algorithm 2 shows the symbolic execution of a statement. Common statements such as conditional statements are handled in the standard way (King, 1976) (omitted for brevity), and here we focus on MPI operations.

The main idea is to delay the executions of MPI operations as much as possible, i.e., trying to get all the message matchings. Instead of execution, Algorithm 2 records each MPI operation for each MPI process (Lines 2&2). We also need to update buffer $\mathcal{B}$ after issuing an MPI operation (Lines 2&2). Then, if $Stat_{i}$ is a non-blocking operation, the execution returns immediately; otherwise, we block $\textsf{Proc}_{i}$ (Line 2, excepting the Wait of an ISend operation). When reaching GlobalBlocking (Lines 2&2), i.e., every process is terminated or blocked, we use Matching (cf. Algorithm 3) to match the recorded but not yet matched MPI operations and execute the matched operations. Since the opportunity of matching messages is GlobalBlocking, we call it blocking-driven symbolic execution.

Matching matches the recorded MPI operations in different processes. To obtain all the possible matchings, we delay the matching of a wildcard operation as much as possible. We use $\textsf{match}_{N}$ to match the non-wildcard operations first (Line 3) w.r.t. the rules in the MPI standard (Forum, 2012), especially the non-overtaken ones: (1) if two sends of a process send messages to the same destination, and both can match the same receive, the receive should match the first one; and (2) if a process has two receives, and both can match a send, the first receive should match the send. The matched send and receive operations will be executed, and the statuses of the involved processes will be updated to active, denoted by $\textsf{Fire}(S_{c},\mathit{pair}_{n})$ (Line 3). If there is no matching for non-wildcard operations, we use $\textsf{match}_{W}$ to match the wildcard operations (Line 3). For each possible matching of a wildcard receive, we fork a new state (denoted by $\textsf{fork}(S_{c},\mathit{pair}_{w})$ at Line 3) to analyze each matching case. If no operations can be matched, but there exist blocked processes, a deadlock happens (Line 3). Besides, for the LTL properties other than deadlock freedom (such as temporal properties), we also check them during symbolic execution (omitted for brevity).

Take the program in Figure 5 for example. When all the processes block at Barrier, MPI-SV matches the recorded operation in the buffers of the processes, i.e., $s_{0}.\mathcal{B}{=}\langle\verb"ISend(1,req"_{1}){,}\verb"Barrier"\rangle$, $s_{1}.\mathcal{B}{=}\langle\verb"IRecv(*,req"_{2}\verb")",\verb"Barrier"\rangle$, and $s_{2}.\mathcal{B}{=}\langle\verb"Barrier"\rangle$. According to the MPI standard, each operation in the buffers is ready to be matched. Hence, Matching first matches the non-wildcard operations, i.e., the Barrier operations, then the status of each process becomes $\mathsf{active}$. After that, MPI-SV continues to execute the active processes and record issued MPI operations. The next GlobalBlocking point is: $P_{0}$ and $P_{2}$ terminate, and $P_{1}$ blocks at Wait(req2). The buffers are $\langle\verb"ISend(1,req"_{1}\verb")"{,}\verb"Wait(req"_{1}\verb")"\rangle$, $\langle\verb"IRecv(*,req"_{2}\verb")"{,}\verb"Wait(req"_{2}\verb")"\rangle$, and $\langle\verb"ISend(1,req"_{3}\verb")",\verb"Wait(req"_{3}\verb")"\rangle$, respectively. All the issued Wait operations are not ready to match, because the corresponding non-blocking operations are not matched. So Matching needs to match the wildcard operation, i.e., $\verb"IRecv(*,req"_{2}\verb")"$, which can be matched with $\verb"ISend(1,req"_{1}\verb")"$ or $\verb"ISend(1,req"_{3}\verb")"$. Then, a new state is forked for each case and added to the $\mathit{worklist}$.

Correctness. Blocking-driven symbolic execution is an instance of model checking with POR. We have proved the symbolic execution method is correct for reachability properties (Manna and Pnueli, 1992). Due to the space limit, the proof can be referred to (Yu et al., 2020).

4. CSP Based Path Modeling

In this section, we first introduce the CSP (Roscoe, 2005) language. Then, we present the modeling algorithm of an MPI program terminated path using a subset of CSP. Finally, we prove the soundness and completeness of our modeling.

4.1. CSP Subset

Let $\Sigma$ be a finite set of events, $\mathbb{C}$ a set of channels, and $\mathbf{X}$ a set of variables. Figure 6 shows the syntax of the CSP subset, where $P$ denotes a CSP process, $a{\in}\Sigma$, $c{\in}\mathbb{C}$, $X{\subseteq}\Sigma$ and $x{\in}\mathbf{X}$.

The single event process $a$ performs the event $a$ and terminates. There are three operators: sequential composition ($\fatsemi$), external choice ($\square$) and parallel composition with synchronization ($\underset{X}{\parallel}$). $P\square Q$ performs as $P$ or $Q$, and the choice is made by the environment. Let $PS$ be a finite set of processes, $\square PS$ denotes the external choice of all the processes in $PS$. $P\underset{X}{\parallel}Q$ performs $P$ and $Q$ in an interleaving manner, but $P$ and $Q$ synchronize on the events in $X$. The process $c?x\rightarrow P$ performs as $P$ after reading a value from channel $c$ and writing the value to variable $x$. The process $c!x\rightarrow P$ writes the value of $x$ to channel $c$ and then behaves as $P$. Process skip terminates immediately.

4.2. CSP Modeling

For each violation-free program path, Algorithm 4 builds a precise CSP model of the possible communication behaviors by changing the matchings and interleavings of the communication operations along the path.

The basic idea is to model the communication operations in each process as a CSP process, then compose all the CSP processes in parallel to form the model. To model $\textsf{Proc}_{i}$, we scan its operation sequence $Seq_{i}$ in reverse. For each operation, we generate its CSP model and compose the model with that of the remaining operations in $Seq_{i}$ w.r.t. the semantics of the operation and the MPI standard (Forum, 2012). The modeling algorithm is efficient, and has a polynomial time complexity w.r.t. the total length of the recorded MPI operation sequences.

We use channel operations in CSP to model send and receive operations. Each send operation $op$ has its own channel, denoted by $\textsf{Chan}(op)$. We use a zero-sized channel to model Ssend operation (Line 4), because Ssend blocks until the message is received. In contrast, considering a Send or ISend operation is completed immediately, we use one-sized channels for them (Line 4), so the channel writing returns immediately. The modeling of Barrier (Line 4) is to generate a synchronization event that requires all the parallel CSP processes to synchronize it (Lines 4&4). The modeling of receive operations consists of three steps. The first step calculates the possibly matched channels written by the send operations (Lines 4&4). The second uses the external choice of reading actions of the matched channels (Lines 4&4), so as to model different cases of the receive operation. Finally, the refined external choice process is composed with the remaining model. If the operation is blocking, the composition is sequential (Line 4); otherwise, it is a parallel composition (Line 4).

$\textsf{StaticMatchedChannel}(op_{j},S)$ (Lines 4&4) returns the set of the channels written by the possibly matched send operations of the receive operation $op_{j}$. We scan $\mathsf{Seq}(S)$ to obtain the possibly matched send operations of $op_{j}$. Given a receive operation $recv$ in process $\textsf{Proc}_{i}$, $\textsf{SMO}(recv,S)$ calculated as follows denotes the set of the matched send operations of $recv$.

• •

If $recv$ is $\verb"Recv"(j)$ or $\verb"IRecv"(j,\verb"r")$, $\textsf{SMO}(recv,S)$ contains $\textsf{Proc}_{j}$’s send operations with $\textsf{Proc}_{i}$ as the destination process.

• •

If $recv$ is $\verb"Recv"(*)$ or $\verb"IRecv"(*,\verb"r")$, $\textsf{SMO}(recv,S)$ contains any process’s send operations with $\textsf{Proc}_{i}$ as the destination process.

$\textsf{SMO}(op,S)$ over-approximates $op$’s precisely matched operations, and can be optimized by removing the send operations that are definitely executed after $op$’s completion, and the ones whose messages are definitely received before $op$’s issue. For example, Let $\mathsf{Proc}_{0}$ be Send(1);Barrier;Send(1), and $\mathsf{Proc}_{1}$ be Recv();Barrier. SMO will add the two send operations in $\mathsf{Proc}_{0}$ to the matching set of the Recv() in $\mathsf{Proc}_{1}$. Since Recv(*) must complete before $\verb"Barrier"$, we can remove the second send operation in $\mathsf{Proc}_{0}$. Such optimization reduces the complexity of the CSP model. For brevity, we use $\textsf{SMO}(op,S)$ to denote the optimized matching set. Then, $\textsf{StaticMatchedChannel}(op_{j},S)$ is $\{\textsf{Chan}(op)\mid op\in\textsf{SMO}(op_{j},S)\}$.

To satisfy the MPI requirements, $\textsf{Refine}(P,S)$ (Lines 4&4) refines the models of receive operations by imposing the completes-before requirements (Vakkalanka et al., 2008) as follows:

• •

If a receive operation has multiple matched send operations from the same process, it should match the earlier issued one. This is ensured by checking the emptiness of the dependent channels.

• •

The receive operations in the same process should be matched w.r.t. their issue order if they receive messages from the same process, except the conditional completes-before pattern (Vakkalanka et al., 2008). We use one-sized channel actions to model these requirements.

We model a Wait operation if it corresponds to an IRecv operation (Line 4), because ISend operations complete immediately under the assumption of infinite system buffer. Wait operations are modeled by the synchronization in parallel processes. GenerateEvent generates a new synchronization event $e_{w}$ for each Wait operation (Line 4). Then, $e_{w}$ is produced after the corresponding non-blocking operation is completed (Line 4). The synchronization on $e_{w}$ ensures that a Wait operation blocks until the corresponding non-blocking operation is completed.

We use the example in Figure 5 for a demonstration. After exploring a violation-free path, the recorded operation sequences are $Seq_{0}{=}\langle\verb"ISend(1,req"_{1}\verb")",\verb"Barrier",\verb"Wait"\verb"(req"_{1}\verb")"\rangle$, $Seq_{1}{=}\langle\verb"IRecv(*,req"_{2}\verb")",$

$\verb"Barrier"{,}\verb"Wait(req"_{2}\verb")"\rangle$, $Seq_{2}{=}\langle\verb"Barrier"{,}\verb"ISend(1,req"_{3}\verb")"{,}\verb"Wait(req"_{3}\verb")"\rangle$. We first scan $Seq_{0}$ in reverse. Note that we don’t model Wait(req1), because it corresponds to ISend. We create a synchronization event B for modeling Barrier (Lines 4&4). For the ISend(1,req1), we model it by writing an element $a$ to a one-sized channel $chan_{1}$, and use prefix operation to compose its model with B (Lines 4-4). In this way, we generate CSP process $chan_{1}!a{\rightarrow}\verb"B"\fatsemi\textbf{skip}$ (denoted by $\mathit{CP}_{0}$) for $\mathsf{Proc}_{0}$. Similarly, we model $\mathsf{Proc}_{2}$ by $\verb"B"\fatsemi chan_{2}!b{\rightarrow}\textbf{skip}$ (denoted by $\mathit{CP}_{2}$), where $chan_{2}$ is also a one-sized channel and $b$ is a channel element. For $\mathsf{Proc}_{1}$, we generate a single event process $e_{w}$ to model Wait(req2), because it corresponds to IRecv (Lines 4-4). For IRecv(*,req2), we first compute the matched channels using SMO (Line 4), and $\textsf{StaticMatchedChannel}(op_{j},S)$ contains both $chan_{1}$ and $chan_{2}$. Then, we generate the following CSP process

[TABLE]

(denoted by $\mathit{CP}_{1}$) for $\mathsf{Proc}_{1}$. Finally, we compose the CSP processes using the parallel operator to form the CSP model (Line 4), i.e., $\mathit{CP}_{0}\underset{\{\texttt{B}\}}{\parallel}\ \mathit{CP}_{1}\underset{\{\texttt{B}\}}{\parallel}\ \mathit{CP}_{2}$.

CSP modeling supports the case where communications depend on message contents. MPI-SV tracks the influence of a message during symbolic execution. When detecting that the message content influences the communications, MPI-SV symbolizes the content on-the-fly. We specially handle the widely used master-slave pattern for dynamic load balancing (Gropp et al., 2014). The basic idea is to use a recursive CSP process to model each slave process and a conditional statement for master process to model the communication behaviors of different matchings. We verified five dynamic load balancing MPI programs in our experiments (cf. Section 5.4). The details for supporting master-slave pattern is in Appendix A.3.

4.3. Soundness and Completeness

In the following, we show that the CSP modeling is sound and complete. Suppose GenerateCSP($S$) generates the CSP process $\textsf{CSP}_{s}$. Here, soundness means that $\textsf{CSP}_{s}$ models all the possible behaviors by changing the matchings or interleavings of the communication operations along the path to $S$, and completeness means that each trace in $\textsf{CSP}_{s}$ represents a real behavior that can be derived from $S$ by changing the matchings or interleavings of the communications.

Since we compute $\textsf{SMO}(op,S)$ by statically matching the arguments of the recorded operations, $\textsf{SMO}(op,S)$ may contain some false matchings. Calculating the precisely matched operations of $op$ is NP-complete (Forejt et al., 2014), and we suppose such an ideal method exists. We use $\textsf{CSP}_{static}$ and $\textsf{CSP}_{ideal}$ to denote the generated models using $\textsf{SMO}(op,S)$ and the ideal method, respectively. The following theorems ensure the equivalence of the two models under the stable-failure semantics (Roscoe, 2005) of CSP and $\textsf{CSP}_{static}$’s consistency to the MPI semantics, which imply the soundness and completeness of our CSP modeling method. Let $\mathcal{T}(P)$ denote the trace set (Roscoe, 2005) of CSP process $P$, and $\mathcal{F}(P)$ denote the failure set of CSP process $P$. Each element in $\mathcal{F}(P)$ is $(s,X)$, where $s\in\mathcal{T}(P)$ is a trace, and $X$ is the set of events $P$ refuses to perform after $s$.

Theorem 4.1**.**

$\mathcal{F}(\emph{{CSP}}_{static})=\mathcal{F}(\emph{{CSP}}_{ideal})$.

Proof.

We only give the skeleton of the proof. We first prove

[TABLE]

based on which we can prove $\mathcal{F}(\emph{{CSP}}_{static})=\mathcal{F}(\emph{{CSP}}_{ideal})$. The main idea of proving these two equivalence relations is to use contradiction for proving the subset relations. We only give the proof of $\mathcal{T}(\textsf{CSP}_{static})\subseteq\mathcal{T}(\textsf{CSP}_{ideal})$; the other subset relations can be proved in a similar way.

Suppose there is a trace $t{=}\langle e_{1},...,e_{n}\rangle$ such that $t\in\mathcal{T}(\textsf{CSP}_{static})$ but $t{\notin}\mathcal{T}(\textsf{CSP}_{ideal})$. The only difference between $\textsf{CSP}_{static}$ and $\textsf{CSP}_{ideal}$ is that $\textsf{CSP}_{static}$ introduces more channel read operations during the modeling of receive operations. Hence, there must exist a read operation of an extra channel in $t$. Suppose the first extra read is $e_{k}{=}c_{e}?x$, where $1\leq k\leq n$. Therefore, $c_{e}$ cannot be read in $\textsf{CSP}_{ideal}$ when the matching of the corresponding receive operation starts, but $c_{e}$ is not empty at $e_{k}$ in $\textsf{CSP}_{static}$. Despite of the size of $c_{e}$, there must exist a write operation $c_{e}!y$ in $\langle e_{1},...,e_{k-1}\rangle$. Because $\langle e_{1},...,e_{k-1}\rangle$ is also a valid trace in $\textsf{CSP}_{ideal}$, it means $c_{e}$ is not empty in $\textsf{CSP}_{ideal}$ at $e_{k}$, which contradicts with the assumption that $c_{e}$ cannot be read in $\textsf{CSP}_{ideal}$. Hence, $\mathcal{T}(\textsf{CSP}_{static})\subseteq\mathcal{T}(\textsf{CSP}_{ideal})$ holds. ∎

Theorem 4.2**.**

$\emph{{CSP}}_{static}$* is consistent with the MPI semantics.*

The proof’s main idea is to prove that $\textsf{CSP}_{ideal}$ is equal to the model defined by the formal MPI semantics (Yu et al., 2020) w.r.t. the failure divergence semantics. Then, based on Theorem 4.1, we can prove that $\emph{{CSP}}_{static}$ is consistent with the MPI semantics. Please refer to (Yu et al., 2020) for the detailed proofs for these two theorems.

5. Experimental Evaluation

In this section, we first introduce the implementation of MPI-SV, then describes the research questions and the experimental setup. Finally, we give experimental results.

5.1. Implementation

We have implemented MPI-SV based on Cloud9 (Bucur et al., 2011), which is built upon KLEE (Cadar et al., 2008), and enhances KLEE with better support for POSIX environment and parallel symbolic execution. We leverage Cloud9’s support for multi-threaded programs. We use a multi-threaded library for MPI, called AzequiaMPI (Rico-Gallego and Martín, 2011), as the MPI environment model for symbolic execution. MPI-SV contains three main modules: program preprocessing, symbolic execution, and model checking. The program preprocessing module generates the input for symbolic execution. We use Clang to compile an MPI program to LLVM bytecode, which is then linked with the pre-compiled MPI library AzequiaMPI. The symbolic execution module is in charge of path exploration and property checking. The third module utilizes the state-of-the-art CSP model checker PAT (Sun et al., 2009) to verify CSP models, and uses the output of PAT to boost the symbolic executor.

5.2. Research Questions

We conducted experiments to answer the following questions:

• •

Effectiveness: Can MPI-SV verify real-world MPI programs effectively? How effective is MPI-SV when compared to the existing state-of-the-art tools?

• •

Efficiency: How efficient is MPI-SV when verifying real-world MPI programs? How efficient is MPI-SV when compared to the pure symbolic execution?

• •

Verifiable properties : Can MPI-SV verify properties other than deadlock freedom?

5.3. Setup

Table 1 lists the programs analyzed in our experiments. All the programs are real-world open source MPI programs. DTG is a testing program from (Vakkalanka, 2010). Matmat, Integrate and Diffusion2d come from the FEVS benchmark suite (Siegel and Zirkel, 2011a). Matmat is used for matrix multiplication, Integrate calculates the integrals of trigonometric functions, and Diffusion2d is a parallel solver for two-dimensional diffusion equation. Gauss_elim is an MPI implementation for gaussian elimination used in (Xue et al., 2009). Heat is a parallel solver for heat equation used in (Müller et al., 2011). Mandelbrot, Sorting and Image_manip come from github. Mandelbrot parallel draws the mandelbrot set for a bitmap, Sorting uses bubble sort to sort a multi-dimensional array, and Image_manip is an MPI program for image manipulations, e.g., shifting, rotating and scaling. The remaining three programs are large parallel applications. Depsolver is a parallel multi-material 3D electrostatic solver, Kfray is a ray tracing program creating realistic images, and ClustalW is a tool for aligning gene sequences.

To evaluate MPI-SV further, we mutate (Just et al., 2014) the programs by rewriting a randomly selected receive using two rules: (1) replace Recv(i) with $\textbf{if}\ (x{>}a)\{\texttt{Recv(i)}\}\ \textbf{else}\ \{\texttt{Recv(*)}\}$; (2) replace Recv() with $\textbf{if}\ (x{>}a)\{\texttt{Recv(*)}\}\ \textbf{else}\ \{\texttt{Recv(j)}\}$. Here $x$ is an input variable, $a$ is a random value, and $j$ is generated randomly from the scope of the process identifier. The mutations for IRecv(i,r) and IRecv(,r) are similar. Rule 1 is to improve program performance and simplify programming, while rule 2 is to make the communication more deterministic. Since communications tend to depend on inputs in complex applications, such as the last three programs in Table 1, we also introduce input related conditions. For each program, we generate five mutants if possible, or generate as many as the number of receives. We don’t mutate the programs using master-slave pattern (Gropp et al., 2014), i.e., Matmat and Sorting, and only mutate the static scheduling versions of programs Integrate, Mandelbrot, and Kfray.

Baselines. We use pure symbolic execution as the first baseline because: (1) none of the state-of-the-art symbolic execution based verification tools can analyze non-blocking MPI programs, e.g., CIVL (Luo et al., 2017; Siegel et al., 2015); (2) MPI-SPIN (Siegel, 2007) can support input coverage and non-blocking operations, but it requires building models of the programs manually; and (3) other automated tools that support non-blocking operations, such as MOPPER (Forejt et al., 2014) and ISP (Vakkalanka et al., 2008), can only verify programs under given inputs. MPI-SV aims at covering both the input space and non-determinism automatically. To compare with pure symbolic execution, we run MPI-SV under two configurations: (1) Symbolic execution, i.e., applying only symbolic execution for path exploration, and (2) Our approach, i.e., using model checking based boosting. Most of the programs run with 6, 8, and 10 processes, respectively. DTG and Matmat can only be run with 5 and 4 processes, respectively. For Diffusion and the programs using the master-slave pattern, we only run them with 4 and 6 processes due to the huge path space. We use MPI-SV to verify deadlock freedom of MPI programs and also evaluate 2 non-reachability properties for Integrate and Mandelbrot. The timeout is one hour. There are three possible verification results: finding a violation, no violation, or timeout. We carry out all the tasks on an Intel Xeon-based Server with 64G memory and 8 2.5GHz cores running a Ubuntu 14.04 OS. We ran each verification task three times and use the average results to alleviate the experimental errors. To evaluate MPI-SV’s effectiveness further, we also directly compare MPI-SV with CIVL (Luo et al., 2017; Siegel et al., 2015) and MPI-SPIN (Siegel, 2007). Note that, since MPI-SPIN needs manual modeling, we only use MPI-SV to verify MPI-SPIN’s C benchmarks w.r.t. deadlock freedom.

5.4. Experimental Results

Table 2 lists the results for evaluating MPI-SV against pure symbolic execution. The first column shows program names, and #Procs is the number of running processes. T specifies whether the analyzed program is mutated, where $o$ denotes the original program, and $\textit{m}_{i}$ represents a mutant. A task comprises a program and the number of running processes. We label the programs using master-slave pattern with superscript “*”. Column Deadlock indicates whether a task is deadlock free, where 0, 1, and -1 denote no deadlock, deadlock and unknown, respectively. We use unknown for the case that both configurations fail to complete the task. Columns Time(s) and #Iterations show the verification time and the number of explored paths, respectively, where to stands for timeout. The results where Our approach performs better is in gray background.

For the 111 verification tasks, MPI-SV completes 100 tasks ($90\%$) within one hour, whereas 61 tasks ($55\%$) for Symbolic execution. Our approach detects deadlocks in 48 tasks, while the number of Symbolic execution is 44. We manually confirmed that the detected deadlocks are real. For the 48 tasks having deadlocks, MPI-SV on average offers a 5x speedups for detecting deadlocks. On the other hand, Our approach can verify deadlock freedom for 52 tasks, while only 17 tasks for Symbolic execution. MPI-SV achieves an average 19x speedups. Besides, compared with Symbolic execution, Our approach requires fewer paths to detect the deadlocks (1/55 on average) and complete the path exploration (1/205 on average). These results demonstrate MPI-SV’s effectiveness and efficiency.

Figure 7 shows the efficiency of verification for the two configurations. The X-axis varies the time threshold from 5 minutes to one hour, while the Y-axis is the number of completed verification tasks. Our approach can complete more tasks than Symbolic execution under the same time threshold, demonstrating MPI-SV’s efficiency. In addition, Our approach can complete $96\ (96\%)$ tasks in $5$ minutes, which also demonstrates MPI-SV’s effectiveness.

For some tasks, e.g., Kfray, MPI-SV does not outperform Symbolic execution. The reasons include: (a) the paths contain hundreds of non-wildcard operations, and the corresponding CSP models are huge, and thus time-consuming to model check; (b) the number of wildcard receives or their possible matchings is very small, and as a result, only few paths are pruned.

Comparison with CIVL**.** CIVL uses symbolic execution to build a model for the whole program and performs model checking on the model. In contrast, MPI-SV adopts symbolic execution to generate path-level verifiable models. CIVL does not support non-blocking operations. We applied CIVL on our evaluation subjects. It only successfully analyzed DTG. Diffusion2d could be analyzed after removing unsupported external calls. MPI-SV and CIVL had similar performance on these two programs. CIVL failed on all the remaining programs due to compilation failures or lack of support for non-blocking operations. In contrast, MPI-SV successfully analyzed 99 of the 140 programs in CIVL’s latest benchmarks. The failed ones are small API test programs for the APIs that MPI-SV does not support. For the real-world program floyd that both MPI-SV and CIVL can analyze, MPI-SV verified its deadlock-freedom under 4 processes in 3 minutes, while CIVL timed out after 30 minutes. The results indicate the benefits of MPI-SV’s path-level modeling.

Comparison with MPI-SPIN**.** MPI-SPIN relies on manual modeling of MPI programs. Inconsistencies may happen between an MPI program and its model. Although prototypes exist for translating C to Promela (Jiang and Jonsson, 2009), they are impractical for real-world MPI programs. MPI-SPIN’s state space reduction treats communication channels as rendezvous ones; thus, the reduction cannot handle the programs with wildcard receives. MPI-SV leverages model checking to prune redundant paths caused by wildcard receives. We applied MPI-SV on MPI-SPIN’s 17 C benchmarks to verify deadlock freedom, and MPI-SV successfully analyzed 15 automatically, indicating the effectiveness. For the remaining two programs, i.e., BlobFlow and Monte, MPI-SV cannot analyze them due to the lack of support for APIs. For the real-world program gausselim, MPI-SPIN needs 171s to verify that the model is deadlock-free under 5 processes, while MPI-SV only needs 27s to verify the program automatically. If the number of the processes is 8, MPI-SPIN timed out in 30 minutes, but MPI-SV used 66s to complete verification.

Temporal properties**.** We specify two temporal safety properties $\varphi_{1}$ and $\varphi_{2}$ for Integrate and Mandelbrot, respectively, where $\varphi_{1}$ requires process one cannot receive a message before process two, and $\varphi_{2}$ requires process one cannot send a message before process two. Both $\varphi_{1}$ and $\varphi_{2}$ can be represented by an LTL formula $!a$ U $b$, which requires event $a$ cannot happen before event $b$. We verify Integrate and Mandelbrot under 6 processes. The verification results show that MPI-SV detects the violations of $\varphi_{1}$ and $\varphi_{2}$, while pure symbolic execution fails to detect violations.

Runtime bugs**.** MPI-SV can also detect local runtime bugs. During the experiments, MPI-SV finds 5 unknown memory access out-of-bound bugs: 4 in DepSolver and 1 in ClustalW.

6. Related Work

Dynamic analyses are widely used for analyzing MPI programs. Debugging or testing tools (Wave, 2009; Allinea, 2002; Krammer et al., 2004; Samofalov et al., 2005; Hilbrich et al., 2012; Laguna et al., 2015; Mitra et al., 2014) have better feasibility and scalability but depend on specific inputs and running schedules. Dynamic verification techniques, e.g., ISP (Vakkalanka et al., 2008) and DAMPI (Vo et al., 2010), run MPI programs multiple times to cover the schedules under the same inputs. Böhm et al. (2016) propose a state-space reduction framework for the MPI program with non-deterministic synchronization. These approaches can detect the bugs depending on specific matchings of wildcard operations, but may still miss inputs related bugs. MPI-SV supports both input and schedule coverages, and a larger scope of verifiable properties. MOPPER (Forejt et al., 2014) encodes the deadlock detection problem under concrete inputs in a SAT equation. Similarly, Huang and Mercer (2015) use an SMT formula to reason about a trace of an MPI program for deadlock detection. However, the SMT encoding is specific for the zero-buffer mode. Khanna et al. (2018) combines dynamic and symbolic analyses to verify multi-path MPI programs. Compared with these path reasoning work in dynamic verification, MPI-SV ensures input space coverage and can verify more properties, i.e., safety and liveness properties in LTL. Besides, MPI-SV employs CSP to enable a more expressive modeling, e.g., supporting conditional completes-before (Vakkalanka et al., 2008) and master-slave pattern (Gropp et al., 2014).

For static methods of analyzing MPI program, MPI-SPIN (Siegel, 2007, ) manually models MPI programs in Promela (Holzmann, 2012), and verifies the model w.r.t. LTL properties (Manna and Pnueli, 1992) by SPIN (Holzmann, 1997) (cf. Section 5.4 for empirical comparison). MPI-SPIN can also verify the consistency between an MPI program and a sequential program, which is not supported by MPI-SV. Bronevetsky (2009) proposes parallel control flow graph (pCFG) for MPI programs to capture the interactions between arbitrary processes. But the static analysis using pCFG is hard to be automated. ParTypes (López et al., 2015) uses type checking and deductive verification to verify MPI programs against a protocol. ParTypes’s verification results are sound but incomplete, and independent with the number of processes. ParTypes does not support non-deterministic or non-blocking MPI operations. MPI-Checker (Droste et al., 2015) is a static analysis tool built on Clang Static Analyzer (Clang, 2016), and only supports intraprocedural analysis of local properties such as double non-blocking and missing wait. Botbol et al. (2017) abstract an MPI program to symbolic transducers, and obtain the reachability set based on abstract interpretation (Cousot and Cousot, 1977), which only supports blocking MPI programs and may generate false positives. COMPI (Li et al., 2018; Li et al., 2019) uses concolic testing (Godefroid et al., 2005; Sen et al., 2005) to detect assertion or runtime errors in MPI applications. Ye et al. (2018) employs partial symbolic execution (Ramos and Engler, 2015) to detect MPI usage anomalies. However, these two symbolic execution-based bug detection methods do not support the non-determinism caused by wildcard operations. Luo and Siegel (2018) propose a preliminary deductive method for verifying the numeric properties of MPI programs in an unbounded number of processes. However, this method still needs manually provided verification conditions to prove MPI programs.

MPI-SV is related to the existing work on symbolic execution (King, 1976), which has been advanced significantly during the last decade (Godefroid et al., 2005; Sen et al., 2005; Cadar et al., 2008; Bucur et al., 2011; Godefroid et al., 2008; Pasareanu et al., 2008; Tillmann and de Halleux, 2008; Wang et al., 2018; Zhang et al., 2015). Many methods have been proposed to prune paths during symbolic execution (Boonstoppel et al., 2008; Jaffar et al., 2013; Cui et al., 2013; Guo et al., 2015; Yu et al., 2018). The basic idea is to use the techniques such as slicing (Jhala and Majumdar, 2005) and interpolation (McMillan, 2005) to safely prune the paths. Compared with them, MPI-SV only prunes the paths of the same path constraint but different message matchings or operation interleavings. MPI-SV is also related to the work of automatically extracting session types (Ng and Yoshida, 2016) or behavioral types (Lange et al., 2018) for Go programs and verifying the extracted type models. These methods extract over-approximation models from Go programs, and hence are sound but incomplete. Compared with them, MPI-SV extracts path-level models for verification. Furthermore, there exists work of combining symbolic execution and model checking (Nori et al., 2009; Su et al., 2015; Daca et al., 2016). YOGI (Nori et al., 2009) and Abstraction-driven concolic testing (Daca et al., 2016) combine dynamic symbolic execution  (Godefroid et al., 2005; Sen et al., 2005) with counterexample-guided abstraction refinement (CEGAR) (Clarke et al., 2000). MPI-SV focuses on parallel programs, and the verified models are path-level. MPI-SV is also related to the work of unbounded verification for parallel programs (Bouajjani and Emmi, 2012; Bouajjani et al., 2018; Bakst et al., 2017; von Gleissenthall et al., 2019). Compared with them, MPI-SV is a bounded verification tool and supports the verification of LTL properties. Besides, MPI-SV is related to the existing work of testing and verification of shared-memory programs (Musuvathi et al., 2008; Guo et al., 2015; Guo et al., 2018; Demsky and Lam, 2015; Huang et al., 2013; Huang and Huang, 2016; Chaki et al., 2004; Cimatti et al., 2011; Kragl et al., 2018; Inverso et al., 2015; Yin et al., 2018). Compared with them, MPI-SV concentrates on message-passing programs. Utilizing the ideas in these work for analyzing MPI programs is interesting and left to the future work.

7. Conclusion

We have presented MPI-SV for verifying MPI programs with both non-blocking and non-deterministic operations. By synergistically combining symbolic execution and model checking, MPI-SV provides a general framework for verifying MPI programs. We have implemented MPI-SV and extensively evaluated it on real-world MPI programs. The experimental results are promising demonstrate MPI-SV’s effectiveness and efficiency. The future work lies in several directions: (1) enhance MPI-SV to support more MPI operations, (2) investigate the automated performance tuning of MPI programs based on MPI-SV, (3) apply our synergistic framework to other message-passing programs.

Appendix A Appendix

A.1. Semantics of the Core MPI Language

Auxiliary Definitions. Before giving the MPI language’s semantics, we give some auxiliary definitions. Given an MPI program $\mathcal{MP}=\{\textsf{Proc}_{i}\mid 0\leq i\leq n\}$, $\mathit{send(dst)}$ and $\mathit{recv(src)}$ denote $\mathcal{MP}$’s send and receive operations222$\mathit{send(dst)}$ and $\mathit{recv(src)}$ can denote both blocking and unblocking operations, and we omit the $req$ parameter for non-blocking ones for the sake of simplicity., respectively, where $dst{\in}\{0,\dots,n\}$ and $src{\in}\{0,\dots,n\}{\cup}\{*\}$. $\mathsf{op}(\mathcal{MP})$ represents the set of all the MPI operations in $\mathcal{MP}$, $\mathit{rank}(\alpha)$ is the process identifier of operation $\alpha$, and $\mathit{isBlocking}(\alpha)$ indicates whether $\alpha$ is a blocking operation.

Definition A.1.

MPI Process State. An MPI process’s state is a tuple $(\mathcal{M},\mathit{Stat},\mathcal{F},\mathcal{B},\mathcal{R})$, where $\mathcal{M}$ maps a variable to its value, $\mathit{Stat}$ is the next program statement to execute, $\mathcal{F}$ is the flag of process status and belongs to the set {$\mathsf{active}$, $\mathsf{blocked}$, $\mathsf{terminated}$}, $\mathcal{B}$ and $\mathcal{R}$ are infinite buffers to store the issued MPI operations not yet matched and the matched MPI operations, respectively.

An element $elem$ of a process state $s$ can be accessed by $s.elem$, e.g., $s.\mathcal{F}$ is the status of $s$. The behavior of a process can be regarded as a sequence of statements, and we use $index(\alpha)$ to denote the index of operation $\alpha$ in the sequence. An MPI program’s global state $S$ is composed by the states of the MPI processes, i.e., $S=(s_{0},\dots,s_{n})$. An MPI program’s semantics is a labeled transition system defined below.

Definition A.2.

Labeled Transition System. A labeled transition system (LTS) of an MPI program $\mathcal{MP}$ is a quadruple $(\mathcal{G},\Sigma,\rightarrow,\mathcal{G}_{0})$, where $\mathcal{G}$ is the set of global states, $\Sigma$ denotes the set of actions defined below, $\rightarrow\subseteq\mathcal{G}\times\Sigma\times\mathcal{G}$ represents the set of transitions, and $\mathcal{G}_{0}$ is the set of initial states.

Actions. The action set $\Sigma$ is $\{B,W,\mathit{SR},\mathit{SR}^{*}\}\cup\{\mathit{issue}({o})\mid o\in\mathsf{op}(\mathcal{MP})\}$, where $B$ represents the synchronization of Barrier, $W$ is the execution of Wait operation, $SR$ denotes the matching of message send and deterministic receive, $SR^{*}$ represents the matching of message send and wildcard receive, and $\mathit{issue}({o})$ stands for the issue of operation $o$.

Transition Rules. We first give some definitions used by the transition rules. We use $ready(\alpha,s_{i})\in\{\mathsf{True},\mathsf{False}\}$ defined as follows to indicate whether operation $\alpha$ is ready to be matched in state $s_{i}$ w.r.t. the MPI standard (Forum, 2012), where $\beta\in s_{i}.\mathcal{B}$ represents that operation $\beta$ is in the buffer $\mathcal{B}$ of process state $s_{i}$ and $k\in\{0,\dots,n\}$.

• •

If $\alpha$ is $\verb"Wait(r)"$, $\alpha$ can be matched if the waited operation has been matched, i.e., $\exists\beta{\in}\mathcal{R},(\beta{=}$ $\verb"ISend(k,r)"\vee\beta{=}\verb"IRecv(k,r)"\vee\beta{=}\verb"IRecv(*,r)")$.

• •

If $\alpha$ is $send(k)$, $\alpha$ can be matched if there is no previously issued $send(k)$ not yet matched, i.e., $\neg(\exists\beta{\in}s_{i}.\mathcal{B},index(\beta)$

$<index(\alpha)\land\beta=send(k))$.

• •

If $\alpha$ is $recv(k)$, $\alpha$ can be matched if the previously issued $recv(k)$ or $recv(*)$ has been matched, which can be formalized as $\neg(\exists\beta{\in}s_{i}.\mathcal{B},\ index(\beta)<index(\alpha)\land(\beta=recv(k)\!\lor\beta=recv(*)))$.

• •

If $\alpha$ is $recv(*)$, $\alpha$ can be matched if the previously issued $recv(*)$ has been matched, i.e., $\neg(\exists\beta{\in}s_{i}.\mathcal{B},\ index(\beta)<index(\alpha)\land\beta=recv(*))$. It is worth noting the conditional completes-before pattern (Vakkalanka et al., 2008), i.e., operation $\verb"IRecv(k,r)"$ followed by a $recv(*)$, and the $recv(*)$ can complete first when the matched message is not from $k$. We will give a condition later to ensure such relation.

Suppose $\alpha$ and $\beta$ are MPI operations, $match(\alpha,\beta)$ represents whether $\alpha$ and $\beta$ can be matched statically, and can be defined as $match^{{}^{\prime}}(\alpha,\beta)\lor match^{{}^{\prime}}(\beta,\alpha)$, where $match^{{}^{\prime}}(\alpha,\beta)$ is $((\alpha,\beta){=}(send(dst),$

$recv(src))\land(dst{=}src\lor src=*)$. We use $s_{i}[ops]$ to denote the updates of the process state $s_{i}$ with an update operation sequence $ops$. The operation $update(\mathcal{F},\alpha)$ updates the process status w.r.t. $\alpha$ as follows.

[TABLE]

$\mathcal{B}.push(\alpha)$ represents adding MPI operation $\alpha$ to buffer $\mathcal{B}$, while $\mathcal{B}.pull(\alpha)$ represents removing $\alpha$ from $\mathcal{B}$ and adding $\alpha$ to $\mathcal{R}$. We use $Stat^{\prime}$ to denote the statement next to $Stat$. We use $C(\alpha,s_{i},\beta,s_{j})$ = $C_{1}(\alpha,s_{i},\beta,s_{j})\wedge C_{1}(\beta,s_{j},\alpha,s_{i})$ to define the conditional completes-before relation requirement, where $C_{1}(\alpha,s_{i},\beta,s_{j})$ is $\neg(\exists\beta^{\prime}\in s_{j}.\mathcal{B},$

$\ (\beta{=}\verb"IRecv(*,r)"\land\beta^{\prime}{=}\verb"IRecv(i,r')"\land ready(\beta^{\prime},s_{j})\land match(\alpha,\beta^{\prime})))$.

Figure 8 shows four transition rules for MPI operations. For the sake of brevity, we omit the transition rules of local statements, which only update the mapping $\mathcal{M}$ and the next statement $Stat$ to execute. Rule $\langle\mathsf{ISSUE}\rangle$ describes the transition of issuing an MPI operation, which requires the issuing process to be $\mathsf{active}$. After issuing the operation, the process status is updated, the next statement to execute becomes $Stat^{\prime}$ (omitted for the sake of spaces), and the issued operation is added to the buffer $\mathcal{B}$. Rule $\langle\mathsf{SR}\rangle$ is about matchings of message send and receive. There are three required conditions to match a send to a receive: (1) both of them have been issued to the buffer $\mathcal{B}$ and are ready to be matched; (2) operation arguments are matched, i.e., $match(\alpha,\beta)$; (3) they comply with the conditional completes-before relation, i.e., $C(\alpha,s_{i},\beta,s_{j})$. After matching, the matched operations will be removed from buffer $\mathcal{B}$ and added to buffer $\mathcal{R}$, and the process status is updated. Rule $\langle\mathsf{B}\rangle$ is for barrier synchronization, which requires that all the processes have been blocked at the Barrier. After barrier synchronization, operation Barrier will be moved from buffer $\mathcal{B}$ to buffer $\mathcal{R}$ and all the processes become $\mathsf{active}$. Rule $\langle\mathsf{W}\rangle$ is for Wait operation, which requires the corresponding non-blocking operation has been finished. After executing Wait operation, the process becomes $\mathsf{active}$ and the Wait operation will be removed from buffer $\mathcal{B}$ and added to buffer $\mathcal{R}$.

A.2. Correctness of Symbolic Execution for MPI Programs

Round-robin schedule and blocking-driven symbolic execution is an instance of model checking with POR preserving reachability properties. Next, we prove the correctness of symbolic execution method for verifying reachability properties.

Definition A.3.

Reachability Property. A reachability property $\varphi$ of an MPI program $\mathcal{MP}$ can be defined as follows, where $\mathbf{assertion}(S)$ represents an assertion of global state $S$, e.g., deadlock and assertions of variables.

[TABLE]

$\mathbf{EF}\ \gamma$ returns true iff there exists an $\mathcal{MP}$’s state that satisfies the formula $\gamma$.

We use $S\xrightarrow{a}S^{\prime}$ to represent the transition $(S,a,S^{\prime})$ in the transition set and $\mathit{enabled}({S})$ to denote the set of enabled actions at global state $S$, i.e., $\mathit{enabled}({S}){=}\{a\mid\exists S^{\prime}\in\mathcal{G},S\xrightarrow{a}S^{\prime}\}$. If $S\xrightarrow{a}S^{\prime}$, we use $a(S)$ to represent $S^{\prime}$. Instead of exploring all the possible states, MPI-SV only executes a subset of $\mathit{enabled}({S})$ (denoted as $E(S)$) when reaching a state $S$. According to the workflow of MPI symbolic execution, we define $E(S)$ below, where

• •

$\mathit{minIssue}(S)=\mathsf{min}\{rank(o)\mid\mathit{issue}({o})\in\mathit{enabled}({S})\}$ is the minimum process identifier that can issue an MPI operation.

• •

$\mathit{minRank}(S)=\mathsf{min}\{rank_{a}(b)\mid b\in\mathit{enabled}({S})\land b\neq SR^{*}\}$ is the minimum process identifier of enabled non-wildcard actions. When $b$ is $SR$, $rank_{a}(b)$ is the process identifier of the send; when $b$ is $W$, $rank_{a}(b)$ is the process identifier of the Wait operation.

[TABLE]

When $issue(o)$ is enabled in state $S$, we will select the enabled issue operation having the smallest process identifier as $E(S)$, which is in accordance with round-robin schedule. Remember that blocking-driven matching delays the matching of wildcard receive ($SR^{*}$) as late as possible. If $B$ is enabled, we use $\{B\}$ as $E(S)$; else, we will use the deterministic matching ($W$ or $SR$) having smallest process identifier (we select $W$ in case $rank_{a}(W){=}rank_{a}(SR)$); otherwise, we use the enabled set as $E(S)$, i.e., $\forall a{\in}\mathit{enabled}({S}),\ a{=}SR^{*}$.

Definition A.4.

Independence Relation ($\mathcal{I}\subseteq\Sigma\times\Sigma$). For $S\in\mathcal{G}$ and $(a,b)\in\mathcal{I}$, $\mathcal{I}$ is a binary relation that if $(a,b)\in enabled(S)$ then $a\in enabled(b(S))$, $b\in enabled(a(S))$, and $a(b(S))=b(a(S))$.

The dependence relation $\mathcal{D}\subseteq\Sigma\times\Sigma$ is the complement of $\mathcal{I}$, i.e., $(a,b)\in\mathcal{D}$, if $(a,b)\notin\mathcal{I}$. Given an MPI program $\mathcal{MP}$, whose LTS model is $M=(\mathcal{G},\Sigma,\rightarrow,\mathcal{G}_{0})$, an execution trace $T=\langle a_{0},\dots,a_{n}\rangle\in\Sigma^{*}$ of $\mathcal{MP}$ is a sequence of actions, such that $\exists S_{i},S_{i+1}\in\mathcal{G},S_{i}\xrightarrow{a_{i}}S_{i+1}$ for each $i\in[0,n]$ and $S_{0}\in\mathcal{G}_{0}$. We use $\mathsf{r}(T)$ to represent the result state of $T$, i.e., $S_{n+1}$, and $T\in M$ to represent $T$ is an execution trace of $\mathcal{MP}$.

Definition A.5.

Execution equivalence $\equiv\;\subseteq\Sigma^{*}\times\Sigma^{*}$ is a reflexive and symmetric binary relation such that (1) $\forall\ a,b\in\Sigma,\ (a,b)\in\mathcal{I}\Rightarrow\langle a,b\rangle\equiv\langle b,a\rangle$. (2) $\forall\ T,T^{\prime}\in\Sigma^{*},\ T\equiv T^{\prime}$ if there exists a sequence $\langle T_{0},\dots,T_{k}\rangle$ that $T_{0}{=}T,\ T_{k}{=}T^{\prime}$, and for every $i{<}k,\ T_{i}=u\cdot\langle a,b\rangle\cdot v,\ T_{i+1}{=}u\cdot\langle b,a\rangle\cdot v$, where $(a,b){\in}\mathcal{I}$, $u,v{\in}\Sigma^{*}$, and $u\cdot v$ is the concatenation of $u$ and $v$.

Given an MPI program $\mathcal{MP}$, suppose $\mathcal{MP}$’s semantic model is $M$ and the $E(S)$ based model is $M^{\prime}$, once $E(S)$ satisfies conditions $\mathbf{C1}$ and $\mathbf{C2}$, then for every execution trace $T$, if $T{\in}M{\land}T{\not\in}M^{\prime}$, there exists an execution trace $T^{\prime}$ in $M^{\prime}$ that $T{\equiv}T^{\prime}$ (Penczek et al., 2000).

$\mathbf{C1.}$ $\forall$ $a\in E(S)$, if $(a,b)\in\mathcal{D}$, then for every trace $S_{0}\xrightarrow{a_{0}}S_{1}\xrightarrow{a_{1}},\dots,\xrightarrow{a_{k}}S_{k}\xrightarrow{\beta}S_{i+1}$, there exists $a_{i}\in E(S)$, where $0\leq i\leq k$.

$\mathbf{C2.}$ On every cycle in $M^{\prime}$, there exists at least one node $S$ that $E(S)=\mathit{enabled}({S})$.

Before proving our selection of $E(S)$ satisfies $\mathbf{C1}$ and $\mathbf{C2}$, we first give a theorem to show the independence relation of co-enabled actions.

Theorem A.1**.**

Given action $a\in\{\mathit{issue}({o}),B,W,SR\}$ and action $b$, for $S\in\mathcal{G}$, if $a,b\in\mathit{enabled}({S})$, then $(a,b)\in\mathcal{I}$.

Proof.

We only prove the case that $a$ is $\mathit{issue}({o})$. The proofs for the other three cases are similar. When $a{=}\mathit{issue}({o})$ and $a,b{\in}\mathit{enabled}({S})$, $b$ can be $\mathit{issue}({o^{\prime}})$, $W$, $SR$, or $SR^{*}$ w.r.t. the transition rules.

$(1)\ b{=}\mathit{issue}({o^{\prime}}).$ Suppose $rank(o){=}i$, $rank(o^{\prime}){=}j$, then $i{\neq}j$. Since an issued operation can only block its process, we can have $b\in enabled(a(S))$ and $a\in enabled(b(S))$. In addition, $a(b(S))=b(a(S))=$

$(\dots,s_{i}[update(\mathcal{F},o),Stat{:=}Stat^{\prime},\mathcal{B}.push(o)],\!\dots,s_{j}[update(\mathcal{F},\!o^{\prime}),$

$Stat{:=}Stat^{\prime},\mathcal{B}.push(o^{\prime})],\!\dots)$. Hence, $(a,b){\in}\mathcal{I}$.

$(2)\ b{=}W.$ Suppose $rank(o){=}i$, $rank_{a}(W){=}j$, then $i{\neq}j$. Since $\mathit{issue}({o})$ can only block process $i$ and $W$ can only make process $j$ active, $b{\in}enabled(a(S))$ and $a{\in}enabled(b(S))$. In addition, $a(b(S)){=}b(a(S)){=}$

$(\dots,s_{i}[update(\mathcal{F},o),Stat{:=}Stat^{\prime},\mathcal{B}.push(o)],{\dots},s_{j}[update(\mathcal{F},$

$\texttt{Wait}),\mathcal{B}.pull(\texttt{Wait})],{\dots})$. Hence, $(a,b){\in}\mathcal{I}$.

$(3)\ b{=}SR{\lor}b{=}SR^{*}.$ Suppose $b{=}(p,q)$, $rank(o){=}i$, $rank(p){=}j_{1}$, and $rank(q){=}j_{2}$. For $i{\neq}j_{1}{\land}i{\neq}j_{2}$: $\mathit{issue}({o})$ only updates the state $s_{i}$, and $ready(p,s_{j_{1}})$ and $ready(q,s_{j_{2}})$ will not be affected. On the other hand, $b$ cannot make process $i$ blocked. Hence $b{\in}enabled(a(S))$ and $a{\in}enabled(b(S))$. Then, $a(b(S)){=}b(a(S)){=}({\dots},s_{i}[update(\mathcal{F}{,}o),Stat$

${:=}Stat^{\prime},\mathcal{B}.push(o)],\dots,s_{j_{1}}[update(\mathcal{F},p),\mathcal{B}.pull(p)],{\dots},$

$s_{j_{2}}[update(\mathcal{F},q),\mathcal{B}.pull(q)],{\dots})$. For $i{=}j_{1}$: since $\mathit{issue}({o})$ and $b$ are co-enabled, $index(o){>}index(p)$ and $p$ is non-blocking. Due to the condition $index(o){>}index(p)$, $\mathit{issue}({o})$ has no effect on $ready(p,s_{j_{1}})$. On the other hand, since $p$ is non-blocking, $b$ cannot make process i blocked. Hence $b{\in}enabled(a(S))$ and $a{\in}enabled(b(S))$. Additionally, since $p$ is non-blocking, $a(b(S)){=}b(a(S)){=}(\dots,s_{i}[update(\mathcal{F},o),Stat$

${:=}Stat^{\prime},\mathcal{B}.pull(p),\mathcal{B}.push(o)],\!\dots\!,s_{j_{2}}[update(\mathcal{F},q),\mathcal{B}.pull(q)],\!\dots)$. For $i{=}j_{2}$, the proof is similar. Hence $(a,b){\in}\mathcal{I}$. ∎

Theorem A.2**.**

$E(S)$* preserves the satisfaction of global reachability properties.*

Proof.

We first prove the $E(S)$ satisfies condition $\mathbf{C1}$ and $\mathbf{C2}$, respectively.

C1: $\forall$ $a\in E(S)$, if $(a,b)\in\mathcal{D}$, then for every trace $S_{0}\xrightarrow{a_{0}}S_{1}\xrightarrow{a_{1}},\dots,\xrightarrow{a_{k}}S_{k}\xrightarrow{b}S_{i+1}$, there exists $a_{i}\in E(S)$, where $0\leq i\leq k$.

Case 1: $E(S)=\mathit{enabled}({S})$, C1 holds because $a_{0}\in E(S)$.

Case 2: $E(S)\neq\mathit{enabled}({S})$. In this case, $E(S)$ contains only one element, and can be $\mathit{issue}({o})$, $B$, $W$, or $SR$. Assume C1 does not hold, i.e., $a_{i}\neq a$. According to Theorem A.1, $(a,a_{i})\in\mathcal{I}$ and $a\in enabled(S_{i})$. Because $a,b\in enabled(S_{k})$, $(a,b)\in\mathcal{I}$, which conflicts with the premise that $(a,b)\in\mathcal{D}$. Hence C1 holds.

C2: Since there is no cycle in the labeled transition system of MPI programs, C2 holds.

Since $E(S)\subseteq\mathit{enabled}({S})$, $M^{\prime}$ is a sub model of $M$. Assume $E(S)$ does not preserve the satisfaction of global reachability property $\varphi$. According to Definition A.3, if $\varphi$ is $\mathbf{EF}\ \gamma$, i.e., there exists a state $S$ in $M$ that satisfies $\gamma$, but no state in $M^{\prime}$ satisfying $\gamma$. Since $E(S)$ satisfies C1 and C2, suppose the execution trace to $S$ is $T$, i.e., $\mathsf{r}(T)=S$, then there must exist an equivalent execution trace $T^{\prime}\in M^{\prime}$. Obviously, commuting independent actions cannot change the result state, so $\mathsf{r}(T^{\prime})=S$, which conflicts with the assumption. If $\varphi$ is $\neg\mathbf{EF}\ \gamma$, i.e., each state in $M$ does not satisfy $\gamma$, but there exists a state in $M^{\prime}$ satisfying $\gamma$, which conflicts with $M^{\prime}$ is a sub model of $M$. Hence the theorem holds.

∎

A.3. Support of Master-Slave Pattern

In real-world MPI programs, communications may depend on message contents, which makes the behavior more complicated. For example, suppose a message content is stored in variable $x$, followed by “$\textbf{if}\ (x>10)\ \verb"Send(0)";\textbf{else}\ \verb"Send(1)"$”. The general way to handle the situation where communications depend on the message contents is to make the contents symbolic. MPI-SV make $x$ to be symbolic once it detects that there exist communications depending on $x$, so that MPI-SV does not miss a branch. Master-slave pattern is a representative situation and has been widely adopted to achieve a dynamic load balancing (Gropp et al., 1999). The verification of the parallel programs employing dynamic load balancing is a common challenge. In the pattern, the master process is in charge of management, i.e., dispatching jobs to slave processes and collecting results. On the other hand, the slave processes repeatedly work on the jobs and send results back to the master process until receiving the message of termination. Figure 9 is an example program. Following shows an example program.

$P_{0}$ is the master process, and the remaining processes are slaves. $P_{0}$ first dispatches one job to each slave. Then, $P_{0}$ will iteratively receive a job result from any slave (Recv(*,r)) and dispatch a new job to the slave process whose result is just received, i.e., Send(r.src), where r is the status of the receive and r.src denotes the process identifier of the received message. Each slave process iteratively receives a job (Recv(0)), completes the job (omitted for brevity) and sends the job result to $P_{0}$ (Send(0)). The if condition becomes true when the received message is for termination. The total number of jobs is controlled by the while loop in $P_{0}$. After all the jobs have been completed, $P_{0}$ will notify all the slave processes to exit. The communication behavior of master-slave pattern is highly dynamic, i.e., the destination of the job send operation depends on the matching of the wildcard receive in the master process. In principle, if there are $n$ dynamically dispatched jobs for $m$ slaves, there exists $m^{n}$ cases of dispatching jobs. MPI-SV supports master-slave pattern as follows.

Recognition. We recognize the master-slave pattern automatically during symbolic execution. More precisely, to recognize the master process, we check whether the process identifier of a received message of a wildcard receive ($\verb"Recv(*,r)"$) is used as the destination of a send operation, i.e., $\verb"Send(r.src)"$. We call such a wildcard receive schedule receive. Then, we locate the corresponding slave processes w.r.t. the matchings of the schedule receive, i.e., a process is a slave if its message can match the schedule receive.

Modeling the master process. We allocate a global variable $label$ for each schedule receive to decide the destination process of the next job. In addition to the operations for modeling normal wildcard receive operations, i.e., using external choice of the matched channel readings, we write the read value from the matched channel to $label$. For example, suppose $Chan_{1}$ and $Chan_{2}$ are the matched channels of a schedule receive, we model it by $Chan_{1}?label\rightarrow\verb"Skip"\square Chan_{2}?label\rightarrow\verb"Skip"$. Considering that a send operation in slave processes is modeled by writing the slave’s process identifier to the channel, we can use the value of $label$ to decide the destination of the next job.

Modeling the slave process. We use recursive CSP process to model a slave’s dynamic feature, i.e., repeatedly receiving a job and sending the result back until receiving the termination message. To model the job receive operation in a slave process, we use a guard expression $[label==i]$ before the channel reading of the receive operation, where $label$ is the global variable of the corresponding schedule receive and $i$ is the slave process’s identifier. Notably, the guard expression will disable the channel reading until the inside condition becomes true, indicating that the slave process cannot receive a new job unless its result has just been received by the master.

We need to refine the algorithms of symbolic execution and CSP modeling to support master-slave pattern. We have already implemented the refinement in MPI-SV. The support of master-slave pattern demonstrates that MPI-SV outperforms the single path reasoning work (Forejt et al., 2014; Huang and Mercer, 2015).

A.4. Proof of CSP Modeling’s Soundness and Completeness

Theorem 4.1 $\mathcal{F}(\emph{{CSP}}_{static})=\mathcal{F}(\emph{{CSP}}_{ideal})$.

Proof.

We first prove $\mathcal{T}(\textsf{CSP}_{static})=\mathcal{T}(\textsf{CSP}_{ideal})$, based on which we can prove $\mathcal{F}(\emph{{CSP}}_{static})=\mathcal{F}(\emph{{CSP}}_{ideal})$.

First, we prove $\mathcal{T}(\textsf{CSP}_{static}){\subseteq}\mathcal{T}(\textsf{CSP}_{ideal})$ by contradiction. Suppose there exists a trace $t{=}\langle e_{1},...,e_{n}\rangle$ such that $t{\in}\mathcal{T}(\textsf{CSP}_{static})$ but $t{\notin}\mathcal{T}(\textsf{CSP}_{ideal})$. The only difference between $\textsf{CSP}_{static}$ and $\textsf{CSP}_{ideal}$ is that $\textsf{CSP}_{static}$ introduces more channel read operations during the modeling of receive operations. Hence, there must exist a read operation of an extra channel in $t$. Suppose the first extra read is $e_{k}{=}c_{e}?x$, where $1{\leq}k{\leq}n$. Therefore, $c_{e}$ cannot be read in $\textsf{CSP}_{ideal}$ when the matching of the corresponding receive operation starts, but $c_{e}$ is not empty at $e_{k}$ in $\textsf{CSP}_{static}$. Despite of the size of $c_{e}$, there must exist a write operation $c_{e}!y$ in $\langle e_{1},...,e_{k-1}\rangle$. Because $\langle e_{1},...,e_{k-1}\rangle$ is also a valid trace in $\textsf{CSP}_{ideal}$, it means $c_{e}$ is not empty in $\textsf{CSP}_{ideal}$ at $e_{k}$, which contradicts with the assumption that $c_{e}$ cannot be read in $\textsf{CSP}_{ideal}$. Hence, $\mathcal{T}(\textsf{CSP}_{static})\subseteq\mathcal{T}(\textsf{CSP}_{ideal})$ holds.

Then, we prove $\mathcal{T}(\textsf{CSP}_{ideal}){\subseteq}\mathcal{T}(\textsf{CSP}_{static})$ also by contradiction. Suppose there exists a trace $t{=}\langle e_{1},...,e_{m}\rangle$ that $t{\in}\mathcal{T}(\textsf{CSP}_{ideal})$ but $t{\notin}\mathcal{T}(\textsf{CSP}_{static})$. Because $\textsf{SMO}(op_{j},S)$ is a superset of the precise matching set of $op_{j}$, $t$ cannot be a terminated trace. So, $\textsf{CSP}_{ideal}$ blocks at $e_{m}$. Because $t\notin\mathcal{T}(\textsf{CSP}_{static})$, there must exist a channel read operation $c_{m}?x$ that is enabled at $e_{m}$ in $\textsf{CSP}_{static}$, i.e., $c_{m}$ is not empty. Hence, there must exist a write operation $c_{m}!y$ in $\langle e_{1},...,e_{m-1}\rangle$. Because $\langle e_{1},...,e_{m-1}\rangle$ is valid in both of $\textsf{CSP}_{static}$ and $\textsf{CSP}_{ideal}$, $c_{m}?x$ is also enabled at $e_{m}$ in $\textsf{CSP}_{ideal}$, which contradicts with the assumption that $\textsf{CSP}_{ideal}$ blocks. Hence, we can have $\mathcal{T}(\textsf{CSP}_{ideal}){\subseteq}\mathcal{T}(\textsf{CSP}_{static})$, and $\mathcal{T}(\mathsf{CSP}_{static}){=}\mathcal{T}(\mathsf{CSP}_{ideal})$ holds.

Next, we can prove $\mathcal{F}(\emph{{CSP}}_{static})=\mathcal{F}(\emph{{CSP}}_{ideal})$ in a similar way. Suppose there exists $(s,X)$ in $\textsf{CSP}_{static}$ but $(s,X)\notin\textsf{CSP}_{ideal}$. It means there exists an event e in $X$ that is refused by $\textsf{CSP}_{static}$ at $s$, but enabled by $\textsf{CSP}_{ideal}$ at $s$. Because there is no internal choice in the CSP models, we have $s{\cdot}\langle e\rangle{\notin}\mathcal{T}(\textsf{CSP}_{static})$ (Roscoe, 2005) and $s{\cdot}\langle e\rangle{\in}\mathcal{T}(\textsf{CSP}_{ideal})$, which conflicts with $\mathcal{T}(\mathsf{CSP}_{static}){=}\mathcal{T}(\mathsf{CSP}_{ideal})$. The contradiction of the case in which $(s,X){\notin}\textsf{CSP}_{static}$ but $(s,X){\in}$

$\textsf{CSP}_{ideal}$ can be proved similarly.

Finally, $\mathcal{F}(\emph{{CSP}}_{static})=\mathcal{F}(\emph{{CSP}}_{ideal})$ is proved. ∎

Theorem 4.2 $\emph{{CSP}}_{static}$ is consistent with the MPI semantics.

Proof.

If the global state of generating CSPstatic is $S_{c}$, then we can get an MPI program $\mathcal{MP}_{p}$ from the sequence set $\mathsf{Seq}(S_{c})$, where each process $\mathsf{Proc}_{i}$ of $\mathcal{MP}_{p}$ is the sequential composition of the operations in $Seq_{i}$. Suppose the LTS model of $\mathcal{MP}_{p}$ is $M_{p}$, and the LTS after hiding all the $\mathit{issue}({o})$ actions in $M_{p}$ is $\hat{M_{p}}$. Then, $\mathsf{CSP}_{static}$ is consistent with the MPI semantics iff $\{(\mathsf{M}_{t}(s),\mathsf{M}_{s}(X))\mid(s,X)\in$

$\mathcal{F}(\textsf{CSP}_{static})\}$ is equal to $\{(T,X){\mid}T{\in}\hat{M_{p}}{\wedge}X{\subseteq}\mathsf{M}_{s}(\Sigma){\setminus}\mathit{enabled}({\mathsf{r}(T)})\}$, where $\Sigma$ is the event set of $\textsf{CSP}_{static}$, $\mathsf{M}_{t}(s)$ and $\mathsf{M}_{s}(X)$ maps the events in the sequence $t$ and the set $X$ to the corresponding actions in MPI semantics, respectively. This can be shown by proving that Algorithms 4 with a precise $\mathsf{SMO}$ ensures all the completes-before relations of MPI semantics (cf. semantic rules in Figure 8). The relations between send operations and those between receive operations (including conditional completes-before relation) are ensured by $\textsf{Refine}(P,S)$. The communications of $send$ and $recv$ operations are modeled by CSP channel operations and process compositions. The requirements of Wait and Barrier operations are modeled by the process compositions defined in Algorithm 4. Hence, we can conclude that $\textsf{CSP}_{ideal}$ is consistent with the MPI semantics. Then, by Theorem 4.1, we can prove $\textsf{CSP}_{static}$ is consistent with the MPI semantics. ∎