Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1297486, author = {Forejt, Vojtěch and Kroening, Daniel and Narayanaswamy, Ganesh and Sharma, Subodh}, address = {Switzerland}, booktitle = {FM 2014: Formal Methods}, doi = {http://dx.doi.org/10.1007/978-3-319-06410-9_19}, editor = {Cliff Jones, Pekka Pihlajasaari, Jun Sun}, keywords = {MPI; verification; parallel computation}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Switzerland}, isbn = {978-3-319-06409-3}, pages = {263-278}, publisher = {Springer}, title = {Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs}, year = {2014} }
TY - JOUR ID - 1297486 AU - Forejt, Vojtěch - Kroening, Daniel - Narayanaswamy, Ganesh - Sharma, Subodh PY - 2014 TI - Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs PB - Springer CY - Switzerland SN - 9783319064093 KW - MPI KW - verification KW - parallel computation N2 - The Message Passing Interface (MPI) is the standard API for high-performance and scientific computing. Communication deadlocks are a frequent problem in MPI programs, and this paper addresses the problem of discovering such deadlocks. We begin by showing that if an MPI program is single-path, the problem of discovering communication deadlocks is NP-complete. We then present a novel propositional encoding scheme which captures the existence of communication deadlocks. The encoding is based on modelling executions with partial orders, and implemented in a tool called MOPPER. The tool executes an MPI program, collects the trace, builds a formula from the trace using the propositional encoding scheme, and checks its satisfiability. Finally, we present experimental results that quantify the benefit of the approach in comparison to a dynamic analyser and demonstrate that it offers a scalable solution. ER -
FOREJT, Vojtěch, Daniel KROENING, Ganesh NARAYANASWAMY a Subodh SHARMA. Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. In Cliff Jones, Pekka Pihlajasaari, Jun Sun. \textit{FM 2014: Formal Methods}. Switzerland: Springer, 2014, s.~263-278. ISBN~978-3-319-06409-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-06410-9\_{}19.
|