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

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

SP2017/82

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

01. 01. 2017 - 31. 12. 2017

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 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ů).

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

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/)