Formal verification of programs that use MPI one-sided communication

Salman Pervez; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur; William Gropp

doi:10.1007/11846802_13

Formal verification of programs that use MPI one-sided communication

Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We used formal-verification methods based on model checking to analyze the correctness properties of one existing and two new distributed-locking algorithms implemented by using MPI's one-sided communication. Model checking exposed an overlooked correctness issue with the first algorithm, which had been developed by relying only on manual reasoning. Model checking helped confirm the basic correctness properties of the two new algorithms, while also identifying the remaining problems in them. Our experience is that MPI-based programming, especially the tricky and relatively poorly understood one-sided communication features, stand to gain immensely from model checking. Considering that many other areas of concurrent hardware and software design now routinely employ model checking, our experience confirms that the MPI community can benefit greatly from the use of formal verification.

Original language	English (US)
Title of host publication	Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings
Publisher	Springer
Pages	30-39
Number of pages	10
ISBN (Print)	354039110X, 9783540391104
DOIs	https://doi.org/10.1007/11846802_13
State	Published - 2006
Externally published	Yes
Event	13th European PVM/MPI User's Group Meeting - Bonn, Germany Duration: Sep 17 2006 → Sep 20 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4192 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	13th European PVM/MPI User's Group Meeting
Country/Territory	Germany
City	Bonn
Period	9/17/06 → 9/20/06

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/11846802_13

Library availability

Discover UIUC Full Text

Cite this

Pervez, S., Gopalakrishnan, G., Kirby, R. M., Thakur, R., & Gropp, W. (2006). Formal verification of programs that use MPI one-sided communication. In Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings (pp. 30-39). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4192 LNCS). Springer. https://doi.org/10.1007/11846802_13

Formal verification of programs that use MPI one-sided communication. / Pervez, Salman; Gopalakrishnan, Ganesh; Kirby, Robert M. et al.
Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings. Springer, 2006. p. 30-39 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4192 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Pervez, S, Gopalakrishnan, G, Kirby, RM, Thakur, R & Gropp, W 2006, Formal verification of programs that use MPI one-sided communication. in Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4192 LNCS, Springer, pp. 30-39, 13th European PVM/MPI User's Group Meeting, Bonn, Germany, 9/17/06. https://doi.org/10.1007/11846802_13

Pervez S, Gopalakrishnan G, Kirby RM, Thakur R, Gropp W. Formal verification of programs that use MPI one-sided communication. In Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings. Springer. 2006. p. 30-39. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11846802_13

Pervez, Salman ; Gopalakrishnan, Ganesh ; Kirby, Robert M. et al. / Formal verification of programs that use MPI one-sided communication. Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings. Springer, 2006. pp. 30-39 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{04dcddbe84f340d89218c113b3005e95,

title = "Formal verification of programs that use MPI one-sided communication",

abstract = "We used formal-verification methods based on model checking to analyze the correctness properties of one existing and two new distributed-locking algorithms implemented by using MPI's one-sided communication. Model checking exposed an overlooked correctness issue with the first algorithm, which had been developed by relying only on manual reasoning. Model checking helped confirm the basic correctness properties of the two new algorithms, while also identifying the remaining problems in them. Our experience is that MPI-based programming, especially the tricky and relatively poorly understood one-sided communication features, stand to gain immensely from model checking. Considering that many other areas of concurrent hardware and software design now routinely employ model checking, our experience confirms that the MPI community can benefit greatly from the use of formal verification.",

author = "Salman Pervez and Ganesh Gopalakrishnan and Kirby, {Robert M.} and Rajeev Thakur and William Gropp",

year = "2006",

doi = "10.1007/11846802_13",

language = "English (US)",

isbn = "354039110X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "30--39",

booktitle = "Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings",

address = "Germany",

note = "13th European PVM/MPI User's Group Meeting ; Conference date: 17-09-2006 Through 20-09-2006",

}

TY - GEN

T1 - Formal verification of programs that use MPI one-sided communication

AU - Pervez, Salman

AU - Gopalakrishnan, Ganesh

AU - Kirby, Robert M.

AU - Thakur, Rajeev

AU - Gropp, William

PY - 2006

Y1 - 2006

N2 - We used formal-verification methods based on model checking to analyze the correctness properties of one existing and two new distributed-locking algorithms implemented by using MPI's one-sided communication. Model checking exposed an overlooked correctness issue with the first algorithm, which had been developed by relying only on manual reasoning. Model checking helped confirm the basic correctness properties of the two new algorithms, while also identifying the remaining problems in them. Our experience is that MPI-based programming, especially the tricky and relatively poorly understood one-sided communication features, stand to gain immensely from model checking. Considering that many other areas of concurrent hardware and software design now routinely employ model checking, our experience confirms that the MPI community can benefit greatly from the use of formal verification.

AB - We used formal-verification methods based on model checking to analyze the correctness properties of one existing and two new distributed-locking algorithms implemented by using MPI's one-sided communication. Model checking exposed an overlooked correctness issue with the first algorithm, which had been developed by relying only on manual reasoning. Model checking helped confirm the basic correctness properties of the two new algorithms, while also identifying the remaining problems in them. Our experience is that MPI-based programming, especially the tricky and relatively poorly understood one-sided communication features, stand to gain immensely from model checking. Considering that many other areas of concurrent hardware and software design now routinely employ model checking, our experience confirms that the MPI community can benefit greatly from the use of formal verification.

UR - http://www.scopus.com/inward/record.url?scp=33750230738&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33750230738&partnerID=8YFLogxK

U2 - 10.1007/11846802_13

DO - 10.1007/11846802_13

M3 - Conference contribution

AN - SCOPUS:33750230738

SN - 354039110X

SN - 9783540391104

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 30

EP - 39

BT - Recent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings

PB - Springer

T2 - 13th European PVM/MPI User's Group Meeting

Y2 - 17 September 2006 through 20 September 2006

ER -

Formal verification of programs that use MPI one-sided communication

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this