-
Notifications
You must be signed in to change notification settings - Fork 0
/
conclusion.tex
4 lines (3 loc) · 1.42 KB
/
conclusion.tex
1
2
3
4
\section{Conclusions and Future Work}
This paper presents a new algorithm that correctly encodes MPI point-to-point communication and MPI collective communication. The encoding supports both infinite buffer semantics and zero buffer semantics. To constrain the behavior of message communication, the encoding directly uses match pairs over sends and receives. The program order over events is also constrained according to the MPI semantics. In particular, the zero buffer encoding is further capable of detecting whether an MPI program is compatible with zero buffer semantics. Experiments demonstrate that the new encoding is correct. Also, salability tests show that the new zero buffer encoding is much faster than the new infinite buffer encoding. The results in the scalability test can be further used as boundary on expected cost for analysis. Finally, benchmark program tests demonstrate that the new encoding is able to efficiently detect violations and is useful for checking zero buffer compatibility.
The encoding is dependent on an input execution trace of the program. Future work will explore using bounded model checking to encode an MPI program instead of an execution trace. This technique statically unrolls an MPI program and then verifies it by constraining the semantics into an SMT encoding. Finally, since the encoding in this paper does not constrain the computation in a program, future work will explore encoding it correctly.