Ellenpélda-alapú absztrakció finomítás alkalmazásai párhuzamos programokon

A formális szoftververifikáció aktívan kutatott alterülete a többszálú programok hatékony kezelésének problémája. A többmagos processzorok biztonságkritikus rendszerekben való megjelenésével egyre nagyobb szükség van olyan robusztus, a biztonságosság bizonyítására alkalmas megoldásokra, amelyek képesek figyelembe venni a több mag jelentette megnövekedett komplexitást. Ezen új kihívások legfőbb oka a megosztott adatokhoz történő párhuzamos hozzáférés, ami újfajta hibalehetőségek (pl. memória- vagy cache-inkonzisztencia) révén előre nem látható, potenciálisan katasztrofális hibához vezető problémákat okozhatnak a szoftverben és a hardverben.

A szoftververifikáció terén eddig publikált kutatások többnyire a probléma egy részhalmazát célozták, leszűkítve arra az esetre, amikor minden adathozzáférés szigorúan szekvenciális. Ezen megoldások nem alkalmasak a gyenge rendezésű hardver-szoftver rendszerek analízisére, melyeket azonban széles körben alkalmaznak a hatékonyság növelése érdekében. A tudományos világ csak az elmúlt néhány évben kezdett el új, általánosabban alkalmazható, memóriamodell-alapú megoldások kifejlesztésével foglalkozni. A probléma komplexitása miatt ezek a megoldások általában a korlátos modellellenőrzés kiterjesztései, melyek csak a program első k lépéséről képesek érvelni, és így nem tekinthetőek általános megoldásnak.

Jelen dolgozatban bemutatok egy új, memóriamodellt figyelembe vevő, ellenpéldaalapú absztrakciófinomítás (CEGAR) technikát alkalmazó nem-korlátos modellellenőrző algoritmust gyengén rendezett párhuzamos programok kezelésére. Az algoritmus hatékonyságát a terület meghatározó szekvenciális és gyenge rendezésű memóriát feltételező verifikációs eszközeivel összevetve értékelem ki. Bemutatok továbbá egy összefoglaló képet a szekvenciális memóriamodellű, párhuzamos programokat kezelő megoldásokról, melyek a CEGAR technikát használják. Ezeket a megközelítéseket összehasonlítom a komplexitásuk, hatékonyságuk és használhatóságuk szerint is.

szerző

• 
  Bajczi Levente
  Mérnök informatikus szak, mesterképzés
  mesterképzés (MA/MSc)
  

konzulens

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

helyezés