Diplomová práce

Verifikace MPI programů pomocí DIVINE

Verification of MPI programs with DIVINE

Bc. Marek Tomáštík, učo 374575
Anotace

Práce popisuje implementaci standardu MPI pro model checker DIVINE. Vytvořená knihovna umožňuje DIVINE verifikovat programy v jazycích C a C++, které používají rozhraní MPI pro komunikaci pomocí předávání zpráv v distribuovaném prostředí. Ačkoliv tato knihovna nepokrývá celou MPI specifikaci, implementované části standardu by měly být dostatečné pro verifikaci většiny MPI programů. Kromě samotné implementace …více

Abstract

This work presents an implementation of the MPI specification for the model checker DIVINE. The created library allows DIVINE to verify C and C++ programs that use the MPI standard to communicate by message-passing in a distributed-memory environment. The library does not cover the entire MPI specification, but the implemented parts of the standard should be sufficient to verify most MPI programs. …více

Klíčová slova
formal verification model checking DIVINE C C++ MPI
Zadání práce
Cílem práce je navrhnout a implementovat modul verifikačního nástroje DIVINE, který umožní verifikovat programy využívající standard MPI pro distribuované počítání. Klíčové části MPI, které budou pokryty, zahrnují point-to-point komunikaci, kolektivní komunikační primitiva, intra-komunikátory a MPI datové typy. Součástí práce je i příprava několika ukázkových MPI programů, na kterých bude funkčnost modulu demonstrována.
Administrativní informace
Práce zkontrolována:
13. 1. 2016 08:02, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
416,6 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
16. 2. 2016
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

RNDr. Petr Ročkai, Ph.D., učo 139761
KTP FI MU

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
  • GRAMA, Ananth. Introduction to parallel computing. 2nd ed. Harlow: Addison-Wesley, 2003, xx, 636. ISBN 0201648652.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.