Schválené projekty 2016

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 2016

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

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

fakulta přidělená částka v Kč
FBI  1 270 231
EKF  4 459 400
FAST  2 765 016
FS  9 344 371
FEI 13 781 413
HGF  5 130 549
FMMI  7 000 000
VC 10 748 511
CELKEM 54 499 491

KódSP2016/118
Název projektuRozšiřování programovacích nástrojů
ŘešitelBěhálek Marek Ing., Ph.D.
Školitel projektu
Období řešení projektu01.01.2016 - 31.12.2016
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 QIT. Oba tyto nástroje vznikly jako vedlejší produkt při řešení jiných výzkumných cílů (QIT - 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ů). Ovšem by mohly tyto nástroje být prakticky používány, vyžadují další rozšiřování, zejména v oblasti funkcí, které zlepšují uživatelský dojem. Takto byla v minulosti v rámci projektů SGS například do nástroje Kaira implementována možnost provádět různé predikce výkonu, nebo přidáno zvýrazňování syntaxe a doplňování kódu.

Kaira nástroje je 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. 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.


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 QIT 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 QIT 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 v C++ 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. Ty relace nebo funkce, pro které by bylo obtížné nebo zbytečně komplikované je popisovat deklarativně, může uživatel doplnit přímo jako kód v C++. 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. Vygenerovaný C++ kód pracuje v současné době pouze sekvenčně, ale do budoucna se počítá s tím, že nástroj QIT umožní generovat paralelní kód, který
bude možno 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.
Členové řešitelského týmuIng. Marek Běhálek, Ph.D.
Ing. Jakub Beránek
Ing. Stanislav Böhm, Ph.D.
Bc. Jan Černoch
Ing. Jan Homola
prof. RNDr. Petr Jančar, CSc.
Ing. Martin Kot, Ph.D.
Ing. Ondřej Meca
Ing. Tomáš Panoc
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 QIT.

V nástroji Kaira se chceme zaměřit zejména na tyto oblasti:
- automatické formátování vizuálního modelu - aktuálně nástroj podporuje jen jednoduché přichytávání k definované mřížce. Chtěli bychom dodat funkci, která by uměla vizuální program automaticky naformátovat (upravit pozice a velikost vizuálních komponent).
- pokročilé funkce pro profilování - nástroje jako Scalasca obsahují řadu funkcí pro zpracování a analýzu tracelogů. Některé tyto funkce bychom chtěli začlenit do nástroje Kaira. Zejména bychom se chtěli zaměřit na analýzy postavené na kritické cestě a synchronizaci údajů v naměřených při profilování.

V nástroji QIT by šlo zejména o rozšíření nástroje:
- z hlediska podporovaných datových typů;
- snadnosti zadávání matematického (deklarativního) modelu;
- generování paralelního kódu v C++.

Předpokládá se, že dosažené výsledky budou publikovány odborné veřejnosti.

Rozpočet projektu - uznané náklady

NávrhSkutečnost
1. Osobní náklady
Z toho
40200,-40200,-
1.1. Mzdy (včetně pohyblivých složek)30000,-30000,-
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,-10200,-
2. Stipendia125000,-144000,-
3. Materiálové náklady0,-0,-
4. Drobný hmotný a nehmotný majetek11800,-22800,-
5. Služby0,-0,-
6. Cestovní náhrady30000,-0,-
7. Doplňkové (režijní) náklady max. do výše 10% poskytnuté podpory23000,-23000,-
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áklady230000,-
Uznané náklady230000,-
Celkem běžné finanční prostředky230000,-230000,-