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

Rozšiřování programovacích nástrojů

SP2016/118

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

01. 01. 2016 - 31. 12. 2016

V 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.

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. Jakub Beránek
Ing. Tomáš Panoc
Ing. Jan Homola
Bc. Jan Černoch
Bc. Petra Tesařová

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.