Schválené projekty 2017

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 2017

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

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

fakulta přidělená částka v Kč
FBI  1 210 137
EKF  3 929 534
FAST  2 465 732
FS  9 344 630
FEI 13 996 004
HGF  5 272 251
FMMI  7 123 785
VC  8 743 333
CP  1 123 505
CELKEM 53 208 911

KódSP2017/82
Název projektuRozšiřování programovacích nástrojů 2
ŘešitelBěhálek Marek Ing., Ph.D.
Školitel projektu
Období řešení projektu01.01.2017 - 31.12.2017
Předmět výzkumuV rámci skupiny Teoretická informatika probíhá vývoj nástrojů pro podporu programování. Tyto nástroje se v principu snaží aplikovat teoretické poznatky při tvorbě softwaru a usnadnit tak práci programátorům. Specificky jde o nástroje Kaira a HAYDI. Oba tyto nástroje vznikly jako vedlejší produkt při řešení jiných výzkumných cílů (HAYDI - GAČR GA15-13784S, Výpočetní složitost vybraných verifikačních problémů, Kaira - GAČR GAP202/11/0340, Modelování a verifikace paralelních systémů). Cílem projektu je podpořit zapojení studentů při vývoji těchto nástrojů.

Kaira je nástroje určený pro zjednodušení vývoje distribuovaných MPI aplikací. Složitost tvorby těchto aplikací nespočívá jen v programování samotném, ale i ve složitosti různých podpůrných aktivit jako ladění nebo profilování. Problémem je také propojení výstupu z těchto nástrojů. Základním prvkem nástroje Kaira, který propojuje další části, je vizuální model postavený na Petriho sítích. 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. Aktuálně Kaira podporuje různé simulace, ladění, profilování, predikci výkonu či verifikace.

V projektu bychom se chtěli věnovat rozšiřování nástroje Kaira a to zejména v těchto oblastech:

- verifikace - aktuálně jsou implementovány funkce umožnující verifikaci distribuovaných aplikací, ale tyto verifikace jsou prováděny jen na jednom PC. Byly realizovány pokročile techniky redukce stavového prostoru postavené na metodě - Partial Order Reduction. Tato technika dokáže výrazně snížit velikost stavového prostoru, ale stále je velikost stavového prostoru limitem, při používání. Dá se očekávat, že uživatelé nástroje Kaira mají přístup k superpočítačům. Proto jsem se aktuálně zaměřili na provádění vlastní verifikace distribuovaně. Toto je velmi složitý úkol. Primární problém je jak rozdělit co nejrovnoměrněji procházeny stavový prostor a s tím související výměna informací (zejména stavů).

- profilování - výsledkem profilování distribuovaných aplikací je množina tracelogů. Tracelog je v podstatě sekvence událostí (opatřených časovými razítky) zachycující běh aplikace. Z různých důvodů mohou být tyto záznamy nekonzistentní (synchronizace hodin mezi uzly, měření času...). V rámci minulého projektu vznikla komponenta v Kaiře, která umožňuje následnou synchronizaci těchto tracelogů. Synchronizace je aktuálně řešena po skončení běhu aplikace na jednom počítači. To může být nevhodné řešení. Tracelogy mohou být i pro krátký běh obrovské a jejich zpracování časově velmi náročné. Podobně jako u verifikací, i zde pracujeme na distribuované verzi této komponenty. Komponenta by opravu udělala na stejném počtu uzlů, na jakém byla spuštěna bezprostředně po skončení běhu aplikace. Dalším možným rozšířením jsou různé analýzy těchto tracelogů (například postavené na kritické cestě).

- zlepšování uživatelského komfortu.


