Absztrakt adatfolyamalapú utasításredukció párhuzamos programok modellellenőrzésének támogatásához
Az utóbbi évtizedekben a többmagos processzorok és a többszálú programok egyre nagyobb mértékű térhódítását figyelhettük meg ipari és biztonságkritikus rendszerekben a technológia ugrásszerű fejlődésének köszönhetően. A párhuzamos szoftverek verifikációja ugyanakkor jelentős kihívást jelent a szálak nagyszámú lehetséges átlapolódása miatt. A kielégítő tesztlefedettség elérése így nagy kihívást jelent, naiv modellellenőrzési technikák pedig rosszul skálázódnak, e nagyfokú bonyolultság miatt gyakorlatilag alkalmazhatatlanná válnak.
Az absztrakciós-finomítási algoritmusok hatékony technikák az állapottérben való elérhetőség vizsgálatára. Azonban az állapottér bejárása során a követő állapotok kiszámítása, vagyis az utasítások kiértékelése költséges feladat, amely gyakran SMT-probléma megoldását igényli. Másrészről viszont sok esetben egy utasítás kiértékelése nincs hatással az ellenőrzött tulajdonságra. Ilyen esetekben egyszerűsíthető az követő állapotok kiszámítása. Számos algoritmus létezik, amely statikusan elemzi a modellt és eltávolítja a modellből a nem releváns változókat vagy utasításokat. Párhuzamos szoftverekben azonban gyakori, hogy egy utasítás eredményét a szálak egy bizonyos átlapolódásában használják másik utasítások, míg egy másik ütemezés mellett nem használják. A modellt statikusan elemző algoritmusok nem tudják kiegyszerűsíteni az ilyen utasításokat.
Munkámban egy új, dinamikus megközelítést javaslok, amely absztrakt adatfolyam-elemzés segítségével, illetve az egyes szálak aktuális állapota alapján felismeri, hogy egy utasítás egyszerűsíthető-e az állapottér feltárása során. Módszerem jelentősen képes csökkenteni a követő állapot számítására fordított időt, ezáltal pedig a verifikáció teljes idejét is. Végezetül kiértékelem a bemutatott algoritmus teljesítményét egy nagyszámú benchmark programhalmazon.
szerző
-
Telbisz Csanád Ferenc
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc)
konzulensek
-
-
Szekeres Dániel
Doktorandusz, Mesterséges Intelligencia és Rendszertervezés Tanszék
