Memóriamodellekkel paraméterezhető állapotmentes szoftver-modellellenőrzés

A többmagos hardveren futó többszálú programok formális verifikációja sokáig a terület legnagyobb kihívásai közé tartozott. A probléma nehézségét elsősorban a szálak végrehajtásainak tetszőleges átfedése jelenti. Ennek ellenére a többmagos beágyazott processzorok iránti igény egyre hangsúlyosabban megjelenik biztonságkritikus környezetben is, elkerülhetetlenné téve, hogy a problémakörrel foglalkozzunk. A többszálú programok nemdeterminisztikus viselkedése ugyanis nagyban megnehezíti a tesztelésüket, így még fontosabbá válik a formális módszerek használata.

Ezen felül a többmagos processzorok a teljesítmény növelése érdekében sok optimalizációs technikát tartalmaznak - egy ilyen módszer a memóriakezelő utasítások átrendezésének lehetővé tétele. Ennek motivációja az, hogy a processzor az általánosan sokkal lassabb memóriautasítások befejezésére való várakozás közben is hasznos munkát végezhessen. Az átrendezés azonban bizonyos esetekben váratlan viselkedésekhez vezethet a tisztán szekvenciális futáshoz képest. Kevés ellenőrzési módszert adaptáltak ezen viselkedés kezelésére, és ezek többsége is előre meghatározott memóriamodelleket feltételez, melyek testreszabása nem lehetséges. Ez csökkenti a módszerek alkalmazhatóságát, mivel a legtöbb hardver nem teljesen feleltethető meg egy-egy elméleti modellnek (akár szándékosan, akár tervezési hibák miatt).

Ezen dolgozatban egy olyan algoritmust mutatok be, ami bemenetként egy futásidejű hibadetektálásokkal (assert) annotált programot és egy memóriamodellt fogad, kimenetként pedig megadja, hogy az adott memóriamodellt betartó processzoron futtatva elérhető-e hibaállapot a programon belül. Az algoritmus az állapotmentes modellellenőrzés megközelítésére épít, és okos állapottér-bejárási stratégiájával lényegesen kisebb memóriahasználatot eredményezhet, mint a hagyományos modellellenőrző algoritmusok. A dolgozatban belátom, hogy - bizonyos feltételeknek megfelelő programok esetén - az algoritmus helyes, és optimális a megvizsgált lefutások tekintetében. Ezen felül néhány ismert architektúrára és programra alkalmazva a teljesítményét is kiértékelem, korszerű szoftver-modellellenőrző eszközökkel összehasonlításban. Munkám eredménye várhatóan hozzájárul majd a többmagos architektúrákon futó többszálú szoftverek kritikus beágyazott rendszerekben való elterjedéséhez, ezzel végső soron jobb teljesítményt és alacsonyabb költségeket hozva az érintett iparágakban.

szerző

• 
  Bajczi Levente
  Villamosmérnöki szak, alapképzés
  alapképzés (BA/BSc)
  

konzulens

• 
  Dr. Molnár Vince
  Adjunktus, Méréstechnika és Információs Rendszerek Tanszék

helyezés