Studentská grantová soutěž - předchozí roky

Implementace predikce výkonu a verifikací do nástroje Kaira

SP2014/120

Běhálek Marek Ing., Ph.D.

01. 01. 2014 - 31. 12. 2014

V rámci minulých SGS projektů a dalších výzkumných aktivit vznikl nástroj Kaira (http://verif.cs.vsb.cz/kaira/). Tento nástroje je určený pro zjednodušení vývoje distribuovaných MPI aplikací. Tvorba paralelních aplikací je obecně považována za složitější než tvorba sekvenčních aplikací. Jejich složitost nespočívá jen v programování samotném, ale i ve složitosti různých podpůrných aktivit jako ladění, profilování a podobně. Problémem je také propojení výstupu z těchto nástrojů. Ke zmíněným problémům můžeme přidat také delší čas potřebný k získání první funkční verze nebo nárůst objemu dat při nárůstu počtu použitých procesů. Kaira se tyto problémy snaží řešit. Základním prvkem, který propojuje další části je vizuální model postavený na Petriho sítích a vizuální programování obecně. Autor tvoří aplikaci pomocí tohoto vizuálního modelu, a Kaira odvodí potřebné implementační detaily a jako výsledek vygeneruje samostatnou MPI/C++ aplikaci. To je v mnoha ohledech jednodušší a rychlejší. Díky tomu je Kaira vhodná jako prototypovací nástroj. Na druhou stranu Kaira není automaticky paralelizující nástroj, uživatel stále musí zachytit paralelní chování, také je toto vizuální programování použito striktně pro paralelní části. Sekvenční jsou tvořeny obvyklým způsobem v C++. Jak bylo zmíněno výše, Kaira a použitý model neslouží jen k vlastnímu vývoji, ale propojují různé podpůrné aktivity. Aktuálně Kaira podporuje různé simulace, ladění a profilování. Zde použitý vizuální model slouží jak k nastavení těchto aktivit tak k prezentaci výsledků. Působí také jako přirozený spojovací prvek a můžeme například snadno použít data z profilování pro simulaci. Toto považujeme za velkou výhodu, protože uživatel může nastavení provádět na stejných prvcích, které použil k vývoji a výsledky jsou prezentovány na modelu, který zná. Například nastavit rozumně profilovaní MPI aplikace může být značně obtížné, stejně jako vydolovat smysluplný závěr z naměřených výsledků.

Ing. Martin Kot, Ph.D.
doc. Ing. Zdeněk Sawa, Ph.D.
prof. RNDr. Petr Jančar, CSc.
Ing. Ada Böhm, Ph.D.
Ing. Marek Běhálek, Ph.D.
Ing. Martin Šurkovský, Ph.D.
Ing. Ondřej Meca, Ph.D.
Bc. Marek Večerka
Jiří Jančijuk
Bc. Jan Koběluš
Bc. Martin Kozubek
Bc. Martin Palásek

Hlavním cílem projektu bude další rozšiřování nástroje Kaira. Předmětem projektu budou dvě hlavní oblasti, kterýma se aktuálně zabýváme. To je predikce výkonu a verifikace.

Predikce výkonu je velice zajímavá z pohledu nástroje určeného pro prototypování paralelních aplikací. Velice často bychom potřebovali odhadnout chování aplikace bez nutnosti skutečného spuštění. Aktuálně již jakási základní predikce výkonu implementovaná je, běží ovšem pouze na jednom procesoru a možnosti jejího nastavení jsou omezené. Cílem bude vlastní implementace těchto rozšíření.

Dalším zajímavým aspektem, který bychom chtěli implementovat do nástroje Kaira, je formální verifikace. Použitý nástroj vychází z Petriho sítí a i když tento model přesně nekopíruje, stále zůstává formálně dobře zachytitelná a umožňuje použití různých technik z oblasti Petriho sítí (jako například: Pratial Order Reduction). Cílem projektu bude tedy implementace takovýchto užitečných technik a prozkoumání možností, které formální verifikace v Kaiře nabízí na poli distribuovaných aplikací.

Kromě vlastního rozšíření nástroje Kaira se předpokládá, že dosažené výsledky budou prezentovány odborné veřejnosti. Předpokládá se aktivní účast na nějaké mezinárodní konferenci, nebo v nějakém odborném časopise.