Schválené projekty 2015

Rozdělení přidělené dotace z MŠMT na specifický vysokoškolský výzkum po fakultách se zohledněním celoškolských pracovišť na rok 2015

Celková přidělená částka z MŠMT na specifický vysokoškolský výzkum na VŠB-TUO - 52 908 039 Kč

Z toho 2.5% - 1 320 739 Kč - úhrada způsobilých nákladů spojených s organizací SGS

fakultapřidělená částka v Kč
FBI  1 172 500
EKF  4 962 700
FAST  3 070 000
FS  8 256 000
FEI 12 282 100
HGF  5 433 000
FMMI  6 188 000
VC 10 223 000
CELKEM 51 587 300
KódSP2015/123
Název projektuRozšiřování nástroje Kaira
ŘešitelBěhálek Marek Ing., Ph.D.
Školitel projektu
Období řešení projektu01.01.2015 - 31.12.2015
Předmět výzkumuV 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ýmuIng. Marek Běhálek, Ph.D.
Ing. Jakub Beránek
Ing. Martin Beseda
Ing. Stanislav Böhm, Ph.D.
Bc. Jan Černoch
Ing. Jan Homola
prof. RNDr. Petr Jančar, CSc.
Ing. Martin Kot, Ph.D.
Bc. David Macek
Ing. Ondřej Meca
doc. Ing. Zdeněk Sawa, Ph.D.
Bc. Pavel Siemko
Ing. Martin Šurkovský
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.

Rozpočet projektu - uznané náklady

NávrhSkutečnost
1. Osobní náklady
Z toho
53600,-53600,-
1.1. Mzdy (včetně pohyblivých složek)40000,-40000,-
1.2. Odvody pojistného na veřejné zdravotně pojištění a pojistného na sociální zabezpečení a příspěvku na státní politiku zaměstnanosti13600,-13600,-
2. Stipendia120000,-145000,-
3. Materiálové náklady0,-0,-
4. Drobný hmotný a nehmotný majetek17400,-24526,-
5. Služby3000,-0,-
6. Cestovní náhrady40000,-10874,-
7. Doplňkové (režijní) náklady max. do výše 10% poskytnuté podpory26000,-26000,-
8. Konference pořádané VŠB-TUO k prezentaci výsledků studentského grantu (max. do výše 10% poskytnuté podpory)0,-0,-
9. Pořízení investic0,-0,-
Plánované náklady260000,-
Uznané náklady260000,-
Celkem běžné finanční prostředky260000,-260000,-