HAYDI (dříve QIT - Quick Idea Tester) je nástroj pro snadné vytváření programů pro ověřování různých hypotéz, hledání protipříkladů apod. při řešení různých problémů z teoretické informatiky. Primární motivací je výzkum v oblasti algoritmů pro rozhodování ekvivalence deterministických zásobníkových automatů, nástroj HAYDI je ale navrhován obecně tak, aby ho bylo možné použít pro nejrůznější druhy problémů. Jako konkrétní příklady typů takových problémů je možné uvést třeba problémy týkající se různých jiných druhů automatů či podobných souvisejících formalizmů jako jsou různé druhy gramatik a různé varianty Petriho sítí, nebo různé kombinatorické problémy (např. Rubikova kostka), problémy týkající se různých logických dedukčních systémů apod. Základní myšlenkou nástroje HAYDI je to, že umožňuje deklarativně popsat základní datové struktury, relace a funkce týkající se daného problému, a poté z tohoto deklarativního popisu vygenerovat kód pro systematické zkoušení všech možností, náhodné vybíraní testovaných možností podle zadaného pravděpodobnostního rozdělení apod. V současné době se deklarativní popis zadává pomocí kódu v Pythonu, který vytváří příslušnou datovou strukturu s tímto deklarativním popisem. Aktuálně lze nástroj spouštět na paralelním superpočítači. Nástroj při generování všech možností používá líný (lazy) přístup, takže je možné deklarativně popisovat i nekonečné nebo velmi velké datové struktury, které jsou ve výsledném kódu generovány postupně. Umožňuje rovněž popisovat data jako pevné body určitých zobrazení, takže je možné snadno popsat například stavový prostor všech dosažitelných konfigurací daného automatu, všech formulí dokazatelných z daných axiomů v daném odvozovacím systému apod.

Aktuálně je připravovaná první nasaditelná verze aplikace. V této fázi se předpokládá nasazení studentů zejména k realizaci těchto úkolů:

- tvorba dokumentace a webové prezentace
- tvorba ukázkových příkladů
- nasazení nástroje k řešení známých problému - příkladem může být ekvivalence zásobníkových automatů nebo synchronizační automaty.
- testování na superpočítači Salamon (byl podán projekt v rámci organizace IT4I na využití výpočetního času).
- další rozvoj aplikace - kromě testování a přípravy na zveřejnění první verze dále pokračuje vývoj vlastní aplikace. Zde se chceme zaměřit především ¨na lepší generování instancí, abychom mohli snadno vyloužit například symetrické příklady (například dva automaty, kde dojde jen k přehození čísel stavů).
Členové řešitelského týmuIng. Marek Běhálek, Ph.D.
Ing. Jakub Beránek
Ing. Stanislav Böhm, Ph.D.
Ing. Jan Homola
prof. RNDr. Petr Jančar, CSc.
Ing. Martin Kot, Ph.D.
Ing. Tomáš Panoc
Radim Polach
doc. Ing. Zdeněk Sawa, Ph.D.
Ing. Martin Šurkovský
Bc. Petra Tesařová
Specifikace výstupů projektu (cíl projektu)Hlavním výstupem budou implementovaná rozšíření nástrojů Kaira a HAYDI.

V nástroji Kaira se chceme zaměřit zejména na tyto oblasti:
- pokročilé funkce pro profilování
- distribuované verifikace
- zlepšování uživatelského komfortu.

V nástroji HAYDI by šlo zejména o tyto oblasti:

- tvorba dokumentace a webové prezentace
- tvorba ukázkových příkladů
- nasazení nástroje k řešení známých problému
- další rozvoj aplikace

Předpokládá se, že dosažené výsledky budou publikovány odborné veřejnosti. Předpokládá se, že bude zaslán příspěvek na konferenci zabývající se:
a) pro nástroj Kaira
- verifikace v oblasti MPI, například konference ACSD
- syntézou Petriho sítí, například konference Petri Nets (http://pn2017.unizar.es/)
b) nástroj Haydi
- předpokládá se prezentace nástroje na konferenci se zaměřením na oblast teoretické informatiky, kde existuje sekce pro prezentaci nástrojů (například CAV http://cavconference.org/2017/)

Rozpočet projektu - uznané náklady

NávrhSkutečnost
1. Osobní náklady
Z toho
40200,-40543,-
1.1. Mzdy (včetně pohyblivých složek)30000,-30256,-
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ěstnanosti10200,-10287,-
2. Stipendia130000,-130000,-
3. Materiálové náklady0,-0,-
4. Drobný hmotný a nehmotný majetek11300,-40957,-
5. Služby0,-0,-
6. Cestovní náhrady30000,-0,-
7. Doplňkové (režijní) náklady max. do výše 10% poskytnuté podpory23500,-23500,-
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áklady235000,-
Uznané náklady235000,-
Celkem běžné finanční prostředky235000,-235000,-