Future Work

Možná budoucí práce (v náhodném pořadí):

• Propojení s dynamickou analýzou ve frameworku ANaConDA. Atomer najde kontrakty, které porušují atomicitu. ANaConDA potom zaměří svoji analýzu pouze na tyto nalezené kontrakty. Otázka je, jak přesně předávat informace z Atomeru do ANaConDA. Při hledání programů pro experimenty se soustředit na C programy, které mají ideálně nějaký test suite, aby na tom ANaConDA šla spustit.

• Uvažovat o implemantaci čtení a zápisů do proměnných v Atomeru. Tzn. neuvažovat pouze volání funkcí. Takhle by se potom daly hledat i data races.

• Vyřešit nějak případy, kdy ve wrapperech nad zámky se zamykání/odemykání objevuje pod nějakou (tou stejnou) podmínkou. Tohle v analýze povede např. k tomu, že se uvažuje i případ, že odemykací wrapper zamkne, ale zamykací wrapper neodemkne. To by se reálně nemělo stát, když je ta podmínka pro zamčení/odemčení stejná. Vyřešit to možná tak, že si při zamykání/odemykání pamatovat (tu nejvíce) zanořenou podmínku a přidávat si ji k informaím o zámcích?

• Udělat nějaké rozsáhlé experimenty s reálnými programy a zkusit najít reálné chyby. Vyladit analýzu tak, aby se našlo něco zajímavého. Např. vybrat pouze konkrétní funkce/třídy, které se budou uvažovat a ostatní ignorovat (přes parametry analýzy). Tipy na čem to zkusit: Apache Tomcat, Apache Cassandra, GNU Coreutils/Binutils, Mozilla, Chromium, FFmpeg, libGraphicsMagick, MariaDB, GCC, Thunderbird, PostgreSQL, Git.

• Vymyslet nebo najít nějaké dobré praktické příklady pro kontrakty (něco jiného než práce s kolekcemi).

• Udělat experimenty s programem Lottery z článku ThreadSafe: Static Analysis for Java Concurrency. Program obsahuje porušení atomicity - viz článek. Program se nachází v tomto benchmarku. Podívat se i na ostatní programy z toho benchmarku.

• Možná zkusit spustit analýzu na nějakých programech z VeriFIT Repository of Test Cases for Concurrency Testing.

• Zamyslet se nad tím, že když mám atomickou množinu {f, g} a potom někde uvidím neatomickou sekvenci f h1 ... hn g, tak tohle nedetekuji jako porušení. Co s tím? Tohle se dá částečně řešit tím, že pokud jsou ty funkce h1 ... hn nějaké banální funkce, tak je mohu ignorovat.

• Zamyslet se nad použitím strojového učení pro vhodné nastavení parametrů analýzy. Tj. např. jaké funkce ignorovat a na jaké se zaměřit. Nebo se nějak strojově učit, které nahlášené porušení atomicity jsou reálné chyby. Ale na čem se učit?

• Nějakým způsobem uvažovat a pracovat s parametrickými kontrakty.

• Uvažovat zamykání typu try_lock. Má to různé varianty v C, C++, Java.

• Uvažovat nad tím, jak udělat to, aby se za chybu nepovažovalo pouze to, že se nějaké funkce nevolají atomicky, ale že nejsou proloženy nějakými jinými konkrétními funkcemi. Jak detekovat takové kontrakty staticky? Jak je ověřovat?