An Approach to Verification of MPI Applications Defined in a High-Level Model
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F17%3A10237738" target="_blank" >RIV/61989100:27240/17:10237738 - isvavai.cz</a>
Alternative codes found
RIV/61989100:27740/17:10237738
Result on the web
<a href="http://ieeexplore.ieee.org/document/7842501/" target="_blank" >http://ieeexplore.ieee.org/document/7842501/</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/ACSD.2016.17" target="_blank" >10.1109/ACSD.2016.17</a>
Alternative languages
Result language
angličtina
Original language name
An Approach to Verification of MPI Applications Defined in a High-Level Model
Original language description
Kaira is a prototyping tool for developing MPI programs (Bohm et al., Petri Nets 2014). The user of Kaira suggests a parallelization of a given sequential C++ code by creating a visual Petri-net based model, the tool then automatically generates the corresponding stand-alone MPI application. One of the tool modules enables to verify that the suggested parallelization has not introduced unexpected behaviors caused by unintended orders of communications among processes. The verification uses a state-space exploration procedure. Here we report on a new substantial enhancement of this procedure, leading to a significant reduction of the explored state space. The enhancement is based on the well-known methods of stubborn sets and ample sets, and is tailored to the use in the above mentioned visual model. Our concrete method is particularly simple but the experiments show that it works very well for practical examples from the area of scientific computing in distributed environment. The experiments also confirm that the Kaira model together with this method outperforms other tools for verifying MPI programs (w.r.t. instance-size/time).
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2017
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
International Conference on Application of Concurrency to System Design
ISBN
978-1-5090-2589-3
ISSN
1550-4808
e-ISSN
neuvedeno
Number of pages
10
Pages from-to
55-64
Publisher name
IEEE
Place of publication
New York
Event location
Torun
Event date
Jun 19, 2016
Type of event by nationality
EUR - Evropská akce
UT code for WoS article
000399126100007