An Approach to Verification of MPI Applications Defined in a High-Level Model

Kód výsledku v 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>

Nalezeny alternativní kódy

RIV/61989100:27740/17:10237738

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

An Approach to Verification of MPI Applications Defined in a High-Level Model

Popis výsledku v původním jazyce

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).

Název v anglickém jazyce

An Approach to Verification of MPI Applications Defined in a High-Level Model

Popis výsledku anglicky

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).

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

International Conference on Application of Concurrency to System Design

ISBN

978-1-5090-2589-3

ISSN

1550-4808

e-ISSN

neuvedeno

Počet stran výsledku

10

Strana od-do

55-64

Název nakladatele

IEEE

Místo vydání

New York

Místo konání akce

Torun

Datum konání akce

19. 6. 2016

Typ akce podle státní příslušnosti

EUR - Evropská akce

Kód UT WoS článku

000399126100007