Název projektu
Rozšiřování nástroje Kaira
Kód
SP2015/123
Řešitel
Období řešení projektu
01. 01. 2015 - 31. 12. 2015
Předmět výzkumu
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í, profilování, predikci výkonu či verifikace. 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ů.
Členové řešitelského týmu
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.
Ing. Martin Beseda, Ph.D.
Ing. Jakub Beránek
Ing. Jan Homola
Bc. Pavel Siemko
Bc. David Macek
Bc. Jan Černoch
Specifikace výstupů projektu (cíl projektu)
V nástroji Kaira byla realizovaná celá řada funkcí. Jednou z nich je verifikace. První celistvý úkol, který bychom rádi realizovali, je zlepšení výkonu verifikace a využití distribuovaného zpracování při jejím počítání. Verifikace v Kaiře je postavená na "state-space" analýze a aktuálně ji je možné provádět jen s využitím jednoho procesoru a sdílené paměti. Při verifikaci se generuje celý stavový prostor. Ten je i pro malé vstupy a malý počet procesorů obrovsky. V rámci minulého projektu byla implementována technika "Partial Order Reduction", která značně redukuje tento stavový prostor a umožňuje tak verifikovat mnohem větší vstupy. Další redukce tohoto stavového prostoru bez ztráty informace už v principu není možná a tak se nám jako jediná cesta jeví využít při vlastní verifikaci distribuované počítání a provádět samotnou verifikaci na superpočítači.
Další ucelenější oblastí, které by jsem se chtěli věnovat je testování výkonnosti nástroje Kaira. S tím souvisí tvorba netriviálních aplikací v nástroji Kaira. V posledních letech byla do Kairy přidána celá řada nových funkcí (více v předcházejících odstavcích). Jejich možnosti byly ověřeny na omezeném množství ukázkových aplikací. Cílem projektu bude aplikovat Kairu na řešení netriviálních problémů z různých oblastí a zhodnocení, které z implementovaných funkcí jsou postačující a které by mohly být vylepšeny. Také může být zajímavé porovnat Kairu s jinými nástroji usnadňujícími tvorbu MPI / C++ aplikací. Jako vhodné se aktuálně jeví využít Kairu k implementaci různých meta-heuristiky nebo řešení vybraných matematických algoritmů.
Kromě těchto hlavních oblastí, stále v nástroji Kaira zbývá vyřešit řadů úkolů, které pro fungování nástroje nejsou podstatné, ale usnadňují jeho použití. To může být například syntax-highliting, automatické doplňování kódu, generování testů, nebo inteligentnější editor tracelogů. Zde bychom zejména chtěli zapojit studenty magisterského programu.
Hlavním výstupem projektu bude praktická implementace zmíněných funkcí v nástroji Kaira. Očekáváme, že dosažené výzkumné výsledky (například distribuované verifikace nepodporuje skoro žádný nástroj) budou prezentovány na vědeckých konferencích případně v časopise.