V prosinci obhajují svou disertační práci David Kozák a František Vídeňský z Ústavu inteligentních systémů

Zveme vás na obhajobu disertační práce Ing. Davida Kozáka z Ústavu inteligentních systémů FIT VUT, která se bude konat ve středu 10. 12. 2025 od 10:30 v zasedací místnosti G108 na FIT VUT. Vedoucím disertační práce s titulem „Nové metody statické analýzy nejen pro ahead-of-time překladače objektově orientovaných jazyků“ je prof. Tomáš Vojnar.

Disertace Davida Kozáka se zabývá využitím metod statické analýzy v kontextu ahead-of-time kompilace objektově orientovaných jazyků, jako je např. Java. Kozák se soustředí na možnosti uplatnění těchto technik při automatizované analýze a současně na poli rekonstruování softwarové architektury v prostředí mikroslužeb. Davidova výzkumná práce má konkrétní aplikační rovinu. Nástroj, do něhož implementoval většinu svého výzkumu, se nazývá GraalVM Native Image. Ten realizuje ahead-of-time kompilaci a je dlouhodobě vyvíjen ve výzkumném institutu Oracle Labs. Kozák je zde součástí GraalVM týmu.

Hlavním cílem autorovy práce bylo zefektivnění řetězce procesů propojujících statickou analýzu typu points-to a následnou práci překladače typu ahead-of-time. Statickou analýzu si nejobecněji můžeme představit jako cokoliv, co analyzuje program, aniž by ho spustilo, a to s cílem zjistit vlastnosti programu či ověřit, zda funguje správně vůči stanovené definici správnosti. Od počátku je tato metoda úzce spjata právě s překladači. Statická analýza aplikovaná na prostředí překladačů musí být rychlá, efektivní a také výpočetně nenáročná. Specifickým cílem autorova výzkumu bylo zachovat spolehlivost a přesnost statické analýzy typu points-to, ale současně ji urychlit, tedy přiblížit se silné stránce jiného typu statické analýzy: rapid type. Navíc toho bylo třeba dosáhnout v prostředí ahead-of-time překladačů, v tomto případě pracujících s nízkoúrovňovou reprezentací programovacího jazyka Java jménem bytekód. Jak napovídá název, ahead-of-time překlad do strojového kódu probíhá před spuštěním programu coby samostatný proces, a to jen jednou a bez „luxusu“ možnosti dodatečně interpretovat kód, který nebyl přeložen, nebo případně některé metody znovu rekompilovat za běhu. Kompiluje se tedy vše, co by mohlo být spuštěno, což je z podstaty věci výpočetně náročné a výsledný binární soubor bývá velký. Zde tedy leží motiv snahy o zefektivnění a zrychlení statické analýzy při současném zachování její korektnosti.

Překladač Native Image, s nímž Kozák pracuje, používá typovou points-to analýzu pracující s typy (třídami) objektů. Kozák využil techniky saturace, kterou můžeme zjednodušeně vnímat jako kompromis mezi points-to analýzou a rapid-type analýzou – její hlavní ideu lze popsat následovně: Podíváme se, které konkrétní implementace daného typu byly vytvořeny (instanciovány), a použijeme jenom tyto. Části programu, které můžeme analyzovat přesně, pokryjeme metodami points-to analýzy. Naopak, pokud o některých částech programu máme k dispozici příliš obsáhlá data, použijeme pro ně rapid-type analýzu. Výsledkem je přesnost blízká výstupům points-to analýzy a rychlost velmi blízko té, kterou nabízí rapid type analýza.

Další součástí Kozákovy disertační práce a výzkumného úkolu byl návrh rozšíření points-to analýzy nástroje Native Image s označením SkipFlow. Toto rozšíření sleduje nově nejen objekty, ale také tok primitivních hodnot a současně používá predikátové hrany, aby zabránilo šíření hodnot z nedosažitelných větví (dead code) programu. SkipFlow snížilo zátěž pro překladač a nabídlo přesnější analýzu za cenu malého prodloužení běhu a se ziskem v podobě následné rychlejší práce samotného překladače.

Kozákův výzkum má i druhé, možná poněkud překvapivé a netypické pole aplikace statické analýzy – jde o sféru mikroslužeb, resp. pochopení dopadů jejich vzájemných závislostí. A toto je spíše doména softwarového inženýrství. Dnes jsou aplikace vyvíjeny formou řady menších mikroslužeb. Problém však spočívá v tom, že lze jen složitě sledovat komunikaci jednotlivých částí a dopady změn dílčích mikroslužeb na služby další. Kozák opět využil nástroj Native Image, tentokrát pro zisk informací o každé dílčí službě, a následně na základě toho vytvořil holistický pohled na celou aplikaci. Z přeložené verze aplikace lze tak rekonstruovat vysokoúrovňovou architekturu a její zcela aktuální vizualizaci, která může být předána softwarovému architektovi. Kozák se také podílel na vzniku nástroje SAVAT, který je schopen analyzovat dopad změn v rámci časové řady jednotlivých verzí mikroslužeb. Sečteno, podtrženo: Disertační práce Davida Kozáka je krokem ke sjednocení tří dosud převážně oddělených oblastí: kompilátorů, interprocedurální statické analýzy pokrývající celý program a softwarového inženýrství.

Při dotazu na pro něj klíčové výsledky výzkumné práce má David Kozák jasno: „Nejvíce jsem hrdý na SkipFlow, tedy rozšíření points-to analýzy, které trackuje primitivní hodnoty a sleduje závislosti mezi větvemi programů. Proč? Protože jsme zde dosáhli ideálního výsledku: Vytvořili jsme současně přesnější i rychlejší analýzu. Pak bych zmínil saturaci, protože tím, že jsme zkombinovali dva typy analýzy a že počítáme velmi přesně jen tam, kde to má smysl, jsme byli schopni dosáhnout téměř identických výsledků jako přesnější analýza, ale za výrazně kratší čas.“ Při bilancování však David zmíní i obecnější momenty: „Jsem spokojený s tím, že nejde o čistě základní výzkum, ale vše je integrováno do skutečného nástroje, do Native Image, a navíc saturace i SkipFlow jsou v tomto nástroji zapnuty automaticky. To znamená, že kdokoliv využívá Native Image, využívá i výsledky mé disertace. Rád svůj výzkum cílím na to, co je v praxi používáno. Mám rád kontakt s průmyslem a reálné nasazení technologie.“ Za konzultace a podporu v průběhu výzkumu by David rád poděkoval kolegům z výzkumné skupiny VeriFIT. A stran budoucích pracovních plánů konstatuje, že by chtěl být i nadále rozkročen mezi akademický výzkum a průmysl. Vysněným cílem je pak sestavit širší tým lidí, kteří by se podíleli na výzkumu v rámci GraalVM týmu, a to i z řad bakalářských či magisterských studentů se zájmem o překladače.

Doplňme, že ve stejném týdnu je na naší fakultě v plánu ještě jedna veřejná obhajoba disertační práce. Autorem disertace „Pozdní vazba proměnných v interpretech jazyka AgentSpeak(L)“ je Ing. František Vídeňský z Ústavu inteligentních systémů, jeho školitelem pak doc. František Zbořil. Veřejná obhajoba této disertace se koná v pátek 12. 12. 2025 od 13:00 v místnosti G108.

Přejeme oběma výzkumníkům, aby jim i nadále jejich obor přinášel úspěchy a radost.