All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

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