ˇ ´ UCEN ´I TECHNICKE ´ V BRNE ˇ VYSOKE BRNO UNIVERSITY OF TECHNOLOGY
ˇ ´ICH TECHNOLOGI´I FAKULTA INFORMACN ´ ´ U ˚ USTAV INTELIGENTN´ICH SYSTEM FACULTY OF INFORMATION TECHNOLOGY DEPARTMENT OF INTELLIGENT SYSTEMS
BOUNDED MODEL CHECKING ´ V NASTROJI JAVA PATHFINDER
´ PRACE ´ DIPLOMOVA MASTER’S THESIS
´ AUTOR PRACE AUTHOR
BRNO 2008
´ Bc. VENDULA HRUBA
ˇ ´ UCEN ´I TECHNICKE ´ V BRNEˇ VYSOKE BRNO UNIVERSITY OF TECHNOLOGY
ˇ ´ICH TECHNOLOGI´I FAKULTA INFORMACN ´ ´ U ˚ USTAV INTELIGENTN´ICH SYSTEM FACULTY OF INFORMATION TECHNOLOGY DEPARTMENT OF INTELLIGENT SYSTEMS
BOUNDED MODEL CHECKING ´ V NASTROJI JAVA PATHFINDER BOUNDED MODEL CHECKING USING JAVA PATHFINDER
´ PRACE ´ DIPLOMOVA MASTER’S THESIS
´ AUTOR PRACE
´ Bc. VENDULA HRUBA
AUTHOR
´ VEDOUC´I PRACE SUPERVISOR
BRNO 2008
ˇ Ing. BOHUSLAV KRENA, Ph.D.
Abstrakt Diplomov´ a pr´ ace je vˇenovan´ a aplikaci form´aln´ı metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojen´e se soubˇeˇznost´ı. Pr´ace je zamˇeˇrena na programy napsan´e v jazyce Java, a proto pro verifikaˇcn´ı metodu byl zvolen model checker Java Pathfinder, kter´ y je urˇcen pro Java programy. Vlastn´ı verifikaˇcn´ı metoda spoˇc´ıv´a v aplikaci strategie pro navigaci stavov´ ym prostorem do m´ısta verifikace. Z dan´eho m´ısta je spuˇstˇen bounded model checking pro ovˇeˇren´ı opravy. Navigace stavov´ ym prostorem je implementov´ ana pomoc´ı strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementov´ any dalˇs´ı parametry a moduly pro verifikaci speci´aln´ıch vlastnost´ı syst´emu, kter´e ovˇeˇruj´ı koreknost opravy chyby. Bounded model checking se prov´ad´ı v okol´ı opravy.
Kl´ıˇ cov´ a slova Model Checking, Java PathFinder, Bounded model checking, verifikace, Record&Replay trace, automatick´ a oprava, soubˇeˇznost, ovˇeˇrov´an´ı opravy
Abstract This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.
Keywords Model Checking, Java PathFinder, Bounded model checking, verification, Record&Replay trace, self-healing, concurrency, healing assurance
Citace Vendula Hrub´ a: Bounded model checking v n´astroji Java PathFinder, diplomov´a pr´ace, Brno, FIT VUT v Brnˇe, 2008
Bounded model checking v n´ astroji Java PathFinder Prohl´ aˇ sen´ı Prohlaˇsuji, ˇze jsem tuto diplovomou pr´aci vypracovala samostatnˇe pod veden´ım pana Ing. Bohuslava Kˇreny, Ph.D. ....................... Vendula Hrub´ a 19. kvˇetna 2008
Podˇ ekov´ an´ı Chtˇela bych podˇekovat cel´e sv´e rodinˇe, pr´atel˚ um a spoluˇz´ak˚ um za jejich podporu a pomoc pˇri studiu. Tato pr´ ace byla podpoˇrena Evropskou uni´ı v r´amci FP6-IST projektu SHADOWS (ˇc. smlouvy IST-035157). Za obsah pr´ ace odpov´ıd´a pouze jej´ı autor. Tato pr´ace nevyjadˇruje n´azor Evropsk´e unie a Evropsk´ a unie nen´ı odpovˇedn´a za uˇzit´ı jak´ekoliv informace v pr´aci uveden´e.
Acknowledgment This work is supported by the European Community under the Information Society Technologies (IST) programme of the 6th FP for RTD – project SHADOWS contract IST-035157. The authors are solely responsible for the content of this thesis. It does not represent the opinion of the European Community, and the European Community is not responsible for any use that might be made of data appearing therein.
c Vendula Hrub´
a, 2008. Tato pr´ ace vznikla jako ˇskoln´ı d´ılo na Vysok´em uˇcen´ı technick´em v Brnˇe, Fakultˇe informaˇcn´ıch technologi´ı. Pr´ ace je chr´ anˇena autorsk´ym z´ akonem a jej´ı uˇzit´ı bez udˇelen´ı opr´ avnˇen´ı autorem je nez´ akonn´e, s v´yjimkou z´ akonem definovan´ych pˇr´ıpad˚ u.
Obsah ´ 1 Uvod
3
2 Rozbor problematiky 2.1 Proces automatick´e opravy . . . 2.1.1 Princip opravy probl´emu 2.1.2 Princip ovˇeˇren´ı opravy . . 2.2 Form´ aln´ı metody . . . . . . . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
5 5 6 7 7
3 Model Checking 3.1 Model syst´emu . . . . . . . . 3.2 Specifikace syst´emu . . . . . . 3.3 V´ ystup verifikace . . . . . . . 3.4 Probl´em stavov´e exploze . . . 3.5 Bounded Model Checking . . 3.6 Navigace stavov´ ym prostorem
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
. . . . . .
10 11 12 14 14 16 17
4 Java PathFinder 4.1 Z´ akladn´ı charakterisitika . . . . . 4.2 Specifikace . . . . . . . . . . . . . 4.3 Prohled´ av´ an´ı stavov´eho prostoru 4.4 Rozˇsiˇritelnost . . . . . . . . . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
19 20 21 22 24
. . . . . . . . . . . .
25 26 27 28 31 33 35 37 39 39 41 42 43
. . . . . .
5 Implementace 5.1 Record&Replay trace v JPF . . . . . . . . . . . . . . . . 5.1.1 Record&Replay pomoc´ı ChoiceGener´ator˚ u. . . . 5.1.2 Record&Replay pomoc´ı byte-code instrukc´ı . . . 5.1.3 Pˇr´ıklad na Record&Replay trace . . . . . . . . . 5.2 Bounded model checking v JPF . . . . . . . . . . . . . . 5.2.1 Pˇr´ıklad na Bounded Model Checking . . . . . . . 5.3 Modifikace Replay trace pro projekt SHADOWS . . . . 5.3.1 Replay trace pomoc´ı p˚ uvodn´ım k´odu . . . . . . . 5.3.2 Replay trace pomoc´ı instrumentovan´eho k´odu . . 5.4 V´ ysledky a Testy . . . . . . . . . . . . . . . . . . . . . . 5.4.1 Rychlost bˇehu programu ve pouˇzit´ ych n´astroj´ıch 5.4.2 Rychlost metody Record&Replay trace . . . . . . 6 Z´ avˇ er
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
45
1
Literatura
47
2
Kapitola 1
´ Uvod V dneˇsn´ı dobˇe se setk´ av´ ame s poˇc´ıtaˇci nebo poˇc´ıtaˇcov´ ymi programy t´emˇeˇr na kaˇzd´em kroku. At’ uˇz se jedn´ a o mobiln´ı telefony, bankovn´ı u ´ˇcty, pr˚ umyslov´e stroje nebo ˇr´ıd´ıc´ı stˇrediska. Vˇzdy chceme, aby n´ am naˇse pˇr´ıstroje pracovaly spr´avnˇe, coˇz ale jiˇz z principu nelze. O ˇz´ adn´em rozs´ ahlejˇs´ım programu nem˚ uˇzeme prohl´asit, ˇze neobsahuje chyby, lze pouze ˇr´ıci, jak´e chyby neobsahuje. Jsou pˇr´ıpady, kdy n´am nevad´ı, ˇze program zatuhne“ nebo ” provede neplatnou akci, napˇr. pˇri pos´ıl´an´ı emailu se nepodaˇr´ı komunikace se serverem, email se neodeˇsle a jeho obsah je ztracen. V takov´em pˇr´ıpadˇe n´as chyba zamrz´ı, mus´ıme email napsat znova. M˚ uˇze ovˇsem nastat situace, kdy se jedn´a o d˚ uleˇzit´e ud´alosti, kter´e mohou zp˚ usobit z´ avaˇznˇejˇs´ı probl´emy – nepˇriˇcten´ı spr´avn´e ˇc´astky na bankovn´ı u ´ˇcet, porucha na l´ekaˇrsk´ ych pˇr´ıstroj´ıch, atd. V takov´em pˇr´ıpadˇe rozhodnˇe nechceme, aby program zatuhl nebo vykonal neoˇcek´ avanou akci. Z toho d˚ uvodu se vynakl´ad´a spousta penˇez na testov´ an´ı a ovˇeˇrov´ an´ı korektnosti program˚ u, aby programy vykon´avaly pouze poˇzadovan´e ud´alosti. I pˇres veˇsker´e snahy v programech z˚ ust´avaj´ı chyby, kter´e se dostanou aˇz k uˇzivateli. D´av´a tedy smysl se zab´ yvat opravou tˇechto chyb, kter´e se neodhal´ı pˇri testov´an´ı a snaˇzit se je opravit za bˇehu aplikace. Pr´avˇe o to se snaˇz´ı projekt SHADOWS, jehoˇz souˇc´ast´ı je i tato diplomov´ a pr´ ace. SHADOWS – A Self-healing Approach to Designing Complex Software Systems je evropsk´ y projekt, kter´ y se zab´ yv´a procesem automatick´e opravy (selfhealing approach). Princip procesu a jeho c´ıl se daj´ı specifikovat pomoc´ı n´asleduj´ıc´ıch ˇctyˇr z´akladn´ıch krok˚ u: 1. zjiˇ stˇ en´ı probl´ emu (problem detection) – pˇredt´ım neˇz se zaˇcne s opravou (l´eˇcen´ım) je potˇreba urˇcit, zda je v syst´emu nˇejak´ y probl´em a ˇceho se t´ yk´a, 2. nalezen´ı pˇ r´ıˇ ciny probl´ emu (problem localization) – druh´ ym krokem po urˇcen´ı moˇzn´eho probl´emu v syst´emu je tˇreba tento probl´em lokalizovat resp. urˇcit m´ısto v programu (sledovan´em syst´emu), kde se probl´em vyskytuje, 3. oprava probl´ emu (problem healing) – dalˇs´ım krokem je v´ ybˇer akce, ze seznamu nab´ızen´ ych l´eˇc´ıc´ıch akc´ı, kter´e je moˇzn´e pro opravu detekovan´eho probl´emu pouˇz´ıt, 4. ovˇ eˇ ren´ı opravy (problem assurance) – posledn´ım krokem je ovˇeˇren´ı, zda provedn´ı opravn´e akce nezp˚ usobilo v syst´emu jin´ y probl´em. L´eˇc´ıc´ı akce zmˇen´ı chov´ an´ı syst´emu, pˇredpokl´ ad´ ame, ˇze se nyn´ı syst´em bude chovat korektnˇe vzhledem k urˇcen´ ym poˇzadavk˚ um. Nicm´enˇe opravn´a akce m˚ uˇze zmˇenit chov´an´ı syst´emu takov´ ym zp˚ usobem, ˇze se objev´ı jin´ y probl´em. Z toho d˚ uvodu je potˇreba prov´est ovˇeˇren´ı opravy.
3
Projekt SHADOWS se zab´ yv´ a splnˇen´ım funkˇcn´ıch poˇzadavk˚ u, v´ ykonem a v neposledn´ı ˇradˇe spr´ avn´ ym pouˇzit´ım soubˇeˇzn´eho prov´adˇen´ı v programu. Fakulta informaˇcn´ıch technologi´ı se v projektu vˇenuje ˇc´ asti zamˇeˇren´e na soubˇeˇzn´e prov´adˇen´ı (concurrency). Pˇresnˇeji se vˇenuje l´eˇcen´ı chyb, kter´e vznikaj´ı pomoc´ı paralelismu resp. soubˇeˇznosti v syst´emu. Jedn´a se o chyby typu deadlocks, data races, lost notification, atd. L´eˇcen´ı se zamˇeˇruje na opravy chyb v Java programech, ve kter´ ych se soubˇeˇznost implementuje velice snadno pomoc´ı vl´aken. Tato diplomov´ a pr´ ace je vˇenovan´a posledn´ımu z uveden´ ych krok˚ u opravn´eho procesu – ovˇeˇren´ı l´eˇc´ıc´ı akce. K tomu, aby bylo moˇzn´e navrhnout vhodnou metodu pro ovˇeˇren´ı l´eˇc´ıc´ı akce, je zapotˇreb´ı zn´ at, co l´eˇc´ıc´ı akce prov´ad´ı a jak´ ym zp˚ usobem funguje. Pokud zn´ame princip opravn´e akce, je moˇzn´e navrhnout a posl´eze implementovat metody pro ovˇeˇren´ı korektnosti opravy. Dalˇs´ı text je dˇelen do n´ asleduj´ıc´ıch kapitol. V druh´e kapitole jsou podrobnˇeji rozeps´any jednotliv´e kroky opravn´eho procesu pro lepˇs´ı porozumˇen´ı cel´eho procesu opravy. D´ale jsou zde struˇcnˇe pops´ any form´ aln´ı metody, ze kter´ ych byla pro ovˇeˇren´ı opravy zvolena metoda model checking. O model checkingu, jeho z´akladech a principu pojedn´av´a tˇret´ı kapitola. Zde jsou tak´e pops´ any jeho modifikace, probl´em stavov´e exploze a jeho moˇzn´a ˇreˇsen´ı. Ve ˇctvrt´e kapitole jsou nejprve uvedeny r˚ uzn´e model checkery, ze kter´ ych byl pro verifikaci zvolen model checker – Java PathFinder. Jeho popis a nastaven´ı jeho vlastnost´ı jsou v t´eto kapitole tak´e uvedeny. Dalˇs´ı kapitola popisuje hloubˇeji zvolenou metodu pro verifikaci syst´emu z hlediska implementace v Java PathFinderu. Jsou zde uvedeny pˇr´ıklady a dosaˇzen´e v´ ysledky. Posledn´ı kapitolou je z´ avˇer, kter´ y obsahuje shrnut´ı v´ ysledk˚ u a n´astin dalˇs´ı pr´ace na projektu.
4
Kapitola 2
Rozbor problematiky 2.1
Proces automatick´ e opravy
V n´asleduj´ıc´ıch odstavc´ıch budou podrobnˇeji rozeps´any jednotliv´e kroky procesu automatick´e opravy. Kroky procesu popisuj´ı princip l´eˇcen´ı chyb, kter´e vznikaj´ı soubˇeˇznost´ı v Java programech [12]. Zjiˇ stˇ en´ı probl´ emu. V prvn´ım kroku se monitoruje vykon´av´an´ı programu. Monitorov´an´ı prob´ıh´ a pomoc´ı instrumentace programu nad byte-codem. Pokud by se chyba hledala na u ´rovni byte-codu pomoc´ı ladˇen´ı (debugging), je velk´a pravdˇepodobnost, ˇze chyba nebude nalezena. Program na u ´rovni byte-codu umoˇzn ˇuje velk´e mnoˇzstv´ı moˇznost´ı prokl´ad´ an´ı instrukc´ı a t´ım se sniˇzuje pravdˇepodobnost nalezen´ı chyby bˇehem testov´an´ı. Pomoc´ı instrumentace se do programu zav´ ad´ı tak´e ˇsum (dalˇs´ı instrukce), pomoc´ı kter´ ych se zvyˇsuje pravdˇepodobnost odhalen´ı chyb vznikl´ ych nespr´avn´ ym prokl´ad´an´ım instrukc´ı (data race). Instrumentace k´ odu se prov´ ad´ı pomoc´ı n´astroje ConTest, kter´ y pracuje nad Java bytecodem a jehoˇz bliˇzˇs´ı popis a specifikace jsou uvedeny v [5]. ConTest je n´astroj vyv´ıjen´ y v´ yzkumnou laboratoˇr´ı IBM pro testov´an´ı Java program˚ u, kter´e obsahuj´ı v´ıce vl´aken [6]. Nalezen´ı pˇ r´ıˇ ciny probl´ emu. Nalezen´ı pˇr´ıˇciny probl´emu je obt´ıˇzn´ yu ´kol i pro ˇclovˇeka, t´ım tˇeˇzˇs´ım u ´kolem se st´ av´ a navrˇzen´ı mechanizmu pro automatickou detekci pˇr´ıˇciny chyby. V projektu SHADOWS byly navrˇzeny metody pro automatickou detekci. Prvn´ı metodou je spr´ avn´ y odhad a v´ ybˇer opravn´e akce ze speci´aln´ıho seznamu, kter´ y byl navrˇzen pro v´ ybˇer spr´ avn´e opravy chyb vznikl´ ych soubˇeˇznost´ı. Jedn´a se o n´asleduj´ıc´ı detektory: dataRace detektor, atomRace detektor nebo deadlock detektor. Jinou moˇznost´ı je prov´adˇen´ı velk´eho mnoˇzstv´ı test˚ u s r˚ uzn´ ymi body instrumentace a n´asledn´e statistick´e vyhodnocen´ı dosaˇzen´ ych v´ ysledk˚ u. Pomoc´ı z´ıskan´ ych statistick´ ych dat a korektnosti chov´an´ı programu v dan´em testu se d´ a urˇcit probl´em. Oba v´ yˇse popsan´e pˇr´ıstupy lze kombinovat s form´aln´ımi metodami (napˇr. model checkingem, statickou anal´ yzou) a pomoc´ı nich sn´ıˇzit poˇcet false alarm˚ u. False alarmy vznikaj´ı v pˇr´ıpadˇe, pokud je nadetekov´an probl´em, kter´ y ve skuteˇcnosti v programu nen´ı. Z principu funkce form´aln´ıch metod, by se tyto metody daly aplikovat na samotnou lokalizaci probl´emu v syst´emu. Nicm´enˇe jejich aplikace na re´aln´ y syst´em je problematick´ a z d˚ uvodu stavov´e exploze. Ta je kritick´ ym probl´emem form´aln´ıch metod, kter´ y br´ an´ı jejich nasazen´ı na re´aln´e syst´emy a proveden´ı jejich celkov´e verifikaci. Oprava probl´ emu. N´ astroj (tool) pro opravu probl´emu m˚ uˇze b´ yt zaloˇzen na v´ ybˇeru opravn´e akce, kter´e jsou vyjmenov´any ve speci´aln´ım seznamu. Zvolen´a oprava detekovan´eho probl´emu m˚ uˇze b´ yt nab´ıdnuta v´ yvoj´aˇri jako moˇzn´e ˇreˇsen´ı bˇehem v´ yvoje syst´emu. V´ yvoj´ aˇr se pak s´ am rozhodne, zda nab´ızenou akci provede ˇci nikoliv. C´ılem projektu je ovˇsem 5
l´eˇcit chyby, kter´e se projev´ı u uˇzivatele. Z´amˇerem je tedy l´eˇcit chyby, kter´e se jiˇz jednou v syst´emu vyskytly a na nˇe aplikovat opravu, a t´ım zamezit jejich opˇetovn´emu v´ yskytu v aplikaci u uˇzivatele. Prozat´ım se l´eˇc´ıc´ı akce zamˇeˇruj´ı na probl´emy typu data races. Data races vznikaj´ı v d˚ usledku paraleln´ıho pˇr´ıstupu ke sd´ılen´e promˇenn´e ve stejn´ y ˇcasov´ y okamˇzik z v´ıce m´ıst, jehoˇz d˚ usledkem je konfliktn´ı z´apis do sd´ılen´e promˇenn´e. Moˇzn´ ym ˇreˇsen´ım odstranˇen´ı probl´emu data race je pˇrid´an´ı z´amk˚ u (locks). Pˇresnˇejˇs´ı popis jednotliv´ ych oprav i samotn´eho probl´emu data race je bl´ıˇze uveden v [1, 12]. Ovˇ eˇ ren´ı opravy. Posledn´ım krokem procesu je ovˇeˇren´ı opravn´e akce. Bylo by chybn´e pˇredpokl´ adat, ˇze lze navrhnout univerz´aln´ı opravu urˇcit´eho probl´emu, kter´a by fungovala za vˇsech okolnost´ı. Z toho d˚ uvodu jsou navrˇzeny speci´aln´ı l´eˇc´ıc´ı akce pro konkr´etn´ı pˇr´ıpady v´ yskytu urˇcit´eho probl´emu. Proto je tak´e potˇreba ovˇeˇrit, zda zvolen´a oprava chyby byla u ´spˇeˇsn´ a a bezpeˇcn´ a (napˇr. ovˇeˇren´ı zda pˇrid´an´ı z´amk˚ u pro odstranˇen´ı probl´emu data race, nezp˚ usobilo jin´ y probl´em – deadlock, apod.). Ke kontrole opravy je vhodn´e pouˇz´ıt form´aln´ı verifikaci, jedn´ a se efektivn´ı metody pro ovˇeˇrov´an´ı spr´avnosti syst´emu. Mezi form´aln´ı metody patˇr´ı model checking, statick´a anal´ yza nebo theorem proving. V pˇr´ıpadˇe jejich omezen´ı resp. modifikace je lze aplikovat na re´aln´ y syst´em a zverifikovat ho. Jak jiˇz bylo uvedeno v u ´vodu, k tomu aby bylo moˇzn´e navrhnout spr´avnou metodu pro ovˇeˇren´ı opravy, je potˇreba zn´ at jej´ı podstatu a zp˚ usob aplikace na probl´em resp. chybu.
2.1.1
Princip opravy probl´ emu
Pˇredpokl´ adejme, ˇze v monitorovan´em syst´emu byl lokalizov´an probl´em. Ten se nach´ az´ı ve speci´ aln´ım seznamu probl´em˚ u, pro kter´e jsou navrˇzeny l´eˇc´ıc´ı akce. Posl´eze se zvolen´ a l´eˇc´ıc´ı akce aplikuje na detekovan´ y probl´em, a ta probl´em v programu oprav´ı [1]. Existuj´ı dvˇe moˇznosti jak opravu na probl´em aplikovat. Prvn´ı moˇznost´ı je pouze navrˇzen´ı opravy v´ yvoj´aˇri, kter´ y se s´ am rozhodne, zda ji na opravu pouˇzije ˇci nikoliv. Druhou vhodnˇejˇs´ı metodou je pouˇzit´ı arichitektury listener˚ u. Listenery umoˇznuj´ı modifikovat chov´an´ı syst´emu za jeho bˇehu bez nutnosti explicitn´ıho z´asahu do zdrojov´eho k´odu. Architektura listener˚ u je souˇc´ ast´ı jiˇz zmiˇ novan´eho n´ astroje ConTest [5, 16]. Oprava pomoc´ı pl´ anov´ an´ı. D´ıky monitorov´an´ı (sledov´an´ı) syst´emu za jeho bˇehu vznik´a v bˇehu programu ˇsum, resp. v programu se vykon´av´a v´ıce instrukc´ı neˇz v bˇeˇzn´em bˇehu programu bez monitorov´ an´ı. Pomoc´ı tohoto mechanizmu je snadnˇejˇs´ı odhalit chyby vznikl´e soubˇeˇznost´ı, kter´e se projevuj´ı pouze pˇri urˇcit´em prokl´ad´an´ı instrukc´ı. K nespr´avn´emu prokl´ ad´ an´ı instrukc´ı vedouc´ı k chybˇe doch´az´ı napˇr´ıklad pˇri vyt´ıˇzen´ı procesoru jin´ ymi programy, kter´e nejsou bˇeˇznˇe pˇri testov´an´ı programu spuˇstˇeny. Proto monitorov´an´ı, kter´e tak´e potˇrebuje porv´ adˇet vlastn´ı instrukce umoˇznuje odhalen´ı tˇechto chyb. Pro opravu podobn´ ych chyb v Java programech je nˇekdy postaˇcuj´ıc´ı zavol´an´ı metody yield(). Metoda se zavol´a pˇred kritickou seck´ı, kde doch´az´ı k chybˇe. Princip metody yield() spoˇc´ıv´a v pˇrepnut´ı kontextu na jin´e vl´ akno (aktu´ aln´ı vl´akno se vzd´av´a procesoru), pˇri dalˇs´ım pˇridˇelen´ı procesoru je jiˇz dostatek ˇcasu na vykon´an´ı kritick´e sekce vcelku (bez pˇrepnut´ı kontextu). Uvedenou techniku lze kombinovat s pˇridˇelov´an´ım r˚ uzn´ ych priorit vl´akn˚ um. V takov´em pˇr´ıpadˇe do kritick´e sekce m˚ uˇze vstoupit nebo ji pˇreruˇsit pouze vl´akno se stejnou nebo vyˇsˇs´ı prioritou. Oprava pomoc´ı synchronizace. Zmiˇ novan´a ˇc´ast projektu SHADOWS je zamˇeˇrena na chyby, kter´e jsou zp˚ usobeny nevhodn´ ym pouˇzit´ım synchronizace, nebo kdyˇz synchronizace zcela chyb´ı. V pˇr´ıpadˇe chybn´eho pouˇzit´ı synchronizace obsahuje oprava vhodnou zmˇenu v synchronizaci. Pokud se jedn´ a o probl´em chybˇej´ıc´ı synchronizaci nad sd´ılenou promˇennou, je tˇreba vˇenovat dostateˇcnou pozornost pˇrid´an´ı z´amku. Z´amek je potˇreba vloˇzit takov´ ym
6
zp˚ usobem, aby jeho pˇrid´ an´ı nezp˚ usobilo jin´ y probl´em v syst´emu, typick´ ym probl´emem je vznik deadlocku. Je tedy nutno ovˇeˇrit, zda pˇrid´an´ı z´amk˚ u skuteˇcnˇe vyˇreˇsilo probl´em (data race) a d´ ale zverifikovat, ˇze zm´ınˇen´a oprava nezp˚ usobila v syst´emu jin´ y probl´em.
2.1.2
Princip ovˇ eˇ ren´ı opravy
Pro ovˇeˇren´ı opravy je moˇzn´e pouˇz´ıt techniky form´aln´ı verifikace jako model checking, statickou anal´ yzu atd. K tomu, aby bylo moˇzn´e form´aln´ı metody aplikovat na re´aln´ y syst´em, je tˇreba udˇelat jejich omezen´ı nebo urˇcitou modifikaci. V tomto pˇr´ıpadˇe – ovˇeˇrov´an´ı opravy, nen´ı c´ılem zverifikovat cel´ y syst´em, ale pouze okol´ı l´eˇcen´e chyby. Jde tedy o aplikaci form´aln´ı metody na konkr´etn´ı ˇc´ ast programu a na kompletn´ı re´aln´ y syst´em. Aplikace form´aln´ı metody m˚ uˇze vypadat n´ asledovnˇe. Pouˇzit´ı statick´e anal´ yzy nad byte-codem: v pˇr´ıpadˇe pouˇzit´ı opravn´e akce – pˇrid´an´ı z´amk˚ u (lock/unlock) je tˇreba ovˇeˇrit, zda nov´e z´amky nejsou v kolizi s jiˇz naimplementovanou synchronizac´ı. Pˇr´ıpadn´ a kolize synchronizace by mohla zp˚ usobit deadlock. Probl´em data races se ˇcasto vyskytuje nad jednoduch´ ymi pˇr´ıkazy (mal´a ˇc´ast k´odu). Prov´est statickou anal´ yzu nad malou ˇc´ ast´ı k´ odu nen´ı probl´em a tud´ıˇz odhalen´ı dan´eho probl´emu je moˇzn´e. Pro pouˇzit´ı model checkingu se je nejprve potˇreba dostat do poˇzadovan´eho stavu resp. do jeho okol´ı a zde posl´eze prov´est bounded model checking. Bounded model checking se provede do pˇredem urˇcen´e hloubky stavov´eho prostoru. K prohled´av´an´ı stavov´eho prostoru existuj´ı r˚ uzn´e heurisitiky, d´ ale je potˇreba pro prohled´av´an´ı stavov´eho prostoru zadat r˚ uzn´e specifikace, kter´e maj´ı b´ yt v syst´emu splnˇeny (verifikov´any). Pokud opravn´ a akce zp˚ usob´ı jin´ y probl´em a pomoc´ı ovˇeˇrov´an´ı opravy se dan´ y probl´em zjist´ı, je potˇreba upravit l´eˇc´ıc´ı akci tak, aby k nov´e chybˇe nedoch´azelo nebo zvolit jinou l´eˇc´ıc´ı akci. Po zmˇenˇe opravy je tˇreba prov´est nov´e ovˇeˇren´ı bˇehu programu, zda se jiˇz syst´em chov´ a korektnˇe. St´ ale zde ale pˇretrv´ av´ a probl´em moˇzn´eho v´ yskytu chyb. Verifikace syst´emu nebo ˇc´asti syst´emu se prov´ ad´ı vˇzdy vzhledem k nˇejak´ ym konkr´etn´ım vlastnostem a specifikac´ım. St´ale tedy neˇreˇs´ı probl´em, kdy o ˇz´adn´em syst´emu nelze ˇr´ıci, ˇze je bezchybn´ y. O programu lze pouze ˇr´ıci, kter´e chyby neobsahuje. Pokud je zn´am princip opravy, je moˇzn´e navrhnout a posl´eze implementovat takovou metodu pro ovˇeˇren´ı korektnosti opravy, kter´a ovˇeˇr´ı ty specifikace, u kter´ ych bˇehem l´eˇcen´ı doˇslo ke zmˇenˇe.
2.2
Form´ aln´ı metody
Form´aln´ı metody jsou zaloˇzeny na matematick´ ych metod´ach, um´ı dok´azat/vyvr´atit urˇcit´e specifikace syst´emu. Form´ aln´ımi metodami rozum´ıme verifikaˇcn´ı nebo analytick´e metody. Verifikace ovˇeˇruje zadan´e vlastnosti v syst´emu. Napˇr´ıklad v paraleln´ıch programech m˚ uˇze verifikace odpovˇedˇet na ot´azku, zda se v programu vyskytuje deadlock. Verifikace tedy vrac´ı odpovˇed’ ano/ne podle toho, jestli je verifikovan´a vlastnost v syst´emu splnˇena nebo ne. Existuj´ı ale tak´e specifikace, kter´e ovˇeˇrit nelze. Anal´yza poskytuje odpovˇedi na obecnˇejˇs´ı ot´azky o syst´emu, neodpov´ıd´a tedy ano/ne, zda je vlastnost v syst´emu splnˇena, ale pod´av´a komplexnˇejˇs´ı informace o chov´an´ı syst´emu jako optimalizace, synt´eza, apod. Rozd´ıl mezi form´ aln´ımi metodami a testov´an´ım spoˇc´ıv´a v odpovˇedi na ot´azku, zda syst´em obsahuje danou chybu. Pokud se bˇehem testov´an´ı objev´ı chyba, je zˇrejm´e, ˇze program danou chybu obsahuje, ale pokud se bˇehem testov´an´ı chyba neprojev´ı, neznamen´ a to, ˇze v programu zadan´ a chyba nen´ı. Narozd´ıl od form´aln´ı verifikace, jestliˇze se bˇehem
7
verifikace chyba neprojev´ı a byla provedena verifikace cel´eho syst´emu, uveden´a chyba se v syst´emu opravdu nevyskytuje. Ide´ aln´ı form´ aln´ı verifikace splˇ nuje n´asleduj´ıc´ı vlastnosti. Ide´aln´ı form´aln´ı verifikace je plnˇe automatick´ a, spolehliv´ a (pokud dojde k z´avˇeru, mus´ı b´ yt spr´avn´ y), u ´pln´a (pokud najde chybu, jedn´ a se o skuteˇcnou chybu – nejede o false alarm), koneˇcn´a (verifikace vˇzdy skonˇc´ı s urˇcit´ ym z´ avˇerem). Bohuˇzel v praxi ide´aln´ı verifikace neexistuje, kritick´ ym probl´emem verifikace je stavov´ a exploze. V pˇripadˇe syst´emu s koneˇcn´ ym stavov´ ym prostorem a moˇznost´ı vyuˇz´ıt´ı dostateˇcnˇe v´ ykonn´eho poˇc´ıtaˇce – verifikace vˇzdy dojde k z´avˇeru. V praxi se ale ˇcasto setk´av´ ame s neomezen´ ym stavov´ ym prostorem nebo nadmˇern´ ymi poˇzadavky na v´ ykon 32 poˇc´ıtaˇce (d˚ uvodem je pr´ ace s daty – jeden tˇricetidvou-bitov´ y integer m˚ uˇze nab´ yvat 2 hodnot, paralelismus, nedeterminismus, ...). Re´aln´e verifikace maj´ı tedy n´ asleduj´ıc´ı vlastnosti: produkuj´ı false alarmy, nekonˇc´ı vˇzdy korektnˇe, nejsou plnˇe automatick´e a nejsou stoprocetnˇe spolehliv´e. K tomu, aby bylo moˇzn´e prov´adˇet verifikace, je nejprve zapotˇreb´ı nadefinovat syst´em, kter´ y bude verifikov´ an a jeho vlastnosti, kter´e se maj´ı zkontrolovat. Vstupn´ı syst´em m˚ uˇze b´ yt pops´ an pomoc´ı modelu (petri net, promela, SMV, atd.) nebo jako re´aln´ y syst´em (programy v r˚ uzn´ ych programovac´ıch jazyc´ıch, Verilog, hardware pospan´ y ve VHDL, atd.). Vlastnosti, kter´e se maj´ı verifikovat, mohou b´ yt napˇr. ˇzivost promˇenn´ ych, invarianty, ukonˇcen´ı syst´emu pouze v poˇzadovan´em m´ıstˇe. Vlastnosti, kter´e se verifikuj´ı, lze rozdˇelit do dvou skupin: bezpeˇcnost a ˇzivost. Bezpeˇcnost n´am ˇr´ık´a, ˇze v syst´emu nikdy nenastane nic ˇspatn´eho, protipˇr´ıklad takov´e vlastnosti je koneˇcn´ y – nˇekdy nastane nˇeco ˇspatn´eho. Oproti tomu ˇzivost syst´emu ˇr´ık´ a, ˇze v syst´emu nˇekdy nastane nˇeco dobr´eho a protipˇr´ıklad je nekoneˇcn´ y– nikdy nenastane nic ˇspatn´eho. Lze tedy uv´est, ˇze bezpeˇcnost se verifikuje snadnˇeni neˇz ˇzivost. Pro popis vlastnost´ı je moˇzn´e pouˇz´ıt napˇr´ıklad formule tempor´aln´ıch logik,µ-calcul, labels, atd. Dalˇs´ı d˚ uleˇzitou charakteristikou vlastnost´ı pro verifikaci je ˇcas, kter´ y m´a dvˇe z´akladn´ı rozdˇelen´ı na ˇcas logick´ y/fyzick´ y a line´arn´ı/vˇetv´ıc´ı se. Logick´y ˇcas ukazuje ˇcasov´ y sled jednotliv´ ych ud´ alost´ı podle bˇehu, kdeˇzto fyzick´y ˇcas slouˇz´ı k urˇcen´ı kolik ˇcasu na jakou ud´alost bylo potˇreba vzhledem ke zvolen´emu mˇeˇr´ıtku. V line´ arn´ım ˇcase je pouze jedna moˇznost ˇcasu, je moˇzn´ y pouze line´ arn´ı bˇeh programu. Oproti tomu vˇetv´ıc´ı se ˇcas umoˇzn ˇuje spoleˇcn´ y n´ahled na dva bˇehy, kter´e se rozch´azej´ı aˇz posl´eze. Nejpouˇz´ıvanˇejˇs´ımi metodami pro form´aln´ı anal´ yzu a verifikaci jsou model checking, statick´ a anal´yza a theorem proving. Model checking. Model checking je algoritmick´a technika, kter´a ovˇeˇruje, zda syst´em y syst´em m˚ uˇze b´ yt pops´an jak modelem, tak splˇ nuje poˇzadovan´e vlastnosti [4]. Verifikovan´ re´aln´ ym syst´emem. Model checking umoˇzn ˇuje verifikovat syst´emy s koneˇcn´ ym stavov´ ym prostorem. Kritick´ ym probl´emem model checkingu je exploze stavov´eho prostoru, kde velikost stavov´eho prostoru roste exponenci´alnˇe s velikost´ı verifikovan´eho syst´emu [21]. Vlastnosti jsou typicky specifikov´ any pomoc´ı tempor´aln´ıch logik. V´ yhodami model checkingu jsou: vysok´ y stupeˇ n automatizace, snadn´e pouˇzit´ı (pokud to umoˇzn ˇuje syst´em), pomˇernˇe vˇseobecn´e pouˇzit´ı pro verifikaci r˚ uzn´ ych vlastnost´ı syst´emu. Oproti tomu hlavn´ı nev´ yhodou je jiˇz zmiˇ novan´a exploze stavov´eho prostoru, kter´ y se d´ a ˇreˇsit r˚ uzn´ ymi metodami jako redukce, abstrakce, kompozice syst´emu z ˇc´ast´ı, atd. Dalˇs´ı nev´ yhodou je nutnost modelovat okol´ı verifikovan´eho syst´emu jako jsou vstupy. Statick´ a anal´ yza. Statick´ a anal´ yza se neprov´ad´ı nad skuteˇcn´ ym bˇehem syst´emu, ale pouze nad zdrojov´ ym k´ odem. T´ım umoˇzn ˇuje zjistit informace o programu ze zdrojov´eho k´odu, aniˇz by bylo nutn´e program spouˇstˇet. Statick´e anal´ yzy jsou r˚ uzn´e druhy (typov´ a 8
anal´ yza, vyhled´ av´ an´ı chybov´ ych vzor˚ u – bug pattern, dataflow anal´ yza, apod.). V´ yhodami statick´e anal´ yzy je moˇznost verifikovat obrovsk´e syst´emy, z´aroveˇ n nen´ı nutn´e modelovat okol´ı syst´emu a nab´ız´ı velk´ y stupeˇ n automatizace. Nev´ yhodou je velk´a specializace jednotliv´ ych statick´ ych anal´ yz na konkr´etn´ı probl´emy. Pokud je c´ılem zverifikovat novˇe zadan´ y probl´em, mus´ı se nejprve navrhnout nov´a statick´a anal´ yza pro jeho ovˇeˇren´ı. Dalˇs´ı nev´ yhodou je vznik false alarm˚ u. D´ıky tomu, ˇze se statick´a anal´ yza prov´ad´ı nad zdrojov´ ym k´odem, m˚ uˇze nadetekovat chybu, kter´ a pˇri skuteˇcn´em bˇehu nikdy nenastane (false positive). Theorem proving. Jedn´ a se o deduktivn´ı verifikaci, kter´a vych´az´ı z axiom˚ u a pomoc´ı pouˇzit´ı r˚ uzn´ ych pravidel produkuje vlastnosti syst´emu. Uˇzit´ı jednotliv´ ych pravidel nen´ı automatick´e, je potˇreba z´ asahu uˇzivatele experta“, kter´ y vede d˚ ukaz. Jedn´a se tedy ” o ˇc´asteˇcnˇe automatickou metodu, kter´a je velmi obecn´a, coˇz je jej´ı v´ yhodou. Nev´ yhodou je probl´em s diagnostickou informac´ı, kter´a m˚ uˇze, ale tak´e nemus´ı b´ yt k dispozici. Pro ovˇeˇren´ı opravy byla zvolena from´aln´ı metoda – model checking. Ta umoˇzn ˇuje verifikovat syst´em dynamicky, a tedy hledat pouze chyby, kter´e mohou v syst´emu re´alnˇe nastat oproti statick´e anal´ yze, kter´ a produkuje hodnˇe false alarm˚ u. Dalˇs´ı v´ yhodou je ˇsirok´ y v´ ybˇer z exituj´ıc´ıch n´ astroj˚ u (model checker˚ u) pro verifikaci pomoc´ı model checkingu.
9
Kapitola 3
Model Checking Model checking je algoritmick´ a cesta k ovˇeˇren´ı, zda zadan´ y syst´em splˇ nuje poˇzadovanou akladn´ı sch´ema verifikaˇcn´ıho procesu je zn´azornˇen´e na obr. 3.1. Vstupem vlastnost [4]. Z´ pro verifikace je verifikovan´ y syst´em, kter´ y je typicky pops´an pomoc´ı form´aln´ıho modelu syst´emu. Druh´ ym vstupem je form´aln´ı specifikace vlastnost´ı, kter´e se maj´ı ovˇeˇrit. Model syst´emu a specifikovan´e vlastnosti vstupuj´ı do model checkeru, kter´ y ovˇeˇruje resp. verifikuje zadan´e vlastnosti. V ide´ aln´ım pˇr´ıpadˇe n´am model checker vr´at´ı odpovˇed’ ano/ne, podle toho jestli je vlastnost splnˇena. V praxi ovˇsem m˚ uˇze nastat i situace, kdy n´am model checker ’ nen´ı schopen poskytnout odpovˇed , napˇr. z d˚ uvodu nedostatku pamˇeti.
Obr´ azek 3.1: Z´ akladn´ı sch´ema procesu verifikace pomoc´ı model checkeru
Principem model checkingu je systematick´e prohled´av´an´ı stavov´eho prostoru. Stav (state) je sn´ımek syst´emu v ˇcase, zachycuje hodnoty promˇenn´ ych v dan´em ˇcasov´em okamˇziku. Z´aroveˇ n chceme zn´ at, jak se stavy mˇen´ı – popis zmˇeny mezi jednotliv´ ymi stavy (stav pˇred ud´alost´ı a stav po ud´ alosti) se naz´ yv´a pˇrechod (transition). V´ypoˇcet (computation) je sekvence stav˚ u, kde se n´ asleduj´ıc´ı stav z´ısk´a z pˇredchoz´ıho stavu pomoc´ı pˇrechodu.
10
3.1
Model syst´ emu
Re´aln´e syst´emy jsou vˇetˇsinou zad´any pomoc´ı textu programu (zdrojov´ y k´od) nebo diagramem cest. Je tedy potˇreba mechanizmus, kter´ y je schopen popsat vˇsechny typy syst´em˚ u tak, aby mohli b´ yt verifikov´ any. Jednou moˇznost´ı popisu chov´an´ı syst´emu je Kripkeho struky popisuje stavy syst´emu a jeho tura (Kripke structure) obr. 3.2(a) . Jedn´a se o graf, kter´ pˇrechody: Necht’ AP je mnoˇzina atomick´ ych v´ yrok˚ u, pak Kripkeho struktura M nad AP je ˇctveˇrice M = (S, S0 , R, L), kde • S je mnoˇzina stav˚ u, • S0 ⊆ S je mnoˇzina poˇc´ ateˇcn´ıch stav˚ u, • R ⊆ S × S je pˇrechodov´ a relace mezi stavy takov´a, ˇze ∀s ∈ S : ∃s0 ∈ S : R(s, s0 ) • L : S → 2AP je funkce pˇriˇrazuj´ıc´ı kaˇzd´emu stavu mnoˇzinu vˇsech atomick´ ych tvrzen´ı, kter´ a v dan´em stavu plat´ı, AP = {v = d | v ∈ V ∧ d ∈ D}, kde V je mnoˇzina promˇenn´ ych nad dom´enou D. Pro popis sekvenˇcn´ıho chov´ an´ı Kripkeho struktury M jsou definov´any cesty (paths). Cesta (path) v Kripkeho struktuˇre M ze stavu s je nekoneˇcn´a sekvence stav˚ u π = s0 s1 s2 ..., kter´a je ˇrazen´ a s ohledem na pˇrechodovou relaci v M . Pˇrechodov´a relace R(si , si+1 ) plat´ı pro vˇsechny 0 ≤ i < |π| − 1. Jestliˇze I(s0 ) t.j. s0 je poˇc´ateˇcn´ı stav, potom se cesta naz´ yv´ a poˇc´ateˇcn´ı (initialized). D´elka cesty (length) |π| m˚ uˇze b´ yt jak koneˇcn´a, tak nekoneˇcn´ a. Pro i < |π| je definovan´ y i-t´ y stav si v sekvenci jako π(i). Suffixem π je πi = (si , si+1 , . . . ), kter´ y zaˇc´ın´ a stavem si . Vˇsechny moˇzn´e poˇc´ateˇcn´ı cesty syst´emu, lze z Kripkeho struktury ypoˇcetn´ı strom tedy zapsat pomoc´ı v´ypoˇcetn´ıho stromu (computation tree) obr. 3.2(b). V´ vznikne rozeps´ an´ım Kripkeho struktury z poˇc´ateˇcn´ıho stavu.
Obr´ azek 3.2: Uk´ azka Kripkeho struktury (a) a v´ ypoˇcetn´ıho stromu (b)
Granularita pˇ rechod˚ u. Jedn´ım ze z´asadn´ıch nastaven´ı verifikace je urˇcen´ı granularity pˇrechod˚ u syst´emu. Tento fakt je podstatn´ y pro urˇcen´ı atomick´ ych pˇrechod˚ u, tyto 11
pˇrechody jsou d´ ale nedˇeliteln´ y. Pokud pˇrechod obsahuje v´ıce operac´ı, prov´adˇej´ı se jako jedna jedin´ a atomick´ a operace. Bˇeˇznou chybou je nastaven´ı hrub´e granularity, kdy se za atomick´e pˇrechody povaˇzuj´ı i takov´e pˇrechody, kter´e v re´aln´em syst´emu atomick´e nejsou. T´ım m˚ uˇze doj´ıt k chybˇe pˇri verifikaci, model checking neodhal´ı chyby (errors), kter´e v syst´emu jsou. Oproti tomu nastaven´ı velmi jemn´e granularity m˚ uˇze zp˚ usobit detekov´an´ı chyb, kter´e v re´aln´em bˇehu syst´emu nemohou nikdy nastat. a 2 promˇenn´e x, y a dva soubˇeˇznˇe provediteln´e pˇrechody α, β. Pˇr´ıklad z [4]: Syst´em m´ α : x := x + y β : y := y + x s poˇc´ateˇcn´ım stavem x = 1, y = 2. Oba pˇrechody maj´ı jemnou granularitu, implementace pˇrechod˚ u je pomoc´ı instrukc´ı assembleru: load, add, store, kter´e slouˇz´ı pro pr´aci s pamˇet´ı a registry: α0 : load R1 , x β0 : load R2 , y α0 : add R1 , y β0 : add R2 , x α0 : store R1 , x β0 : store R2 , y V´ ypoˇcet pˇrechodu α a pak β d´av´a v´ ysledek x = 3 ∧ y = 5. Pokud je pˇrechod β vykon´ an pˇred α obdrˇz´ıme v´ ysledek x = 4 ∧ y = 3. Na druhou stranu podle granularity implementace m˚ uˇze nastat i situace α0 β0 α1 β1 α2 β2 a v´ ysledek x = 3 ∧ y = 3. Pˇredpokl´ adejme, ˇze x = 3 ∧ y = 3 poruˇsuje vlastnosti syst´emu, d´ale pˇredpokl´adejme, ˇze syst´em je implementov´ an pro pˇrechod α a β. V tom pˇr´ıpadˇe je nemoˇzn´e z´ıskat v´ ysledek x = 3 ∧ y = 3. Potom s granularitou α0 α1 α2 β0 β1 β2 m˚ uˇzeme dostat stavy, kter´e v syst´emu nikdy nenastanou. Na druhou stranu m´ame implementaci α0 α1 α2 β0 β1 β2 , ale syst´em modelujeme s α a β, potom nikdy nenalezneme chybu v syst´emu. Syst´ emy se soubˇ eˇ znost´ı. Takov´e syst´emy se skl´adaj´ı z mnoˇziny komponent, kter´e bˇeˇz´ı souˇcasnˇe. Jednotliv´e komponenty si mezi sebou pˇred´avaj´ı r˚ uzn´a data – komunikuj´ı. Zp˚ usob komunikace je v jednotliv´ ych syst´emech r˚ uzn´ y. Komunikace m˚ uˇze prob´ıhat asynchronnˇe – v ˇcasov´em okamˇziku pracuje pouze jedna komponenta, nebo synchronnˇe – vˇsechny komponenty dˇelaj´ı krok ve stejn´em ˇcase. Komunikace prob´ıh´a za pomoci sd´ılen´ych promˇenn´ych (shared variables) nebo zas´ıl´ an´ı zpr´ av (exchanging messages). Pokud program obsahuje sd´ılen´e promˇenn´e resp. promˇenn´e, ke kter´ ym m´a pˇr´ıstup v´ıce neˇz jeden proces, je tˇreba zajistit, aby ke sd´ılen´e promˇenn´e mˇel v dan´ y ˇcasov´ y okamˇzik pˇr´ıstup pouze jeden proces. V opaˇcn´em pˇr´ıpadˇe m˚ uˇze doj´ıt k nekonzistenci dat. Pro tyto u ´ˇcely slouˇz´ı synchronizaˇcn´ı pˇr´ıkazy, kter´e jsou atomick´e a mohou m´ıt podobu pˇr´ıznaku ˇcek´an´ı (wait) nebo z´amk˚ u (lock/unlock).
3.2
Specifikace syst´ emu
Po form´ aln´ım nadefinov´ an´ı syst´emu je tˇreba tak´e form´alnˇe nadefinovat vlastnosti, kter´e se maj´ı verifikovat. Typickou formou specifikace vlastnost´ı pro model checking jsou n´asleduj´ıc´ı tempor´ aln´ı logiky:Linear-time Temporal Logic (LTL), Computation Tree Logic (CTL) a CTL∗ , kter´ a spojuje vyjadˇrovac´ı moˇznosti LTL a CTL. Tempor´ aln´ı logiky jsou speci´ aln´ım typem mod´aln´ıch logik, pomoc´ı nichˇz se daj´ı nadefinovat formule, kter´e vyajdˇruj´ı urˇcitou vlastnost syst´emu. V tempor´aln´ı logice nen´ı ˇcas uveden explicitnˇe, naopak, formule umoˇzn ˇuj´ı urˇcit, zda je nˇejak´ y stav provediteln´ y nebo tento stav nikdy nenastane (napˇr. chybov´ y stav), jedn´a se o logick´ y ˇcas. Vlastnosti typu nˇekdy (sometimes) nebo nikdy (never) jsou pops´any speci´aln´ımi tempor´aln´ımi oper´atory. Tempor´ aln´ı oper´ atory mohou b´ yt kombinov´any libovolnˇe s booleovsk´ ymi spojkami nebo 12
vz´ajemnˇe vnoˇreny. Jednotliv´e tempor´aln´ı logiky se liˇs´ı v oper´atorech, kter´e poskytuj´ı a tak´e v jejich s´emantice. Logika CTL∗ . Tato logika zahrnuje v sobˇe logiky CTL a LTL. CT L∗ formule popisuj´ı vlastnosti v´ ypoˇcetn´ıch strom˚ u. CT L∗ formule obsahuje: atomick´e v´ yroky (AP), booleovsk´e spojky (∧, ∨, ¬), kvantifik´ atory cesty, tempor´aln´ı oper´atory. Kvantifik´ atory cesty jsou pouˇzity pro popis vˇetven´ı ve v´ ypoˇcetn´ım stromu: • A pro vˇsechny cesty • E existuje cesta Tempor´ aln´ı oper´ atory popisuj´ı vlastnosti cesty (cesty pˇres strom). Existuje pˇet z´akladn´ıch tempor´ aln´ıch oper´ ator˚ u: • Xp (next time) vlastnost p bude splnˇena v n´asleduj´ıc´ım stavu dan´e cesty, • Fp (eventually) vlastnost p bude splnˇena nˇekdy na dan´e cestˇe, • Gp (globally) vlastnost p je splnˇena ve vˇsech stavech dan´e cesty, • pUq (until) vlastnost p plat´ı na cestˇe dokud neplat´ı q, • pRq (release) vlastnost q byla splnˇena ve vˇsech stavech cesty aˇz po prvn´ı stav vˇcetnˇe, ve kter´em plat´ı formule p. V CT L∗ logice existuj´ı dva typy formul´ı stavov´e formule (state formulas) a formule cesty (path formulas). Logika CTL a LTL. Jsou podlogiky CT L∗ , rozd´ıl mezi nimi je v upoˇr´ad´an´ı vˇetven´ı ve v´ ypoˇcetn´ım stromu. CTL (Computation Tree Logic) je logika s vˇetv´ıc´ım se ˇcasem a tempor´ aln´ı oper´ atory urˇcuj´ı cesty, kter´e jsou moˇzn´e z dan´eho stavu obr. 3.3(b). Oproti tomu LTL (Linear Temporal Logic) je logika s line´arn´ım ˇcasem a oper´atory urˇcuj´ı ud´alosti, kter´e mohou nastat po cestˇe ve v´ ypoˇcetn´ım stromu obr. 3.3(a).
Obr´ azek 3.3: KS, VS, CTL, LTL
13
3.3
V´ ystup verifikace
V´ ysledkem verifikace je tedy odpovˇed’ na ot´azku model checkingu: Necht’, je d´ana Kripkeho struktura M = (S, S0 , R, L), pomoc´ı kter´e je pops´an verifikovan´ y syst´em a tempor´aln´ı formule f , reprezentuj´ıc´ı poˇzadovanou vlastnost, kterou m´a syst´em splˇ novat. Odpovˇed´ı model checkingu je, zda zadan´ a formule f je splnˇena v Kripkeho struktuˇre M : M |= ϕ ?, respektive urˇcit mnoˇzinu stav˚ u syst´emu S, ve kter´ ych je formule f splnˇena: {s ∈ S | M, s |= ϕ}. Postup urˇcen´ı, zda je formule f plnˇena spoˇc´ıv´a v ovˇeˇren´ı, ˇze: • pro kaˇzdou podformuli ψ formule ϕ je vypoˇctena mnoˇzina stav˚ u: Sψ = {s ∈ S | M, s |= ψ}, • v´ ypoˇcet mnoˇziny stav˚ u Sψ zaˇc´ın´a u nejvnitˇrenjˇs´ıch (d´ale nedˇeliteln´ ych) podformul´ı a postupuje se smˇerem ven k z´ısk´an´ı mnoˇziny stav˚ u p˚ uvodn´ı formule ϕ. Typicky se prov´ ad´ı model checking z poˇc´ateˇcn´ıho stavu (stav˚ u) syst´emu, d´ıky tomu se ovˇeˇr´ı, zda je specifikace splnˇena v cel´em syst´emu (S0 ⊆ Sϕ ) nebo jeho ˇc´asti – formule je splnˇena v poˇzadovan´ ych stavech. Existuj´ı r˚ uzn´e algoritmy, pomoc´ı nichˇz se urˇcuj´ı mnoˇziny stav˚ u, ve kter´ ych je poˇzadovan´ a formule splnˇena. Nicm´enˇe pro v´ ypoˇcet mnoˇziny u r˚ uzn´ ych formul´ı, kter´e obsahuj´ı jin´e tempor´aln´ı oper´ atory je tˇreba aplikovat r˚ uzn´e algoritmy, jednotliv´e algoritmy lze naj´ıt napˇr´ıklad v [4]. Algoritmy pro ovˇeˇren´ı formule jsou zaloˇzeny na proch´azen´ı stavov´ ym prostorem a jejich hlavn´ım probl´em se tedy st´ av´ a exploze stavov´eho prostoru.
3.4
Probl´ em stavov´ e exploze
Exploze stavov´eho prostoru je kritick´ ym probl´emem model checkingu (state space explosion problem), kde verifikace spoˇc´ıv´a v generov´an´ı stavov´eho prostoru. Velikost stavov´eho prostoru roste exponenci´ alnˇe s velikost´ı verifikovan´eho modelu resp. syst´emu [21]. Z toho d˚ uvodu je prakticky model checking bez redukce stavov´eho prostoru v praxi nepouˇziteln´ y. Exploze stavov´eho prostoru spoˇc´ıv´a v nedeterminismu – ve velk´em mnoˇzstv´ı moˇznost´ı stav˚ u, kter´ ymi m˚ uˇze syst´em pokraˇcovat z aktu´aln´ıho stavu. Pro ˇreˇsen´ı probl´emu stavov´e exploze existuj´ı r˚ uzn´e pˇr´ıstupy [7, 15, 21, 23]. Jedn´ım z moˇzn´ ych dˇelen´ı tˇechto pˇr´ıstup˚ u je n´asleduj´ıc´ı: • Pˇ redzpracov´ an´ı (preprocessing). Jeˇstˇe pˇred zaˇc´atkem prov´adˇen´ı model checkingu se vykon´ a pˇredzpracov´ an´ı verifikovan´eho syst´emu. Do t´eto skupiny patˇr´ı: slicing a jemu podobn´e techniky zaloˇzen´e na statick´e anal´yze, jejich podstatou je oˇr´ıznut´ı“ ve” rifikovan´eho syst´emu pouze na tu ˇc´ast, kter´a m˚ uˇze ovlivnit verifikovanou vlastnost. Vlastn´ı model checking se prov´ad´ı pouze nad oˇr´ıznutou“ ˇc´ast´ı syst´emu. Dalˇs´ı meto” dou je nad aproximace, pomoc´ı n´ı je moˇzn´e zjistit, co ovlivˇ nuje zkoumanou oblast a d´ ale pracovat se zvolenou ˇc´ast´ı syst´emu. D´ale je moˇzn´e pouˇz´ıt explicitn´ı urˇcen´ı atomick´e sekce. Uˇzivatel s´ am zad´a oblasti, kter´e maj´ı b´ yt vykon´any atomicky a nem´a se rozgenerov´ avat jejich stavov´ y prostor. V tom pˇr´ıpadˇe s´am uˇzivatel zaruˇcuje, ˇze j´ım zadan´ a atomick´ a sekce nezp˚ usob´ı nenalezen´ı chyby. Existuj´ı i metody, kter´e dok´ aˇz´ı urˇcit atomick´e sekce automaticky. Tyto sekce jsou ovˇsem vˇetˇsinou velice jednoduch´e a 14
neefektivn´ı vzhledem k redukci stavov´eho prostoru. Dalˇs´ı moˇznost´ı je abstrakce (abstraction). Abstrakce se m˚ uˇze vytvoˇrit bud’ ruˇcnˇe (theorem proving, uˇzivatel) nebo automaticky (predik´ atov´ a abstrakce, petriho s´ıtˇe). • Efektivn´ı uloˇ zen´ı Kripkeho struktury v pamˇ eti. Dalˇs´ı moˇznost´ı jak se vypoˇr´adat se stavovou exploz´ı je komprimace stavov´eho prostoru. BDD (binary decision diagram) je jednou z moˇznost´ı jak komprimovat stavov´ y prostor, jednotliv´e stavy jsou reprezentov´ any pomoc´ı formul´ı. Dalˇs´ı moˇznost´ı je efektivn´ı uloˇzen´ı stavu v pamˇeti, neukl´adaj´ı se cel´e novˇe generovan´e stavy, ale pouze zmˇeny mezi jiˇz uloˇzen´ ym stavem a novˇe generovan´ ym. Abstrakce stav˚ u je metoda, kter´a redukuje informace o procesech. Neuchov´ av´ a se informace o pˇresn´em poˇctu proces˚ u, ale pouze informace zda na dan´em ˇr´ adku k´ odu je 0, 1 nebo ∞ proces˚ u, jedn´a se o nadaproximaci. • Redukce stavov´ eho prostoru. Redukce stavov´eho prostoru neznamen´a pouze efektivn´ı proch´ azen´ı stavov´eho prostoru, ale tak´e redukce poˇctu stav˚ u. Redukce stav˚ u m˚ uˇze prob´ıhat bud’ pˇredem nebo za bˇehu programu – nˇekter´e generovan´e stavy nejsou z hlediska verifikovan´e vlastnosti zaj´ımav´e. Metody pro redukci stavov´eho prostoru jsou: symmetry reduction, Petri-net unifolding (rozvinut´ı petriho s´ıtˇe do line´arn´ıho stromu). Zaj´ımav´e redukce pro programy se soubˇeˇznost´ı jsou Partial order reduction“ (POR) ” a on-the-fly model checking“. POR je zaloˇzen´a na redukov´an´ı generov´an´ı stavov´eho ” prostoru. V programech existuj´ı nez´avisl´e pˇrechody u kter´ ych nez´aleˇz´ı na poˇrad´ı jejich vykon´ an´ı, po jejich proveden´ı se verifikace dost´av´a do shodn´eho stavu. Takov´e pˇrechody (operace) se typicky vyskytuj´ı u v´ıce vl´aknov´ ych aplikac´ı, kdy r˚ uzn´a v´alkna prov´ ad´ı na sobˇe nez´ avisl´e operace a nez´aleˇz´ı tedy na poˇrad´ı jejich prov´adˇen´ı. Uk´azka ˇc´ asti vygenerovan´eho stavov´eho prostoru, kde je moˇzn´e tuto generovanou ˇc´ast redukovat pouze na proveden´ı jednoho pr˚ uchodu je na obr. 3.4.
Obr´ azek 3.4: Uk´ azka redukce stavov´eho prostoru pomoc´ı POR Metoda on-the-fly je zaloˇzena na souˇcasn´em generov´an´ı stavov´eho prostoru a ovˇeˇrov´ an´ı vlastnosti syst´emu najednou. Pˇri generov´an´ı stavov´eho prostoru se souˇcasnˇe verifikuje, zda je vlastnost v dan´em generovan´em stavu splnˇena. Pokud dojde k nalezen´ı protipˇr´ıkladu verifikovan´e vlastnosti, generov´an´ı stavov´eho prostoru konˇc´ı. Verifikace dospˇela k z´ avˇeru bez nutnosti rozgenerov´av´avat cel´ y stavov´ y prostor a t´ım k jeho redukci.
15
• Kompoziˇ cn´ı model checking (Compositional of MC). Jedn´a se o rozdˇelen´ı syst´emu na komponenty, kde u kaˇzd´e komponenty sledujeme urˇcit´e vlastnosti. Nakonec z tˇechto d´ılˇc´ıch vlastnost´ı komponent odvod´ı vlastnosti cel´eho syst´emu. Existuj´ı i dalˇs´ı metody pro redukci stavov´eho prostoru, kter´e zde nejsou uvedeny. Tak´e je moˇzn´e jednotliv´e metody vhodn´ ym zp˚ usobem kombinovat, a t´ım doc´ılit vyˇsˇs´ı efektivnosti pˇri redukci stavov´eho prostoru.
3.5
Bounded Model Checking
Bounded model checking resp. ohraniˇcen´ y model checking se pouˇz´ıv´a pro verifikaci koneˇcnˇe stavov´ ych syst´em˚ u. Bounded model checking m˚ uˇze u ´ˇcinnˇe redukovat probl´em splnitelnosti booleovsk´e formule – SAT . Tento probl´em byl jedn´ım z d˚ uvod˚ u pro vytvoˇren´ı t´eto metody [3]. Z´akladn´ı myˇslenkou bounded model checkingu je ovˇeˇren´ı urˇcit´e vlastnosti syst´emu pouze za pomoci koneˇcn´eho prefixu cesty v syst´emu. Nalezen´ı d˚ ukazu o splnˇen´ı nebo vyvr´acen´ı urˇcit´e vlastnosti syst´emu se prov´ad´ı v koneˇcn´em poˇctu krok˚ u. Prohled´av´an´ı stavov´eho syst´emu je omezeno na pˇredem danou d´elku k. Pomoc´ı omezen´ı prohled´av´an´ı stavov´eho syst´emu se omez´ı i verifikace poˇzadovan´e vlastnosti. Verifikace je omezena na verifikaci prefixu cesty, kter´ a m´ a d´elku k. V praxi se vˇetˇsinou omezen´a d´elka cesty prodluˇzuje na takovou dobu, dokud se nez´ısk´ a d˚ ukaz o splnˇen´ı/vyvr´acen´ı verifikovan´e vlastnosti. Pˇrestoˇze prefix cesty je koneˇcn´ y – obsahuje koneˇcn´ y poˇcet stav˚ u, m˚ uˇze reprezentovat nekoneˇcnou cestu. Pokud cesta obsahuje zpˇetnou smyˇcku (back loop) z posledn´ıho stavu prefixu do nˇekter´eho z pˇredchoz´ıch stav˚ u (obr. 3.5(b)) jedn´a se o reprezentaci nekoneˇcn´e cesty pomoc´ı koneˇcn´eho poˇctu stav˚ u. V pˇr´ıpadˇe, ˇze prefix cesty neobsahuje zpˇetnou smyˇcku (obr. 3.5(a)), nelze ˇr´ıci nic o nekoneˇcn´em chov´an´ı syst´emu. Nelze zverifikovat vlastnosti, kter´e poˇzaduj´ı, aby urˇcit´ a vlastnost byla platn´a nekonˇcnˇe dlouho. Pokud prefix neobsahuje zpˇetnou smyˇcku nen´ı zn´ am´e chov´an´ı syst´emu za stavem sk .
Obr´ azek 3.5: Dvˇe moˇznosti omezen´e cesty Definice pro cestu, kter´ a obsahuje zpˇetnou smyˇcku je n´asleduj´ıc´ı: Pro l ≤ k naz´ yv´ ame cestu π: (k, l)-loop, pokud T (π(k), π(l)) a π = u.v ω , kde u = (π(0), . . . , π(l − 1)) a v = (π(l), . . . , π(k)). Pokud existuje k≥l≥0, pro kter´e je cesta π: (k, l)-loop, pak naz´ yv´ ame cestu π: k-loop. Pokud na cestˇe d´elky k existuje pˇrechod z posledn´ıho stavu cesty sk do nˇekter´eho z pˇredeˇsl´ ych stav˚ u cesty sl , pak je moˇzn´e danou ˇc´ast cesty neomezenˇe kr´at opakovat k-loop. S´emantika model checkingu na limitovan´ ych cest´ach se naz´ yv´a bounded semantics. Vyuˇz´ıv´a se prvn´ıch k + 1 stav˚ u cesty (s0 , . . . , sk ), jedn´a se o koneˇcn´ y prefix cesty. Pomoc´ı tohoto prefixu se urˇcuje splnitelnost formule na cestˇe. Pokud cesta obsahuje smyˇcku k-loop, m˚ uˇze se pro splnitelnost formule pouˇz´ıt origin´aln´ı s´emantika model checkingu. Tato s´emantika lze vyuˇz´ıt vzhledem k faktu, ˇze pokud cesta obsahuje zpˇetnou smyˇcku jsou nekoneˇcn´e vlastnosti 16
cesty obsaˇzeny v jej´ım koneˇcn´em prefixu. Form´alnˇe lze toto tvrzen´ı Bounded Semantics ” for a Loop“ zapsat n´ asledovnˇe: Necht’ k ≥ 0 a π je k-loop. Potom LT L formule f je splnˇena na cestˇe π d´elky k (symbolick´ y z´ apis π |=k f iff π |= f ). Druh´ a moˇznost nast´ av´ a v pˇr´ıpadˇe, kdy cesta π neobsahuje k-loop. Potom formule f = Fp je splnˇena na cestˇe π v origin´ aln´ı (neomezen´e ) s´emantice, jestliˇze existuje index i ≥ 0, takov´ y, kde p je splnˇena na sufixu (πi ) cesty π. Pokud je pouˇzita omezen´ a s´emantika, potom k+1-n´ı stav π(k) nem´ a n´ asledovn´ıka a nen´ı tedy moˇzn´e tuto s´emantiku definovat rekurzivnˇe pomoc´ı sufix˚ u cesty (πi ). Z toho d˚ uvodu se zav´ad´ı znaˇcen´ı π |=ik f , kde i je aktu´aln´ı pozice v prefixu na cestˇe π a suffix πi cesty π splˇ nuje formuli f : π |=ik f implikuje πi |= f . Form´ aln´ı definice tohoto tvrzen´ı Bounded Semantics without a Loop“ lze zapsat ” n´asledovnˇe: Necht’ k ≥ 0, cesta π nen´ı k-loop. Potom LT L formule f je splnˇena na cestˇe π d´elky k resp. π |=k f iff π |=0k f , kde π π π π π π π π π
|=ik |=ik |=ik |=ik |=ik |=ik |=ik |=ik |=ik
p ¬p f ∧g f ∨g Gf Ff Xf f Ug f Rg
iff p ∈ L(π(i)) iff p∈ / L(π(i)) iff π |=ik f and π |=ik g iff π |=ik f or π |=ik g nen´ı splnˇena nikdy iff ∃j, i ≤ j ≤ k. π |=jk f iff i < k and π |=i+1 f k iff ∃j, i ≤ j ≤ k. π |=jk g and ∀n, i ≤ n < j. π |=nk f iff ∃j, i ≤ j ≤ k. π |=jk f and ∀n, i ≤ n < j. π |=nk g
Na z´ avˇer t´eto kapitoly o bounded model checkingu zle uv´est n´asleduj´ıc´ı dvˇe vˇety: Necht’ f je LT L formule a π je cesta, potom π |=k f ⇒ π |= f . Necht’ f je LT L formule a M je Kripkeho struktura. Jestliˇze M |= Ef , potom existuje k ≥ 0, kde M |=k Ef . Z tˇechto dvou vˇet lze odvodit n´asleduj´ıc´ı theor´em o bounded model checkingu: Necht’ f je LT L formule a M je Kripkeho struktura, potom M |= Ef iff existuje k ≥ 0, resp. M |=k Ef . Theor´em ˇr´ık´ a, pokud zle z´ıskat takovou d´elku k, na kter´e je formule splnˇena, potom omezen´ a a neomezen´ a s´emantika jsou ekvivalentn´ı.
3.6
Navigace stavov´ ym prostorem
V projektu SHADOWS se bounded model checking vyuˇz´ıv´a pro zverifikov´an´ı okol´ı l´eˇcen´e chyby, nen´ı tedy c´ılem prov´est bounded model checking z poˇc´ateˇcn´ıho stavu (s0 ), ale z nˇejak´eho konkr´etn´ıho stavu ve stavov´em prostoru syst´emu. Aby bylo moˇzn´e z toho stavu prov´est bounded model checking, je potˇreba nejprve dan´eho stavu dos´ahnout, proj´ıt stavov´ y prostor do konkr´etn´ıho stavu. K tomuto u ´ˇcelu existuj´ı r˚ uzn´e metody [14, 20], kter´e slouˇz´ı k navigaci stavov´ ym prostorem do poˇzadovan´eho stavu. Tyto metody mohou b´ yt n´asleduj´ıc´ı. • Record&Replay trace. Tato strategie pro navigaci stavov´ ym prostorem je zaloˇzena na zaznamen´ an´ı bˇehu programu (trace) a posl´eze pˇrehr´an´ı t´eto cesty ve zvolen´em 17
model checkeru. Pomoc´ı z´ aznamu bˇehu programu se je moˇzn´e nav´adˇet stavov´ ym prostorem aˇz do m´ısta opravy chyby, ze kter´eho je moˇzn´e spustit bounded model checking. V´ yhodou t´eto metody je zaznamen´an´ı cel´e cesty prov´adˇen´ı programu. D´ıky tomu je moˇzn´e prov´est bounded model checking ne pouze z chybov´eho stavu programu, ale z kter´ehokoliv stavu, kter´ y mu na cestˇe pˇredch´az´ı. Z´asadn´ı nev´ yhodou t´eto metody je nutnost ukl´ ad´an´ı cel´eho bˇehu programu, a t´ım zpomalen´ı chodu aplikace. Dalˇs´ı nev´ yhodou je pamˇet’ov´a n´aroˇcnost, pro z´aznam cesty programu je zaˇ ım delˇs´ı dobu program bˇeˇz´ı, t´ım je potˇreba v´ıce pamˇeti potˇreb´ı velk´e mnoˇzstv´ı dat. C´ pro z´ aznam cesty. Minim´ alnˇe stejnˇe dlouh´a doba jako pro z´aznam cesty je tak´e potˇreba pro pˇrehr´ an´ı zaznamenan´e cesty. Proto se tato metoda nehod´ı pro navigaci stavov´ ym prostorem u syst´em˚ u, kter´e jsou dlouhodobˇe v chodu. Aby bylo moˇzn´e pˇrehr´ at zaznamenanou cestu bˇehu programu, je tˇreba ukl´adat relevantn´ı informace jako informace o aktu´aln´ım vl´aknˇe, vykonan´e byte-code instrukci atd. • Store&Restore state. Dalˇs´ı strategie pro z´ısk´an´ı poˇzadovan´eho stavu ze stavov´eho prostoru syst´emu je zaloˇzena na uloˇzen´ı a opˇetovn´em obnoven´ı stavu. Neprve se uloˇz´ı aktu´ aln´ı stav bˇeˇz´ıc´ıho programu a n´aslednˇe se uloˇzen´ y stav obnov´ı ve zvolen´em model checkeru. Po obnoven´ı uloˇzen´eho stavu je z nˇej moˇzn´e prov´est bounded model checking. Nev´ yhodou t´eto metody je nemoˇznost zaˇc´ıt bounded model checking z jin´eho neˇz z pouze uloˇzen´eho stavu. Nen´ı moˇzn´e jako u pˇredeˇsl´e metody zah´ajit bounded model checking z nˇejak´eho z pˇredch´azej´ıc´ıch stav˚ u bˇehu programu. Dalˇs´ı nev´ yhodou je slabost v ukl´ ad´ an´ı stavu. Pokud dojde ke zmˇenˇe v uloˇzen´em stavu je tˇreba prov´est pˇr´ısluˇsnou zmˇenu i v ukl´ adan´em resp. obnoven´em stavu. Napˇr. u Java program˚ u m˚ uˇze doj´ıt ke zmˇenˇe verze Java virt´aln´ıho stroje (JVM) nebo zmˇena verze model checkeru m˚ uˇze zp˚ usobit tak´e nutnost zmˇeny v ukl´ad´an´ı a obnoven´ı stavu. Nev´ yhoda moˇznosti verifikace pouze z uloˇzen´eho stavu se d´a ˇc´asteˇcnˇe odstranit opˇetovn´ ym ukl´ad´an´ım stav˚ u syst´emu napˇr. po urˇcit´em ˇcasov´em intervalu. Nicm´enˇe st´ale tu z˚ ust´av´a nutnost uloˇzen´ı veˇsker´ ych potˇrebn´ ych informac´ı pro obnoven´ı stavu syst´emu v model checkeru. Tˇechto informac´ı je znaˇcn´a spousta a jak jiˇz bylo zm´ınˇeno, s kaˇzdou zmˇenou verze m˚ uˇze doj´ıt k nutnosti zmˇenˇe ukl´adan´ ych informac´ı. Naopak v´ yhodou je fakt, ˇze nezp˚ usobuje trval´e zpomalen´ı bˇehu programu, ke zpomalen´ı doch´az´ı pouze v dobˇe ukl´ ad´ an´ı stavu. • Dalˇ s´ı Strategie. V´ yˇse uveden´e strategie se daj´ı r˚ uznˇe kombinovat, napˇr. po urˇcit´em ˇcasov´em intervalu m˚ uˇze doch´azek k ukl´ad´an´ı stavu syst´emu a zaznamen´av´an´ı cesty z tohoto stavu. Po urˇcit´e dobˇe dojde k pˇremaz´an´ı uloˇzen´e cesty a stavu nov´ ymi informacemi. Dalˇs´ı moˇznost´ı je modifikace uveden´ ych strategi´ı, jako napˇr´ıklad Record&Replay trace lze kombinovat s oˇrez´ av´ an´ım (slicing)“. Jedn´a se o metodu, pomoc´ı kter´e se ne” ukl´ adaj´ı vˇsechny informace o bˇehu programu, ale pouze ty informace, kter´e jsou relevantn´ı k pˇrehr´ an´ı bˇehu programu do poˇzadovan´eho stavu.
18
Kapitola 4
Java PathFinder Projekt SHADOWS se vˇenuje l´eˇcen´ı program˚ u napsan´ ych v jazyce Java, a proto bylo vyb´ır´ano z model checker˚ u vhodn´ ych pro verifikaci Java program˚ u. Byly zkoum´any vlastnosti tˇechto tˇr´ı zn´ am´ ych a zaj´ımav´ ych model checker˚ u. • Bogor [10] je softwarov´ y model checking framework, kter´ y poskytuje vizualizaci, grafick´e uˇzivatelsk´e rozhran´ı, a tak´e r˚ uzn´e algoritmy po model checking (pro redukci stavov´eho prostoru, vyhled´ avac´ı heuristiky, abstraktn´ı definice atd.). Bogor lze pouˇz´ıt i jako plugin do Eclipse. (Eclipse je integrovan´e v´ yvojov´e prostˇred´ı pro programov´ an´ı Java program˚ u, jeho n´ avrh umoˇznuje rozˇs´ıˇren´ı prostˇred´ı pomoc´ı plugin˚ u [2].) Jedn´ım z moˇzn´ ych vyuˇzit´ı Bogoru, je pro studijn´ı u ´ˇcely. Je moˇzn´e ho vyuˇz´ıt pro v´ yuku z´ akladn´ıch algoritm˚ u model checkingu a jeho podstaty. Z´aroveˇ n lze Bogor vyuˇz´ıt pro klasick´ y model checking. • Bandera [8] je model checker pro programy napsan´e v Javˇe, kter´e obsahuj´ı paralelismus. Bandera pˇrekl´ ad´ a zdrojov´ y k´od v Jave do vstupn´ıho jazyka nˇejak´eho jin´eho existuj´ıc´ıho model checkeru jako napˇr´ıklad SPIN, SMV, SAL, atd. Tyto jin´e model checkery zabezpeˇcuj´ı vlastn´ı verifikaci syst´emu. Po zverifikov´an´ı syst´emu Bandera umoˇzn ˇuje namapovat v´ ystup verifikace ze zvolen´eho model checkeru na p˚ uvodn´ı Java k´ od. • Java PathFinder(JPF) [9] je model checker, kter´ y prov´ad´ı verifikaci nad Java byte-codem. JPF je implementov´an jako speci´aln´ı Java virtu´aln´ı stroj (JVM), kter´ y v sobˇe pˇrehr´ av´ a programy urˇcen´e k verifikaci. Bˇehem pˇrehr´av´an´ı programu kontroluje poˇzadovan´e vlastnosti nebo specifikace syst´emu. JPF je implicitnˇe nastaven na detekci deadlocks, unhandled exception, violations of assertions. Z´aroveˇ n JPF m˚ uˇze detekovat i dalˇs´ı vlastnosti syst´emu, kter´e se daj´ı zadat pomoc´ı parametr˚ u. Nebo je moˇzn´e naimplementovat dalˇs´ı vlastn´ı speci´aln´ı souˇc´asti JPF pro verifikaci poˇzadovan´ ych vlastnost´ı syst´emu. Pro vlastn´ı implementaci bounded model checkingu byl zvolen model checker Java PathFinder pro jeho snadnou rozˇsiˇritelnost o dalˇs´ı moduly a funkce. Java PathFinder obsahuje ˇradu vyhled´ avac´ıch strategi´ı (search strategies), redukce stavov´eho prostoru, r˚ uzn´e heuristiky pro prohled´ av´ an´ı stavov´eho prostoru atd. Model checker Bogor je tak´e moˇzn´e rozˇs´ıˇrit o vlastn´ı moduly, nicm´enˇe v´ yhodou JPF je jeho nasazen´ı jiˇz na re´aln´e syst´emy. Hlavn´ı nev´ yhodu model checkeru Bandera je nutnost transformovat vstupn´ı zdrojov´ y k´odu programu do jin´eho jazyka. T´ım je zp˚ usobena nemoˇznost selod´av´an´ı pr˚ ubˇehu verifikace nad p˚ uvodn´ım Java k´ odem. 19
4.1
Z´ akladn´ı charakterisitika
Java PathFinder je explicitn´ı stavov´ y model checker pro programy napsan´e v jazyce Java [9, 13, 17, 19, 22]. Verifikace se prov´ad´ı na u ´rovni Java byte-codu. JPF pˇredstavuje speci´aln´ı virtu´aln´ı stroj, ve kter´e se spouˇst´ı verifikovan´ y syst´em. Z d˚ uvodu bˇehu aplikace pˇr´ımo v JPF, nen´ı nutn´e spouˇstˇet program v´ıcekr´at nebo ho nˇejak´ ym zp˚ usobem upravovat. JPF neprov´ ad´ı jednoduch´ y bˇeh programu, ale vykon´av´a rovnou verifikaci za bˇehu (runtime). Prohled´ av´ an´ı stavov´eho prostoru prob´ıh´a pomoc´ı r˚ uzn´ ych prohled´avac´ıch strategi´ı, kter´e budou pops´ any d´ ale. Samotn´ y Java PathFinder je tak´e naps´an v jazyce Java, jeho architektura je rozdˇelena do modul˚ u, kter´e umoˇzn ˇuj´ı dalˇs´ı rozˇsiˇritelnost. Je moˇzn´e rozˇsiˇrovat jiˇz existuj´ıc´ı moduly o dalˇs´ı funkce nebo implementovat nov´e moduly. Pokud JPF bˇehem verifikace nalezne chybu (error), standardnˇe vyp´ıˇse cestu (trace), kter´a k chybˇe vedla, a tak´e vyp´ıˇse relevantn´ı informace o bˇehu (aktu´aln´ı vl´akno, jednotliv´e ˇr´adky zdrojov´eho k´odu, apod), tyto informace mohou pomoci opravit nalezenou chybu. Z´akladn´ı architektura Java PathFinderu je vyobrazena na obr. 4.1.
Obr´ azek 4.1: Architektura Java PathFinderu [9]
Vstupem JPF je Java byte-code program, kter´ y je urˇcen k verifikaci. Na bˇeh JPF jsou pˇrilinkov´ any r˚ uzn´e moduly, kter´e definuj´ı jak´ ym zp˚ usobem bude verifikace prob´ıhat. Pomoc´ı nastaven´ı JPF se urˇc´ı, jak´a vyhled´avac´ı strategie (search strategy) bude pouˇzita pro prohled´ av´ an´ı stavov´eho prostoru, kter´e listenery (search listener) budou s touto strategi´ı pouˇzity (pro z´ısk´ an´ı poˇzadovan´ ych informac´ı). D´ale lze nastavit generov´an´ı moˇznost´ı (choice generator) nedeterminismu, jedn´a se o hodnoty vstupn´ıch dat, prokl´ad´an´ı vl´ aken atd. Dalˇs´ı nastaven´ı umoˇznuje pˇrilinkovat listener zaloˇzen´ y na sledov´an´ı jednotliv´ ych krok˚ u virtu´aln´ıho stroje. JPF tedy systematicky, podle zvolen´e strategie, prohled´av´a stavov´ y prostor vstupn´ıho programu, pokud dojde k detekci chyby. JPF uˇzivateli poskytne zpr´avu o verifikaci, kter´ a obsahuje cestu, kter´a vedla k chybˇe, typ detekovan´eho probl´emu a dalˇs´ı informace, kter´e byly nastaveny uˇzivatelem.
20
JPF umoˇzn ˇuje verifikovat programy, kter´e maj´ı v´ıce vl´aken, nicm´enˇe neumoˇzn ˇuje verifikaci soubˇeˇzn´eho bˇehu vl´ aken (na dvou procesorech). JPF pouze simuluje soubˇeˇznost vl´aken. Z´aroveˇ n neumoˇzn ˇuje zverifikovat programy, kter´e obsahuj´ı nativn´ı metody (metody psan´e v jin´em jazyce neˇz Java). JPF neobsahuje podporu vˇsech knihoven Java, pokud program obsahuje urˇcit´e knihovny, nen´ı ho moˇzn´e verifikovat [9]. Nicm´enˇe umoˇzn ˇuje vytvoˇren´ı nativn´ıch metod, kter´e jsou v r´amci verifikace br´any jako atomick´e ˇc´ asti k´ odu a neprov´ ad´ı se nad nimi verifikace. Metoda je vykon´ana bez prokl´ad´ an´ı jin´ ymi instrukcemi k´ odu. D´ıky tomuto mechanizmu je moˇzn´e verifikovat programy obsahuj´ıc´ı knihovny nebo metody, kter´e nechceme br´at v u ´vahu do verifikace. Pro verifikaci vstupn´ıch dat obsahuje JPF specializovan´e API, pomoc´ı kter´eho lze urˇcit, jak´ ych hodnot mohou tyto data nab´ yvat. Jinou moˇznost´ı je volba pro n´ahodn´ y v´ ybˇer hodnot vstupn´ıch dat. Nast´ınˇen´e vlastnosti JPF budou d´ale rozeps´any. JPF m˚ uˇze simulovat nedeterminismus, pro generov´ an´ı nedeterminismu obsahuje JPF dva mechanismy: • Backtracking znamen´ a, ˇze se JPF m˚ uˇze vr´atit k vykonan´emu stavu a nahradit zvolenou moˇznost (hodnotu promˇenn´e), z kter´e vznikl nedeterminismus, jinou moˇznost´ı a t´ım vygenerovat nov´ y stav a n´aslednˇe generovat cestu. Tento zp˚ usob se aplikuje na postupn´e rozgenerov´ an´ı vˇsech moˇzn´ ych pl´anovac´ıch sekvenc´ı (moˇzn´ ych hodnot). • State matching je zaloˇzen na mechanismu vyhnut´ı se generov´an´ı jednoho stavu syst´emu dvakr´ at, kaˇzd´ y nov´ y stav je uloˇzen na heap. Pokud je dan´ y stav uloˇzen, neukl´ ad´ a se jiˇz vygenerovan´ y stav, ale JPF se vrac´ı k prvn´ımu nerozgenerovan´emu stavu a zde se pokraˇcuje s verifikac´ı.
4.2
Specifikace
JPF umoˇzn ˇuje verifikovat r˚ uzn´e vlastnosti podle zadan´ ych poˇzadavk˚ u. V JPF existuj´ı tˇri z´akladn´ı mechanizmy pro nastaven´ı vlastnost´ı: ordinary assertions, gov.nasa.jpf.Property a listenery (gov.nasa.jpf.SearchListner nebo gov.nasa.jpf.VMListener). Java assertions se zad´ avaj´ı pˇr´ımo do zdrojov´eho k´odu programu a slouˇz´ı k z´ısk´ an´ı informac´ı z´ avisl´ ych pˇr´ımo na datech aplikace. Jedn´a se o u ´ˇcinn´e z´ısk´an´ı informac´ı a chov´ an´ı syst´emu. Nev´ yhodou t´eto metody je nutnost z´asahu do zdrojov´eho k´odu programu. Z´aroveˇ n m˚ uˇze doj´ıt k n´ ar˚ ustu stavov´eho prostoru, pokud se maj´ı zverifikovat i pˇridan´e assertions. Gov.nasa.jpf.Property je mechanismem zapouzdˇruj´ıc´ım kontrolu vlastnost´ı (properties). Verifikace tˇechto vlastnost´ı m˚ uˇze b´ yt nastavena staticky pomoc´ı search.properties nebo dynamicky pomoc´ı jpf.getSerach().addProperty(). Potom je moˇzn´e tyto vlastnosti kontrolovat za bˇehu programu pˇri kaˇzd´e zmˇenˇe pomoc´ı search objektu. Z´akladn´ı specifikace, kter´e jsou implicitnˇe v JPF pomoc´ı tohoto mechanizmu kontrolov´any jsou n´asleduj´ıc´ı: deadlocks, assertion violation, uncaught exceptions. Kontrola tˇechto specifikac´ı je jiˇz v JPF naiplementov´ ana. Listenery – gov.nasa.jpf.SearchListener a gov.nasa.jpf.VMListener jsou dalˇs´ım mechanismem, kter´ y lze vyuˇz´ıt pro ovˇeˇren´ı komplexnˇejˇs´ıch informac´ı. Jedn´a se o dvˇe tˇr´ıdy, pomoc´ı kter´ ych jsou naimplementov´any r˚ uzn´e listnery. Ty slouˇz´ı k z´ısk´av´an´ı r˚ uzn´ ych informac´ı o bˇehu programu. V JPF je jiˇz ˇrada tˇechto listener˚ u naimplementov´ana. Jednotliv´e listenery d´ avaj´ı napˇr´ıklad n´asleduj´ıc´ı inforamce: SearchMonitor – v´ ypis statistick´ y informac´ı o bˇehu programu (poˇcet vygenerovan´ ych stav˚ u, velikost vyuˇzit´e pamˇeti, atd.),
21
HeapTracker – v´ ypis vyuˇzit´ı haldy (heap) na vˇsech cest´ach verifikace, StateSpaceDot – vytvoˇr´ı graf vygenerovan´eho stavov´eho prostoru bˇehem verifikace, MethodTracker – v´ ypis vˇsech metod, kter´e byly bˇehem verifikace vol´any, atd. Mechanizmus listener˚ u umoˇznuje z´ısk´av´at informace o programu na tˇrech u ´rovn´ıch. Obecn´e listenery poskytuj´ı informace o programu z´ıskan´e pomoc´ı rozhran´ı, nach´azej´ı se mimo program. Jedn´ a se o SearchListnery a VMListenery. Druh´ ym typem listener˚ u jsou specializovan´e vyhled´ avac´ı listenery, ty se opˇet nach´az´ı mimo program a jsou k nˇemu pouze linkov´ any. Nicm´enˇe jsou navrˇzeny pro z´ısk´an´ı specifick´ ych informac´ı o programu, nebo jsou navrˇzeny ke konkr´etn´ımu u ´ˇcelu, napˇr. gov.nasa.jpf.search.heuristic.BFSHeuristic slouˇz´ı pro nastaven´ı prohled´ av´ an´ı stavov´eho prostoru pomoc´ı BFS strategie. Tˇret´ım typem listener˚ u jsou vnitˇrn´ı listenery, kter´e se nach´az´ı v konkr´etn´ım bal´ıku uvnitˇr implementace JPF a umoˇznuj´ı z´ısk´ avat inforamce z dan´eho konkr´etn´ıho bal´ıˇcku. Napˇr. bal´ık gov.nasa.jpf.jvm.bytecode obsahuje jednotliv´e instrukce byte-codu a tedy listener v tomto bal´ıku umoˇznuje z´ıskat nebo mˇenit prim´arn´ı informace o jednotliv´ ych instrukc´ıch bytecodu, kter´e jsou ostatn´ım listener˚ um skryty. Nejˇsirˇs´ı vyuˇzit´ı nab´ızej´ı obecn´e listenery, kter´e umoˇznuj´ı z´ıskat nebo mˇenit informace v programu bezpeˇcn´ ym“ zp˚ usobem. ” SearchListenery lze pouˇz´ıt pro monitorov´an´ı prohled´avac´ıho procesu stavov´ ym prostorem. Umoˇznuj´ı zaznamen´ avat napˇr´ıklad informace o jednotliv´ ych stavech syst´emu nebo vytv´aˇret graf stavov´eho prostoru, kter´ y obsahuje inforamce o postupu stavov´ ym prostorem i z´akladn´ı informace o jednotliv´ ych stavech. VMListenery mohou zaznamen´avat nebo mˇenit jednotliv´e kroky prov´adˇen´ı programu na u ´rovni virtu´ aln´ıho stroje. VMListener zle napˇr´ıklad pouˇz´ıt pro monitorov´an´ı vykon´ an´ı byte-code instrukc´ı MONITORENTER a MONITOREXIT, kter´e slouˇz´ı k synchronizaci v programu. Monitorov´ an´ı tˇechto instrukc´ı umoˇznuje odhalit chybˇej´ıc´ı synchronizaci nebo naopak detekovat m´ısto vzniku deadlocku. Pˇrilinkov´ an´ı listener˚ u k bˇehu JPF lze prov´est dvˇema zp˚ usoby. Prvn´ım zp˚ usobem je statick´e nastaven´ı vlastnost´ı JPF pˇred jeho spuˇstˇen´ım. Tento mechanizmus umoˇznuje zvolit jednotliv´e listnery, kter´e maj´ı b´ yt pˇrilinkov´any a tak´e nastavit parametry pˇrid´avan´ ych listener˚ u. Druhou moˇznost´ı je dynamick´e pˇrid´an´ı listener˚ u do bˇehu JPF, lisntener je pˇrid´ an pˇr´ımo do zdrojov´eho k´ odu aplikace a vyvol´an aˇz za bˇehu.
4.3
Prohled´ av´ an´ı stavov´ eho prostoru
JPF obsahuje r˚ uzn´e nastaviteln´e vyhled´avac´ı strategie (Search strategies) pro prohled´av´ an´ı stavov´eho prostoru verifikovan´eho syst´emu. Naimplementov´any jsou z´akladn´ı vyhled´avac´ı strategie jako DF S (Depth First Search – prohled´av´an´ı do hloubky), BF S (Breadth First Search – prohled´ av´ an´ı do ˇs´ırky), A∗ , Best-F irst or BeamSearch. Z´aroveˇ n je moˇzn´e nastavit r˚ uzn´e parametry u jednotliv´ ych strategi´ı jako hloubku prohled´av´an´ı, prioritu stav˚ u, apod. JPF obsahuje i strategie pro n´ahodn´ y bˇeh programem napˇr.RandomSearch nebo P athSearch. Vhodn´ ym v´ ybˇerem prohled´avac´ı strategie a jej´ıho nastaven´ı lze ˇr´ıdit generov´an´ı stavov´eho prostoru a t´ım doc´ılit zverifikov´an´ı zadan´e specifikace syst´emu dˇr´ıve, nemus´ı doj´ıt k explozi stavov´eho prostoru.
Redukce stavov´ eho prostoru. Java PathFinder obsahuje r˚ uzn´e mechanizmy, kter´e maj´ı za c´ıl omezit explozi stavov´eho prostoru. V kapitole 3, kter´a pojedn´av´a o Model checkingu jsou vyps´ any r˚ uzn´e pˇr´ıstupy jak doc´ılit redukce stavov´eho prostoru. Mechanizmy redukce v JPF jsou zaloˇzeny na uveden´ ych principech.
22
• Partial Order Reduction (POR) je metoda, kter´a u ´ˇcinnˇe redukuje poˇcet generovan´ ych stav˚ u. Poˇcet pl´ anovan´ ych rozhodov´an´ı (vˇetven´ı) m˚ uˇze b´ yt znaˇcnˇe omezen, pokud seskup´ıme vˇsechny instrukce v konkr´etn´ım vl´aknˇe, kter´e nemohou zp˚ usobit zmˇenu mimo toto vl´ akno. Takov´e instrukce jsou seskupeny do jednoho pˇrechodu, pokud program obsahuje hodnˇe vl´aken, kter´e mezi sebou nesd´ılej´ı data, m˚ uˇze b´ yt redukce stavov´eho prostoru znaˇcn´a. Oproti tomu pokud program obsahuje mnoˇzstv´ı sd´ılen´ ych dat nebo prov´ azan´ ych operac´ı, redukce pomoc´ı POR je minim´aln´ı. JPF prov´ ad´ı POR on-the-fly“, pˇri prov´adˇen´ı se nespol´eh´a na statickou anal´ yzu, ale vy” hodnocuje atomick´e sekce za bˇehu, resp. urˇcuje, kter´e instrukce mus´ı b´ yt vyhodnoceny jako hraniˇcn´ı dan´eho pˇrechodu do nov´eho stavu. Pokud je POR pˇri spuˇstˇen´ı JPF povolena, vykon´ avaj´ı se vˇsechny instrukce v aktu´aln´ım vl´aknˇe do okamˇziku neˇz dalˇs´ı instrukce zp˚ usob´ı zmˇenu v pl´anov´an´ı (scheduling relavant) nebo se m˚ uˇze jednat o instrukci, kter´ a zp˚ usobuje nedeterminismus. Z Java byte-code instrukc´ı je pouze asi 10% instrukc´ı, kter´e zp˚ usobuj´ı zmˇenu v pl´anov´an´ı, na obr. 4.2 jsou tyto instrukce vyobrazeny s jejich z´ avislostmi.
Obr´ azek 4.2: Instrukce maj´ıc´ı vliv na pl´anov´an´ı [9] • Choice Generatory (CG) jsou dalˇs´ım d˚ uleˇzit´ ym mechanizmem pro pr´aci s nedeterminismem. CG slouˇz´ı k vytvoˇren´ı vˇsech hodnot, kter´ ych mohou data v programu nab´ yvat nebo k vytvoˇren´ı vˇsech moˇznost´ı pl´anov´an´ı. CG jsou jedn´ım z moˇzn´ ych ˇreˇsen´ı jak se vyrovnat s probl´emem vstupn´ıch dat. Pomoc´ı rozhran´ı gov.nasa.jpf.jvm.Verify lze zadat, jak´ ych hodnot maj´ı urˇcit´e promˇenn´e nab´ yvat a takto specifikovan´ ymi moˇznostmi hodnot promˇenn´ ych se prov´ad´ı verifikace. Pokud jsou vstupn´ı data typu boolean nen´ı probl´em prov´est verifikaci nad vˇsemi moˇznostmi hodnot, u typu integer jiˇz nast´ av´ a probl´em s vygenerov´an´ım vˇsechn moˇznost´ı hodnot a u promˇenn´e typu float je to jiˇz velmi nevhodn´e.
23
K ˇreˇsen´ı tohoto probl´emu slouˇz´ı CG, pomoc´ı kter´ ych m˚ uˇzeme zadat jak´ ych hodnot m´ a promˇenn´ a nab´ yvat pˇri verifikaci (explicitn´ı urˇcen´ı zaj´ımav´ ych“ hodnoty pro ve” rifikaci). Pomoc´ı CG lze vymezit interval moˇzn´ ych hodnot Na obr. 4.3(a) typ boolean nab´ yv´ a vˇsech moˇznost´ı, typ integer nab´ yv´a hodnot ze zvolen´eho intervalu a u typu float i po vymezen´ı intervalu z˚ ust´av´a velk´e mnoˇzstv´ı moˇzn´ ych hodnot. Proto je zde dalˇs´ı mechanizmus jak urˇcit interval i krok mezi jednotliv´ ymi hodnotami. Pˇresn´e hodnoty promˇenn´e se pak definuj´ı aˇz pomoc´ı nastaven´ı parametr˚ u pˇri spuˇstˇen´ı JPF (obr. 4.3(b)). Tento mechanizmus lze pouˇz´ıt napˇr´ıklad pokud z hlediska verifikace je potˇreba pouze zjistit, zda je promˇenn´a vˇetˇs´ı nebo menˇs´ı neˇz urˇcit´ y pr´ ah. Podle v´ ysledku se zvol´ı jedna ze dvou moˇznost´ı. Je tedy nadbyteˇcn´e generovat vˇsechny moˇzn´e hodnoty promˇenn´e, pokud je relevantn´ı pouze vztah hodnoty k prahu).
Obr´ azek 4.3: Instrukce maj´ıc´ı vliv na pl´anov´an´ı [9]
• Explicitn´ı urˇ cen´ı Atomicity spoˇc´ıv´a v proveden´ı urˇcit´eho k´odu programu atomicky. Ta ˇc´ ast k´ odu, kter´ a m´a b´ yt provedena atomicky je explicitnˇe urˇcena uˇzivatelem pomoc´ıVerify.beginAtomic() a Verify.endAtomic(). Z´aroveˇ n mus´ı uˇzivatel zaruˇcit, ˇze d´ıky t´eto atomicitˇe nedojde k nenalezen´ı chyby v syst´emu.
4.4
Rozˇ siˇ ritelnost
Pro vyuˇzit´ı JPF v projektu SHADOWS je podstatn´a jeho vlastnost rozˇsiˇritelnosti. JPF je open source a je tedy moˇzn´e doimplementovat jin´e vlastn´ı moduly nebo funkce. Pro z´ısk´ an´ı dalˇs´ıch vlastnost´ı z verifikovan´eho syst´emu je moˇzn´e vytv´aˇret nov´e listenery, nov´e prohled´avac´ı strategie. Ty mohou b´ yt modifikac´ı jiˇz naimplementovan´ ych a upraveny pro konkr´etn´ı u ´ˇcel nebo je moˇzn´e vytv´ aˇret nov´e strategie spojen´ım v´ıce pˇr´ıstup˚ u dohromady.
24
Kapitola 5
Implementace Jak jiˇz bylo uvedeno v u ´vodu, c´ılem pr´ace bylo navrhnout a posl´eze implementovat metodu pro ovˇeˇren´ı opravy v projektu SHADOWS. C´ılem opravy je automatick´e l´eˇcen´ı chyb v Java programech. L´eˇcen´ı se specializuje na chyby vznikl´e soubˇeˇznost´ı, kapitola 2. Pro kontrolu opravy byla zvolena form´aln´ı metoda Model Checking, kapitola 3. Z d˚ uvodu probl´emu stavov´e exploze nen´ı moˇzn´e prov´est cel´ y model checking nad re´aln´ ym syst´emem. Proto pro vlastn´ı verifikaci byla zvolena modifikace – bounded model checking kapitola 3.5. Klasick´ y bounded model checking spoˇc´ıv´a v omezen´ı hloubky stavov´eho prostoru, kter´ y se m´a prohled´ avat. Pokud m´ a b´ yt bounded model checking pouˇzit pro ovˇeˇren´ı opravy, nen´ı c´ılem prov´est model checking od zaˇc´atku bˇehu programu do pˇredem definovan´e hloubky, ale zverifikovat konkr´etn´ı ˇc´ ast programu, kde byla aplikov´ana oprava. K tomuto u ´ˇcelu uzn´e strategie pro navigaci stavov´ ym prostorem do chybyly v kapitole 3.6 uvedeny i r˚ bov´eho stavu. Potom je jiˇz moˇzn´e prov´est bounded model checking ne z poˇc´ateˇcn´ıho stavu, ale z dan´eho stavu (napˇr. chybov´eho stavu) a zverifikovat poˇzadovan´e vlastnosti. K navigaci stavov´ ym prostorem byla vybr´ana strategie Record&Replay trace. Tato strategie byla vybr´ana pro moˇznost prov´est bounded model checking ne pouze z podezˇrel´eho (chybov´eho) stavu, ale i z nˇekter´eho z pˇredeˇsl´ ych stav˚ u. Tato vlastnost je velmi v´ yhodn´a z hlediska ovˇeˇren´ı opravy. Jako podezˇrel´ y stav je detekov´an chybov´ y stav, ale oprava m˚ uˇze prov´est zmˇeny v prov´ adˇen´ı programu nejenom po chybov´em stavu, ale tak´e pˇred n´ım (napˇr. pˇrid´ an´ı z´amku). Proto je moˇznost zaˇc´ıt verifikaci z nˇekter´eho z pˇredeˇsl´ ych stav˚ u v´ yhodn´a. Tento fakt pˇreb´ıj´ı nev´ yhody t´eto metody jako n´aroˇcnost na zaznamenan´e informace a zpomalen´ı bˇehu aplikace. Pro vlastn´ı implementaci byl zvolen model checker Java PathFinder, kter´ y sk´ yt´a velk´e moˇznosti rozˇsiˇritelnost o dalˇs´ı funkce (Listenery a Search Strategie). Listenery lze vyuˇz´ıt k z´aznamu potˇrebn´ ych informac´ı, lze tedy listenery pouˇz´ıt k z´aznamu bˇehu programu. Dalˇs´ı ˇc´ast spoˇc´ıv´ a v pˇrehr´ an´ı zaznamenan´e cesty a navigaci do konkr´etn´ıho stavu. K tomuto u ´ˇcelu lze vyuˇz´ıt vyhled´ avac´ı strategie, kter´e je samozˇrejmˇe opˇet potˇreba upravit a doimplementovat pro pˇrehr´ an´ı zaznamenan´e cesty. Pokud se dostaneme do poˇzadovan´eho stavu stavov´eho prostoru, je moˇzn´e prov´est bounded model checking, kter´ y se prov´ad´ı tak´e pomoc´ı modifikovan´e prohled´ avac´ı strategie, kter´a obsahuje vlastnosti bounded model checkingu. Kapitola je d´ ale rozdˇelena do d´ılˇc´ıch podkapitol, kde kaˇzd´a podkapitola popisuje urˇcitou ˇc´ast implementace. V prvn´ı podkapitole je uvedena implementace zvolen´e metody pro navigaci skrz stavov´ y prostor. Jedn´a se o strategii Record&Replay Trace. V prvn´ı f´azi byla tato metoda cel´ a implementov´ ana v Java PathFinderu, pro ovˇeˇren´ı a otestov´an´ı funkˇcnosti metody a ovˇeˇren´ı pouˇzitelnosti pomoc´ı zvolen´eho model checkeru. D´ale je zde uveden jednoduch´ y pˇr´ıklad, kter´ y demonstruje funkˇcnost zvolen´e strategie. 25
Druh´ a podkapitola se vˇenuje bounded model checkingu, po pˇrehr´an´ı cesty v JPF se z dosaˇzen´eho stavu provede bounded model checking. V t´eto podkapitole je pops´ana nov´ a prohled´ avac´ı strategie, kter´ a slouˇz´ı k vykon´an´ı bounded model checkingu, a kterou je moˇzn´e d´ale rozˇsiˇrovat o verifikaci dalˇs´ıch vlastnost´ı. I zde je uveden jednoduch´ y pˇr´ıklad pro lepˇs´ı n´azornost funkˇcnosti bounded model checkingu. Tˇret´ı podkapitola se vˇenuje modifikaci naimplementovan´ ych metod pro u ´ˇcel projektu SHADOWS. Aby bylo moˇzn´e v´ yˇse popsan´ y mechanizmus vyuˇz´ıt v projektu SHADOWS, je nutn´e prov´ adˇet nahr´ av´ an´ı bˇehu programu mimo JPF a v JPF prov´est aˇz samotnou verifikaci. Tato ˇc´ ast implementace nen´ı zcela dokonˇcen´a z d˚ uvod˚ u r˚ uzn´ ych peripeti´ı, s kter´ ymi bylo potˇreba se pˇri implementaci vypoˇr´adat. Probl´emy a jejich n´avrh ˇreˇsen´ı jsou uvedeny v dan´e podkapitole. Z´ aroveˇ n je zde nast´ınˇeno, jak´ ym smˇerem se bude d´ale pokraˇcovat v dokonˇcen´ı zaˇclenˇen´ı naimplementovan´ ych metod do projektu SHADOWS. Posledn´ı podkapitola obsahuje nˇekter´e testy a v´ ysledky, kter´e jsou pouze d´ılˇc´ı. Celkov´e testov´an´ı naimplementovan´ ych metod bude moˇzn´e aˇz po integraci strategi´ı do projektu SHADOWS.
5.1
Record&Replay trace v JPF
Metoda Record&Replay trace je zaloˇzena na z´aznamu potˇrebn´ ych informac´ı pro opˇetovn´e pˇrehr´an´ı stejn´eho bˇehu programu. Aby bylo moˇzn´e tuto metodu aplikovat pro ovˇeˇren´ı opravy, bylo nutn´e nejprve otestov´an´ı, zda je tento mechanizmus – z´aznamu cesty a pˇrehr´an´ı dan´e cesty v JPF – v˚ ubec moˇzn´ y. Z toho d˚ uvodu byly vytvoˇreny listenery (cz.vutbr.fit.tools.CG.SaveCurChoice a cz.vutbr.fit.tools.CG.LoadCurChoice) pro ovˇeˇren´ı moˇznosti implementace navigace stavov´ ym prostorem. JPF je model checker, kter´ y prov´ad´ı rozgenerov´an´ı cel´eho stavov´eho prostoru a bylo tedy nutn´e nejprve pochopit jeho princip verifikace. Jak jiˇz bylo uvedeno JPF obsahuje ˇradu prohled´ avac´ıch strategi´ı. Pro pochopen´ı principu generov´an´ı stavov´eho prostoru jsou d˚ uleˇzit´e n´ asleduj´ıc´ı z´ akladn´ı strategie DF S a BF S. • DF S strategie: 1) Sestrojen´ı z´asobn´ıku (stack), kter´ y obsahuje vˇsechny uzly, kter´e se maj´ı expandovat. Na zaˇc´atku z´asobn´ık obsahuje poˇc´ateˇcn´ı stav. 2) Je-li z´asobn´ık pr´ azdn´ y, prohled´ av´ an´ı konˇc´ı. Jinak se pokraˇcuje v prohled´av´an´ı. 3) Ze z´asobn´ıku se vybere prvn´ı uzel. 4) Vybran´ y uzel se expanduje a vˇsechny jeho bezprostˇredn´ı n´ asledn´ıci se uloˇz´ı do z´ asobn´ıku. Pokud se nejedn´a o stav, kter´ y jiˇz v z´asobn´ıku je nebo je jiˇz expandovan´ y, provede se n´avrat do bodu 2). Implementace DF S metody v JPF (gov.nasa.jpf.search.DFSearch) je navrˇzena takov´ ym zp˚ usobem, aby nedoch´azelo ke generov´an´ı vˇsech n´asledn´ık˚ u, ale do z´asobn´ıku jsou uloˇzeny pouze vˇsechny expandovan´e stavy a informace o moˇzn´ ych n´asledovn´ıc´ıch pomoc´ı CG (ne cel´ y stav). Dalˇs´ı bezprostˇredn´ı n´asledovn´ıci stavu se generuj´ı aˇz pˇred vykon´ an´ım stavu. Pro oˇsetˇren´ı, aby se negeneroval jeden stav v´ıcekr´at, slouˇz´ı mechanizmus State matching, kapitola 4. • BF S strategie: 1) Sestrojen´ı dvou seznam˚ u, prvn´ı tvoˇr´ı frontu obsahuj´ıc´ı vˇsechny uzly urˇcen´e k vykon´ an´ı a druh´ y obsahuje jiˇz expandovan´e stavy. Do prvn´ı fronty se na zaˇc´ atku vloˇz´ı poˇc´ ateˇcn´ı stav. 2) Pokud prvn´ı fronta neobsahuje ˇz´adn´ y stav pro rozgenerov´ an´ı prohled´ av´an´ı konˇc´ı. Jinak se pokraˇcuje v prohled´av´an´ı stavov´eho prostoru. 3) Z prvn´ıho seznamu se vybere ˇceln´ı stav a uloˇz´ı se do druh´eho seznamu 26
ˇ ı stav z prvn´ıho seznamu se expanduje a jeho bez(jiˇz expandovan´ ych uzl˚ u). 4) Celn´ prostˇredn´ı n´ asledovn´ıci se uloˇz´ı do prvn´ıho seznamu (pokud jiˇz nejsou vygenerov´any bud’ v prvn´ım nebo druh´em seznamu). Implementace BF S metody v JPF (gov.nasa.jpf.search.heuristic.BFSearch) je naimplementov´ ana podobn´ ym zp˚ usobem. V metodˇe doch´az´ı k vygenerov´an´ı vˇsech bezprostˇredn´ıch n´ asledovn´ık˚ u po expandov´an´ı stavu (vˇsechny moˇznosti z CG), tyto stavy jsou vytvoˇreny a pˇred jejich vykon´an´ım doch´az´ı pouze k jejich postupn´emu obnoven´ı. Ve strategii BF S je zaj´ımavou myˇslenkou rozgenerov´an´ı vˇsech moˇzn´ ych n´asledovn´ık˚ u (t´ım je vidˇet, co kter´ y vykon´ av´ a). Nicm´enˇe ve strategii BF S se do fronty pro n´asledovan´e obnoven´ı a vykon´ an´ı stavu uloˇz´ı vˇsichni bezprostˇredn´ı n´asledovn´ıci. C´ılem strategie Record&Replay trace je vykonat pouze konkr´etn´ı moˇznost a ostatn´ı nerozgenerov´avat, resp. vykonat pouze jeden konkr´etn´ı bˇeh programu. Toho lze doc´ılit napl´anov´an´ım a uloˇzen´ım do fronty pouze zvolen´e moˇznosti CG.
5.1.1
Record&Replay pomoc´ı ChoiceGener´ ator˚ u
Aby bylo moˇzn´e napl´ anovat pouze konkr´etn´ı moˇznost CG, je zapotˇreb´ı pochopit ovl´ad´ an´ı ChoiceGenr´ ator˚ u a volba urˇcit´ ych moˇznost´ı. JPF obsahuje Listener, kter´ y demonstruje pr´ aci ChoiceGener´ ator˚ u gov.nasa.jpf.tools.CGMonitor. Uk´azka ˇc´asti v´ ypisu z dan´eho listeneru je na obr. 5.1, listener vypisuje moˇznosti CG, kde doˇslo k volbˇe a kter´a moˇznost byla zvolena. V´ ypis je ze vzorov´eho verifikaˇcn´ıho pˇr´ıkladu JPF (trunk/examples/Rand.java). Dalˇs´ım naimplementovan´ ym listenerem je gov.nasa.jpf.tools.ChoiceSeletor, kter´ y demonstruje prov´ adˇen´ı pouze jedn´e n´ahodnˇe zvolen´e moˇznosti z CG. ============================================================== system under test application:.../trunk/examples/Rand.java ============================================================== search started:... gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main} .gov.nasa.jpf.jvm.choice.IntIntervalGenerator[0..1,delta=+1,cur=0] a=0 ..gov.nasa.jpf.jvm.choice.IntIntervalGenerator[0..2,delta=+1,cur=0] b=0 c=0 ..gov.nasa.jpf.jvm.choice.IntIntervalGenerator[0..2,delta=+1,cur=1] b=1 c=0 ..gov.nasa.jpf.jvm.choice.IntIntervalGenerator[0..2,delta=+1,cur=2] b=2
ˇ ast v´ Obr´ azek 5.1: C´ ypisu testov´eho pˇr´ıkladu s listenerem CGMonitor
SaveCurChoice. SaveCurChoice je listener, kter´y zaznamen´av´a potˇrebn´e informace o zvolen´e moˇznosti CG do souboru. Pomoc´ı pˇreddefinovan´eho rozhran´ı VMListener˚ u je detekov´ an zaˇc´ atek nov´e moˇznosti ChoiceGener´atoru. Po vykon´an´ı prvn´ı instrukce do zaˇc´atku nov´e moˇznosti CG (zvolen´ a moˇznost se jiˇz vykon´av´a), se uloˇz´ı informace o jak´ y typ CG se jedn´a (BooleanChoiceGenerator, ThreadChoiceGenerator, atd.), o kolik´atou moˇznost z CG se jedn´ a a jak´e je aktu´ aln´ı vl´ akno. Tyto informace jsou postaˇcuj´ıc´ı k opˇetovn´emu pˇrehr´ an´ı spr´avn´e moˇznosti CG. Listener umoˇznuje n´asleduj´ıc´ı nastaven´ı (properties): 27
save cur choice.trace – n´ azev v´ ystupn´ıho souboru se z´aznamem bˇehu, y bude zaps´an do v´ ystupn´ıho souboru, save cur choice.comment – znˇen´ı koment´aˇre, kter´ vut.logging – (true/false) pro v´ ypis vykonan´ ych moˇznost´ı CG na pˇr´ıkazovou ˇr´adku (v´ ypis urˇcen´ y pro testov´ an´ı).
LoadCurChoice Jedn´a se o listener, kter´y podle vstupn´ıho souboru, kter´y obsahuje CG a jejich zvolen´e moˇznosti provede naˇcten´ı cesty a pokud je to moˇzn´e opˇetovn´e pˇrehr´ an´ı programu koresponuj´ıc´ı s uloˇzenou cestou (uloˇzen´a cesta CG koresponduje s CG, kter´e jsou voleny ve spuˇstˇen´e aplikaci). Listener gov.nasa.jpf.tools.ChoiceSelector je z´akladem uveden´eho nov´eho listeneru. Bˇehem registrace listeneru pˇri spuˇstˇen´ı JPF se naˇcte cesta ze souboru. Pokud se pˇri vykon´av´an´ı programu naraz´ı na vytv´aˇren´ı nov´eho CG, provede se kontrola s naˇctenou cestou, pokud typ aktu´ aln´ıho CG z uloˇzen´e cesty koresponduje s typem CG z vykon´avan´eho programu napl´ anuje se proveden´ı pouze uloˇzen´e moˇznosti. Listener umoˇznuje n´asleduj´ıc´ı nastaven´ı (propeties): azev vstupn´ıho souboru se zaznamenanou cestou, load cur choice.trace – n´ load cur choice.after – (true/false) pro moˇznost pokraˇcovat ve vyhled´av´an´ı i pokud uloˇzen´a cesta jiˇz skonˇcila nebo uloˇzen´a cesta nekoresponduje s vykon´avan´ ym programem, load cur choice.randomSeed – zad´an´ı ˇrady pro Random, kter´a se pouˇzije pro n´ahodn´ y v´ ybˇer moˇznosti CG, nekoresponduj´ıc´ıch s uloˇzenou cestou (urˇceno pro testov´an´ı).
5.1.2
Record&Replay pomoc´ı byte-code instrukc´ı
Z pˇredchoz´ı ˇc´ asti vypl´ yv´ a, ˇze JPF lze pouˇz´ıt pro implementaci metody Record&Replay trace. V prvn´ı f´ azi byly pro z´ aznam a pˇrehr´an´ı cesty vyuˇzity ChoiceGener´atory, ty lze ale z´ıskat pouze v pˇr´ıpadˇe z´ aznamu bˇehu programu v JPF. Podstata pouˇzitelnosti metody spoˇc´ıv´a v moˇznosti pˇrehr´an´ı bˇehu programu pomoc´ı informac´ı, kter´e lze z´ıskat z libovoln´eho“ bˇehu programu. ” C´ılem je pˇrehr´ at bˇeh programu napsan´eho v Javˇe, zdrojov´ y k´od se nejprve pˇreloˇz´ı do spustiteln´eho mezik´ odu – Java byte-code. Tento k´od se posl´eze spust´ı pomoc´ı JVM (Java Virtual Machine). Jak jiˇz bylo uvedeno, JPF je speci´aln´ı virtu´aln´ı stroj, kter´ y tak´e prov´ ad´ı bˇeh programu pomoc´ı byte-code instrukc´ı. Pro pˇrehr´ an´ı urˇcit´eho bˇehu programu je tedy potˇreba zaznamenat poˇrad´ı vykon´av´ an´ı jednotliv´ ych byte-code instrukc´ı a informace o tom, kter´e vl´akno dan´e instrukce vykon´av´ a. Z´aznam cesty je st´ ale prov´ adˇen pomoc´ı JPF, ale tentokr´at se ukl´adaj´ı ty informace, kter´e lze z´ıskat z programu i bez JPF. Mezi dalˇs´ı informace, kter´e je potˇreba zn´at pro pˇresn´e pˇrehr´an´ı cesty programu jsou vstupn´ı data, ˇcten´ı/z´apis do souboru atd. Tyto informace nebyly prozat´ım br´ any v potaz a z´ aznam/pˇrehr´an´ı cesty se prov´ad´ı nad programy, u kter´ ych ˇ ı/z´apis do souboru je sloˇzit´ tyto informace nejsou zapotˇreb´ı. Cten´ y probl´em, JPF nepodporuje knihovny pro ˇcten´ı/z´ apis do souboru. Dalˇs´ı d˚ uleˇzit´e informace, jako vstupn´ı data, lze oˇsetˇrit naˇcten´ım poˇzadovan´ ych hodnot pomoc´ı CG. Pouˇzit´ı CG ovˇsem vyˇzaduje z´asah do zdrojov´eho k´ odu programu. Z toho d˚ uvodu se zat´ım programy se vstupn´ımi daty neuvaˇzuj´ı. JPF je speci´ aln´ı virtu´ aln´ı stroj, jako takov´ y potˇrebuje i speci´aln´ı byte-code instrukce. Mechanizmus pˇrehr´ an´ı programu v JPF spoˇc´ıv´a v naˇcten´ı Java byte-codu a pˇreveden´ı standardn´ıch byte-code instrukc´ı na instrukce JPF, tyto instrukce plnˇe koresponduj´ı s Java byte-code instrukcemi. Maj´ı stejn´e n´azvy, stejn´e funkce i stejn´e parametry.
28
D´ıky faktu prov´ adˇen´ı programu pˇr´ımo v JPF a dobr´emu rozhran´ı na listenery, je moˇzn´e pˇripojit listenery t´emˇeˇr kamkoliv. Rozhran´ı pro VMListenery obsahuje metodu pro napojen´ı se na bˇeh programu za kaˇzdou vykonanou instrukci instructionExecuted(...). D´ıky tomuto mechanizmu je jednoduch´e odchyt´avat d˚ uleˇzit´e informace – vˇsechny vykonan´e byte-code instrukce, bˇeˇz´ıc´ı vl´ akna atd. Jelikoˇz k z´aznamu potˇrebn´ ych informac´ı doch´ az´ı st´ale zat´ım v JPF, je moˇzn´e zaznamenat v´ıce informac´ı najednou a pouˇz´ıt je pro ovˇeˇren´ı korektnosti pˇrehr´ an´ı cesty nebo pro informativn´ı v´ ypis.
RecordTrace. Pro z´aznam cesty, kter´a obsahuje vykonan´e byte-code instrukce je vytvoˇren nov´ y listener cz.vutbr.fit.tools.RecordTrace. Ten se podob´a pˇredeˇsl´e implementaci listeneru (SaveCurChoice). Rozd´ıl je v implementovan´ ych metod´ach pomoc´ı rozhran´ı VMListener a v zaznamenan´ ych informac´ıch bˇehem bˇehu programu. I tento listener umoˇzn ˇuje nastaven´ı parametr˚ u, kter´e ovlivˇ nuj´ı jeho funkci: vut record trace.CG – (true/false) pro zaznamen´av´an´ı informace o zvolen´e moˇznosti CG (urˇceno pro testov´ an´ı), vut record trace.Insn – (true/false) pro zaznamen´av´an´ı vykonan´e instrukce byte-codu, vut record trace.Thread – (true/false) pro zaznamen´av´an´ı informac´ı o aktu´aln´ım vl´aknˇe (jm´eno, index), vut record trace.FileName – n´ azev v´ ystupn´ıho souboru se zaznamenanou cestou, vut record trace.Info – (true/false) zaznamen´av´an´ı dalˇs´ıch informac´ı (krok vpˇred, krok vzad, apod.). Z nastaven´ı listeneru plyne moˇznost zaznamen´avat r˚ uzn´e informace podle poˇzadavk˚ u. Aby pˇr´ı naˇc´ıt´ an´ı inforamc´ı zaznamenan´e cesty bylo patrn´e, o jakou informaci se jedn´ a, obsahuje kaˇzd´ y typ informace sv˚ uj pˇredem definovan´ y prefix. Pˇr´ıklad ˇc´asti souboru se zaznamenanou cestou, kter´ a obsahuje vˇsechny moˇzn´e informace, je na obr. 5.2. /* Record trace, search started. */ application vut.delivereble.TwoThreadsTest [0] gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet 1 main 0 # main@0 "invokestatic java.lang.Object.
()V" # main@0 "invokestatic java.lang.Object.registerNatives()V" # main@0 "return java.lang.Object.()V" ... # main@0 "return vut.delivereble.SimpleThread.(Ljava/lang/String;)V" % started Martin index 2 % # main@0 "invokevirtual vut.delivereble.SimpleThread.start()V" [5] gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet 1 main 0 # main@0 "invokevirtual vut.delivereble.SimpleThread.start()V" % terminated main index 0 % # main@0 "return vut.delivereble.TwoThreadsTest.main([Ljava/lang/String;)V" [6] gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet 2 main 0 # Marek@2 "runstart" # Marek@2 "iconst_0" ...
Obr´azek 5.2: Zaznamenan´ a cesta pomoc´ı listeneru cz.vutbr.fit.tools.RecordTrace Kaˇzd´ y v´ ypis obsahuje na zaˇc´atku informace o aplikaci, ke kter´e byl poˇr´ızen – n´ azev aplikace a vstupn´ı parametry, pokud nˇejak´e byly. D´ale obsahuje informace o CG (prefix [x], kde x je ˇc´ıslo CG), typ CG, jak´a moˇznost byla zvolena a ˇc´ıslo vybran´e moˇznosti. 29
Nejˇcastˇejˇs´ı poloˇzkou z´ aznamu jsou informace, podstatn´e pro pˇrehr´an´ı cesty. Tyto informace jsou: jm´eno aktu´ aln´ıho vl´ akna, index aktu´aln´ıho vl´akna a popis byte-code instrukce (prefix #). Posledn´ım typem informace jsou informace o stavech a prohled´av´an´ı stavov´ ym prostorem (prefix %). Pomoc´ı listeneru RecordTrace lze tedy prov´est z´aznam cesty v JPF. Nicm´enˇe pokud by byla aplikace spuˇstˇena v JPF pouze s t´ımto listenerem, nedoˇslo by k z´aznamu jedn´e cesty, ale JPF automaticky prohled´ av´ a cel´ y stavov´ y prostor. Implicitn´ı prohled´avac´ı strategi´ı je DFS. Pokud je tedy c´ılem zaznamenat pouze jeden bˇeh aplikace, je nutn´e spustit JPF s jinou vyhled´ avac´ı strategi´ı, kter´ a prov´ ad´ı resp. simuluje pouze jeden bˇeh programu. JPF obsahuje dvˇe jednoduch´e naimplementovan´e strategie RandomSearch a PathSearch. Ty simuluj´ı n´ahodn´ y v´ ybˇer moˇznosti CG a jeho proveden´ı. Jinou moˇznost´ı je vyuˇzit naimplementovan´ ych listener˚ u SaveCurChoice a LoadCurChoice. JPF se spust´ı s aplikac´ı v z´akladn´ım nastaven´ı a s listenerem SaveCurChoice. Pomoc´ı nˇeho se zaznamenaj´ı vˇsechny moˇzn´e cesty, jedna z nich se vybere a uloˇz´ı do souboru, kter´ y bude na vstupu druh´eho listeneru LoadCurChoice. Pˇri spuˇstˇen´ı JPF s listenerem LoadCurChoice se pˇrilinkuje i listener pro z´aznam relevantn´ıch informac´ı o cestˇe RecordTrace. D´ıky tomu se doc´ıl´ı zaznamen´ an´ı n´ami zvolen´e zaj´ımav´e cesty a ne pouze n´ahodn´e cesty.
ReplayTrace. Pˇrehr´an´ı cesty jiˇz nelze implementovat jako listener. Je tˇreba vybrat a prov´est stavy ve stavov´em prostoru, kter´e koresponduj´ı se zaznamenanou cestou. Pro tento mechanizmus je naimplementov´ ana nov´a prohled´avac´ı strategie. Tato prohled´avac´ı strategie, jako vˇsechny naimplementovan´e prohled´avac´ı strategie v JPF, je zaloˇzena na superclass Search. Nov´ a strategie ReplayTrace m´a z´aklad v prohled´avac´ıch strategi´ıch – DFSearch a BFSearch. Princip ReplayTrace spoˇc´ıv´ a v generov´an´ı vˇsech bezprostˇredn´ıch n´asledovn´ık˚ u aktu´aln´ıho stavu a v´ ybˇerem pouze tˇech, kteˇr´ı koresponduj´ı se zaznamenanou cestou ve vstupn´ım souboru (kter´ y je v´ ystupem z RecordTrace). Tento mechanizmus se opakuje u kaˇzd´eho stavu a t´ım se doc´ıl´ı rozgenerov´ an´ı pouze t´e ˇc´asti stavov´eho prostoru, kter´a koresponduje s uloˇzenou cestou. Prohled´ av´ an´ı stavov´eho prostoru pro urˇcen´ı koresponduj´ıc´ıch n´asledovn´ık˚ u se prov´ad´ı pomoc´ı prohled´ avac´ı strategie BFS. ReplaySearchHeuristic je tedy nov´a vyhled´avac´ı strategie zaloˇzen´a na principu Search strategi´ı, a jej´ı z´ aklad je pˇrevzat z vyhled´avac´ıch strategi´ı DFSearch a BFSHeuristic. Z´asadn´ı rozd´ıl spoˇc´ıv´ a v rozgenerov´av´an´ı jednotliv´ ych n´asledovn´ık˚ u a jejich prov´adˇen´ı. Stejnˇe jako listenery i vyhled´ avac´ı strategie sk´ ytaj´ı moˇznost nastaven´ı parametr˚ u. U t´eto strategie lze nastavit n´ asleduj´ıc´ı: u, kter´e se ukl´adaj´ı ke genevut.replay search.QueueLimit – maxim´aln´ı d´elka fronty stav˚ rov´an´ı (omezen´ı pouˇzit´ı pamˇeti), vut.replay search.FileName – n´ azev vstupn´ıho souboru se zaznamenanou cestou, vut.replay search.ShowInfo – (true/false) podm´ınka pro vypisov´an´ı pr˚ ubˇeˇzn´ ych informac´ı bˇehem prohled´ av´ an´ı (urˇceno pro testov´an´ı), vut.replay search.HeurisiticName – volba prohled´avac´ı strategie stavov´ ym prostorem (DFS, BFS). Pˇri zaregistrov´ an´ı vyhled´ avac´ı strategie po spuˇstˇen´ı JPF se nejprve naˇcte zaznamenan´a cesta ze vstupn´ıho souboru. Pro naˇc´ıt´an´ı cesty byla implementov´ana nov´a tˇr´ıda cz.vutbr.fit.tools.LoadRecord. LoadRecord slouˇz´ı k naˇcten´ı cesty ze souboru a souˇcasn´emu rozdˇelen´ı jednotliv´ ych informac´ı. Ty jsou zaps´any do struktury Trace ti insn,
30
kter´a m´ a formu seznamu. Trace ti insn umoˇznuje uchov´avat pˇr´ıznak o n´aslednosti jednotliv´ ych informac´ı, a tak´e umoˇznuje jednoduch´ y pˇr´ıstup k d´ılˇc´ım dat˚ um. Dalˇs´ım krokem je naˇcten´ı struktury Trace ti insn do tˇr´ıdy CheckStep, kter´a prov´ ad´ı samotn´e porovn´ an´ı zaznamenan´e cesty s bˇehem programu. Porovn´an´ı bˇehu se prov´ ad´ı po jednotliv´ ych kroc´ıch. Po vygenerov´an´ı nov´eho stavu se zavol´a metoda CheckState(), kter´a porovn´ a aktu´ aln´ı krok programu s aktu´aln´ım krokem zaznamenan´e cesty. Aktu´aln´ı krok z´aznamu, je prvn´ı krok z´ aznamu, kter´ y jeˇstˇe nebyl pˇrehr´an prov´adˇen´ ym programem. Po spuˇstˇen´ı prohled´ av´ an´ı stavov´eho prostoru pomoc´ı strategie ReplaySearchHeuristic se zaˇcne prohled´ avat stavov´ y prostor stejn´ ym zp˚ usobem jako u strategie BF S. Po vykon´an´ı poˇc´ ateˇcn´ıho stavu dojde k rozgenerov´an´ı bezprostˇredn´ıch n´asledovn´ık˚ u. Po vygenerov´an´ı n´ asledovn´ık˚ u dojde k jejich zaˇrazen´ı do fronty, kde ˇcekaj´ı na vykon´an´ı, z´aroveˇ n dojde k nastaven´ı pˇr´ıznakugenerateChildren. Ten urˇcuje, zda m´a b´ yt stav vykon´an a jeho n´ asledovn´ıci generov´ ani. Pomoc´ı pˇr´ıznaku doch´az´ı k vykon´av´an´ı pouze tˇech stav˚ u, kter´e koresponduj´ı s uloˇzenou cestou v souboru. Urˇcen´ı, zda aktu´ aln´ı stav (krok) programu koresponduje s uloˇzenou cestou, se prov´ ad´ı v metodˇe CheckState(), tˇr´ıdy CheckStep. Na zaˇc´atku prohled´av´an´ı byla zaznamenan´ a cesta pˇred´ ana do tˇr´ıdy CheckStep. Po z´aznamu cesty je moˇzn´e se pohybovat po jednotliv´ ych kroc´ıch, aktu´ aln´ım krokem zaznamenan´e cesty je posledn´ı nevykonan´ y krok v programu. Parametrem metody CheckState() je aktu´aln´ı krok prov´adˇen´eho programu, ten se porovn´ av´ a s aktu´ aln´ım krokem zaznamenan´e cesty. Urˇcen´ı koresponduj´ıc´ıch krok˚ u se prov´ad´ı podle shody jednotliv´ ych byte-code instrukc´ı a vl´akna, kter´e je vykon´av´a. Porovn´ an´ı byte-code instrukc´ı a identifikace vl´akna je jednoduch´a, maj´ı stejnou signaturu (z´aznam i pˇrehr´ an´ı se prov´ ad´ı pomoc´ı JPF). Probl´em pro porovn´an´ı jednotliv´ ych krok˚ u nast´ av´ a u hranice pˇrechodu mezi jednotliv´ ymi stavy. Hranic´ı pˇrechodu b´ yv´a typicky instrukce pro naˇcten´ı/uloˇzen´ı promˇenn´e nebo zmˇenu aktu´aln´ıho vl´akna. Pokud v m´ıstˇe naˇcten´ı/uloˇzen´ı promˇenn´e doch´ az´ı k vˇetven´ı (generov´an´ı nov´ ych stav˚ u). Je tˇreba d´avat pozor, zda k vykon´an´ı instrukc´ı doch´ az´ı pˇred ukonˇcen´ım pˇrechodu, a je tud´ıˇz tˇreba z´ıskat naˇctenou/uloˇzenou hodnotu promˇenn´e i ve vˇsech rozgenerovan´ ych stavech, vykon´an´ı instrukce se opakuje na zaˇc´atku nov´eho pˇrechodu. M˚ uˇze nastat i situace, kdy je vykon´an´ı instrukce napl´anovan´e aˇz na zaˇc´ atku nov´ ych pˇrechod˚ u. V pˇr´ıpadˇe jednoho bˇehu JPF tento probl´em nevznik´ a, probl´em nast´ av´ a pˇri porovn´ av´ an´ı pˇrechod˚ u dvou bˇeh˚ u JPF. Je tedy nutn´e s t´ımto probl´emem poˇc´ıtat pˇri porovn´ av´ an´ı jednotliv´ ych krok˚ u programu. Pˇri urˇcov´ an´ı korespondence jednotliv´ ych krok˚ u je nutn´e tak´e poˇc´ıtat s faktem, kdy m˚ uˇze skonˇcit zaznamenan´ a cesta a prohled´av´an´ı stavov´eho prostoru nen´ı ukonˇceno. V takov´em pˇr´ıpadˇe lze prov´est bud’ ukonˇcen´ı prohled´av´an´ı s koncem zaznamenan´e cesty nebo d´ ale prov´adˇet n´ ahodn´ y v´ ybˇer a dokonˇcen´ı jednoho bˇehu programu.
5.1.3
Pˇ r´ıklad na Record&Replay trace
Pro uk´ azku funkˇcnosti strategie Record&Replay, je zde uveden pˇr´ıklad TwoThreads. Jedn´ a se o jednoduch´ y pˇr´ıklad, kter´ y prov´ad´ı prokl´ad´an´ı dvou vl´aken. Kaˇzd´e z vl´aken v cyklu vypisuje na standardn´ı v´ ystup svoje jm´eno a index pr˚ uchodu cyklem. Na obr. 5.3 je uveden zdrojov´ y k´ od programu.
31
class SimpleThread extends Thread { ... public void run() { for (int i = 0; i < 2; i++) { System.out.println(i + " " + getName()); } System.out.println("DONE! " + getName()); } } public class TwoThreads ... { public static void main (String args[]) { new SimpleThread("First-thread").start(); new SimpleThread("Second-thread").start(); } }
Obr´ azek 5.3: Zdrojov´ y Java k´ od pˇr´ıkladu pro demonstraci strategie Record&Replay
V prvn´ım kroku dojde k z´ aznamu jednoho bˇehu programu pomoc´ı JPF. Na obr. 5.4 je uveden jeden z moˇzn´ ych bˇeh˚ u programu v JPF s listenerem pro z´aznam bˇehu do souboru. ... -----------------------------------listener recordTrace Started. 0 First-thread 1 First-thread DONE! First-thread 0 Second-thread 1 Second-thread DONE! Second-thread -----------------------------------listener recordTrace Finished. ...
Obr´ azek 5.4: Jeden z moˇzn´ ych v´ ystup˚ u programu pˇri z´aznamu cesty v JPF Pomoc´ı nastaven´ı listeneru bylo zvoleno uloˇzen´ı pouze nejnutnˇejˇs´ıch informac´ı pro pˇrehr´ an´ı cesty programu. Zaznamenan´e informace jsou jm´eno aktu´aln´ıho vl´akna, jeho index a vykonan´e byte-code instrukce. Uk´ azka ˇc´asti z´aznamu cesty je na obr. 5.5. /* Record trace, search started. */ application: vut.testBytecode.TwoThreads # main@0 "invokestatic java.lang.Object.()V" # main@0 "invokestatic java.lang.Object.registerNatives()V" ... # First-thread@1 "runstart" # First-thread@1 "iconst_0" # First-thread@1 "istore_1" # First-thread@1 "goto 17" # First-thread@1 "iload_1" # First-thread@1 "iconst_2" ... # Second-thread@2 "invokevirtual java.io.PrintStream.println(Ljava/lang/String;)V" # Second-thread@2 "return vut.testBytecode.SimpleThread.run()V" /* Record trace, search finished. */
Obr´ azek 5.5: Zaznamenan´ a cesta koresponduj´ıc´ı s bˇehem programu z obr. 5.4 Pˇrehr´ an´ı zaznamenan´e cesty v JPF demonstruje n´asleduj´ıc´ı obr. 5.6. Na obr´azku je patrn´e generov´ an´ı stavov´eho prostoru. Z kaˇzd´eho stavu doˇslo k vygenerov´an´ı vˇsech bezprostˇredn´ıch n´ asledovn´ık˚ u. Nicm´enˇe vykon´av´an´ı vygenerovan´eho stavu a jeho n´asledovn´ık˚ u pokraˇcuje pouze t´ım stavem (stavy), kter´e koresponduj´ı se zaznamenan´ ymi kroky cesty. 32
V uveden´em pˇr´ıkladˇe se jedn´ a vˇzdy pouze o jeden koresponduj´ıc´ı n´asleduj´ıc´ı stav. Generov´an´ı cesty konˇc´ı po dosaˇzen´ı posledn´ıho stavu uloˇzen´e cesty.
Obr´ azek 5.6: Graf vygenerovan´eho stavov´eho prostoru pomoc´ı cesty z obr. 5.5
5.2
Bounded model checking v JPF
Po implementaci metody Record&Replay trace je dalˇs´ım krokem proveden´ı bounded model checkingu v JPF. Bounded model checking v JPF je moˇzn´e aplikovat na r˚ uzn´e prohled´avac´ı strategie, napˇr. na ˇcasto jmenovan´e BF S a DF S. Pomoc´ı parametr˚ u strategi´ı je moˇzn´e zadat poˇzadovanou nejvˇetˇs´ı hloubku prohled´ av´ an´ı k. Standardnˇe se bounded model checking prov´ad´ı z poˇc´ ateˇcn´ıho stavu do zvolen´e hloubky k, z´aroveˇ n je moˇzn´e zad´avat dalˇs´ı nastaviteln´e parametry prohled´ av´ an´ı, a tak´e pˇrid´ an´ı dalˇs´ıch listener˚ u pro verifikaci dalˇs´ıch vlastnost´ı sledovan´eho syst´emu. Pokud vezmeme form´ aln´ı z´ apis bounded model checkingu z kapitoly 3.5, kde je verifikovan´ y syst´em pops´ an pomoc´ı Kripkeho struktury, je moˇzn´e naj´ıt podobnou strukturu syst´emu i v JPF. V JPF se nejprve nevytv´aˇr´ı model verifikovan´eho syst´emu, ale verifikace se prov´ ad´ı pˇr´ımo nad re´ aln´ ym syst´emem. Nicm´enˇe i zde se d´a naj´ıt podobnost v pr˚ uchodu stavov´ ym prostorem s v´ ypoˇcetn´ım stromem Kripkeho struktury. JPF pˇr´ı prohled´av´an´ı stavov´eho prostoru vytv´ aˇr´ı stavy syst´emu i pˇrechody. Pˇrechod mezi stavy je definov´an pomoc´ı vykonan´ ych byte-code instrukc´ı. Stav syst´emu je charakterizov´an aktu´aln´ım stavem cel´eho syst´emu (hodnoty promˇenn´ ych, aktu´aln´ı vl´akno, atd.). Vlastnosti, kter´e se maj´ı u syst´emu verifikovat jsou form´ alnˇe zapsan´e pomoc´ı tempor´aln´ıch formul´ı. Pˇri verifikace pomoc´ı JPF lze nadefinovat verifikovan´e vlastnosti a ovˇeˇrit je pomoc´ı listener˚ u. Ty se daj´ı pˇripojit na ve33
rifikovan´ y syst´em do poˇzadovan´eho m´ısta a s generov´an´ım stavov´eho prostoru kontroluj´ı poˇzadovan´e vlastnosti. JPF umoˇzn ˇuje z´ıskat informaci, zda omezen´a cesta obsahuje smyˇcku (k-loop) pro verifikaci nekoneˇcn´ ych vlastnost´ı. V JPF nedoch´az´ı k opˇetovn´emu vytv´aˇren´ı shodn´eho stavu. Pokud byl jednou stav vygenerov´ an, nedoch´az´ı k jeho opˇetovn´emu generov´an´ı v jin´em m´ıstˇe stavov´eho prostoru, ale pouze se vyuˇziji jiˇz existuj´ıc´ı stav. Proto je snadn´e zjistit, zda na generovan´e cestˇe existuje zpˇetn´ a smyˇcka. JPF implicitnˇe umoˇzn ˇuje prov´adˇet bounded model checking z poˇc´ateˇcn´ıho stavu. C´ılem pr´ace je ovˇsem prov´est bounded model checking z pˇredem urˇcen´eho stavu a ne pouze ze stavu poˇc´ ateˇcn´ıho. K tomu u ´ˇcelu byly vytvoˇreny pˇredch´azej´ıc´ı listenery a prohled´avac´ı strategie. Prvn´ı moˇznost´ı je vyuˇzit´ı prvn´ıch listener˚ u (LoadCurChoice a SaveCurChoice). Pomoc´ı listeneru SaveCurChoice se zaznamen´a cesta aˇz do podezˇrel´eho (chybov´eho) stavu. Z´aznam cesty tedy konˇc´ı v m´ıstˇe, kde se posl´eze m´a zaˇc´ıt prov´adˇet bounded model checking nebo je moˇzn´e urˇcit, zda se pˇred zaˇc´ atkem bounded model checkingu m´a prov´est p´ar krok˚ u zpˇet (backtrack()) pro zverifikov´ an´ı cel´eho okol´ı chyby. Druh´ ym krokem je pˇrehr´an´ı z´aznamu cesty pomoc´ı LoadCurChoice, navigace stavov´ ym prostorem konˇc´ı po vygenerov´an´ı posledn´ıho stavu zaznamenan´e cesty. Druhou moˇznost´ı je vyuˇzit´ı listeneru pro z´aznam cesty RecordTrace, jehoˇz z´aznam cesty tak´e konˇc´ı v podezˇrel´em stavu. Potom se JPF spust´ı s novou prohled´avac´ı strategi´ı ReplaySearchHeurisicBMC, kter´a vykon´av´a navigaci stavov´ ym prostorem pomoc´ı zaznamenan´e cesty. Jedn´ a se o modifikaci prohled´avac´ı strategie ReplaySearchHeurisic. Rozd´ıl spoˇc´ıv´ a v doimplementov´ an´ı funkce, kter´a po ukonˇcen´ı navigace stavov´ ym prostorem umoˇznuje spustit bounded model checking. Strategie obsahuje dalˇs´ı nastaven´ı urˇcen´ a pro bounded model checking, nastaven´ı slouˇz´ı k urˇcen´ı poˇc´ateˇcn´ıho stavu bounded model checkingu, k urˇcen´ı hloubky prov´adˇen´ı generov´an´ı stavov´eho prostoru, atd. Proto, aby bounded model checking slouˇzil k u ´ˇcelu ovˇeˇren´ı opravy, je tˇreba verifikovat specifick´e vlastnosti chov´ an´ı syst´emu v okol´ı chyby. K tomuto u ´ˇcelu jsou implementov´any dalˇs´ı listenery, kter´e sleduj´ı poˇzadovan´e vlastnosti. Pˇrilinkovan´e listenery k bˇehu programu v JPF sleduj´ı poˇzadovanou vlastnost od zaˇc´atku bˇehu aˇz do jeho konce. Tento mechanizmus v pˇr´ıpadˇe bounded model checkingu nen´ı ˇz´adouc´ı. Napˇr´ıklad pokud listener slouˇz´ı k sledov´an´ı pˇr´ıstup˚ u ke sd´ılen´e promˇenn´e, nen´ı c´ılem zaznamen´ avat veˇsker´e pˇr´ıstupy ke sd´ılen´e promˇenn´e, ale pouze pˇr´ıstupy v okol´ı chyby. Je snahou sledovat pouze ty pˇr´ıstupy, kter´e mohou m´ıt vliv na detekovanou chybu. C´ılem je zapnout funkci listener˚ u aˇz pˇri bounded model checkingu a ne jiˇz pˇri pr˚ uchodu stavov´ ym prostorem pomoc´ı prohled´ avac´ı strategie. Doc´ılen´ı tohoto mechanizmu si vyˇzaduje pˇrid´ an´ı parametru (zaˇc´ atku verifikace) do listeneru. Tento pˇr´ıznak mus´ı b´ yt moˇzn´e nastavit pomoc´ı vyhled´ avac´ı strategie a jeho pˇr´ıznak pˇred´an do pˇrilinkovan´ ych listener˚ u. Implementace tohoto mechanizmu si vyˇzaduje z´ asah do navrˇzen´eho rozhran´ı mezi vyhled´avac´ımi strategiemi a listenery.
ReplayTraceAndBoundedModelChecking. Jak bylo zm´ınˇeno v´yˇse, modifikac´ı prohled´ avac´ı strategie ReplaySearchHeuristic je moˇzn´e prov´adˇet bounded model checking po pr˚ uchodu stavov´ ym prostorem do podezˇrel´eho stavu. Jedn´a se o strategii ReplaySearchHeuristicBMC, kter´ a obsahuje rozˇs´ıˇren´ı nastaven´ı parametr˚ u o parametry bounded model checking: u, o kter´e se m´a strategie vr´atit pˇred spuˇstˇevut.replay search.bmcBackStep – poˇcet krok˚ n´ım bounded model checkingu, 34
vut.replay search.bmcStartDepth – explicitn´ı urˇcen´ı hloubky, ze kter´e se zaˇc´ın´a prov´adˇet bounded model checking, explicitn´ı urˇcen´ı hloubky na cestˇe, kde se zaˇc´ın´a prov´adˇet bounded model checking, (pokud je hodnota rovna −1, bounded model checking zaˇc´ın´a na konci zaznamenan´e cesty), vut.replay search.bmcMaxDepth – maxim´aln´ı hloubka prov´adˇen´ı bounded model checkingu (verifikace m˚ uˇze skonˇcit i v menˇs´ı hloubce – konec programu). Do prohled´ avac´ı strategie byly tedy pˇrid´any zm´ınˇen´e parametry, kter´e ˇr´ıd´ı navigaci stavov´ ym prostorem a n´ asledn´e vykon´an´ı bounded model checkingu. Zadan´e parametry urˇc´ı, kde skonˇc´ı navigace a zaˇcne verifikace, resp. zp˚ usob´ı generovov´an´ı a vykon´av´an´ı vˇsech n´asledn´ık˚ u stav˚ u, kter´e maj´ı b´ yt provedeny. Prohled´avac´ı strategie se ˇr´ıd´ı pomoc´ı jiˇz popsan´ ych heuristik, ty jsou tak´e souˇc´ast´ı nastaven´ı vstupn´ıch parametr˚ u. Prozat´ım jsou implementov´ any pouze dva prohled´avac´ı mechanizmy BF S – HeuristicBFS VUT a DF S – HeuristicDFS VUT.
5.2.1
Pˇ r´ıklad na Bounded Model Checking
Pro uk´ azku funkˇcnosti bounded model checkingu byl zvolen pˇr´ıklad Bank Account [11]. Jedn´a se o vzorov´ y pˇr´ıklad, kter´ y je implementov´an jako program s v´ıce vl´akny. Pouˇz´ıv´a se pro demonstraci soubˇeˇzn´eho pˇr´ıstupu ke sd´ılen´e promˇenn´e pomoc´ı v´ıce vl´aken. Soubˇeˇzn´ y pˇr´ıstup m˚ uˇze zp˚ usobit chybu v programu – data race. Tento pˇr´ıklad je pouˇzit i jako vzorov´ y v projektu SHADOWS pro opravy chyby – data races. Jednou moˇznost´ı, jak vyuˇz´ıt bounded model checking spoˇc´ıv´ a v urˇcen´ı, zda v programu opravdu v dan´em m´ıstˇe dojde k chybˇe nebo zda se jedn´ a pouze o false alarm. Data race – je chyba, kter´a vznik´a u soubˇeˇzn´eho pˇr´ıstupu dvou vl´ aken ke sd´ılen´e promˇenn´e, pˇriˇcemˇz jedno vl´akno se snaˇz´ı o z´apis do sd´ılen´e promˇenn´e. Probl´em nast´ av´ a v pˇr´ıpadˇe nekonzistence pˇreˇcten´ ych a uloˇzen´ ych dat. Program Bank Account obsahuje dvˇe tˇr´ıdy. Hlavn´ı tˇr´ıdou je tˇr´ıda Bank, kter´a vytv´ aˇr´ı a spouˇst´ı dalˇs´ı vl´ akna. Tato vl´ akna reprezentuj´ı jednotliv´e u ´ˇcty – tˇr´ıda Account. Kaˇzd´e vl´akno m˚ uˇze simulovat r˚ uzn´e operace nad u ´ˇcty. Kaˇzd´a z operac´ı nad u ´ˇcty je ukonˇcena a vol´an´ım metody Service() z tˇr´ıdy Bank. Zdrojov´ y k´od metody je na obr. 5.7. Metoda m´ dva parametry: Id je identifikace u ´ˇctu a sum reprezentuj´ıc´ı celkov´ y obnos transakce. public static void Service(int id, int sum) { // operace s~obnosem na~ucte accounts[id].Balance += sum; // operace s~celkovym obnosem v~bance Bank_Total += sum; }
Obr´ azek 5.7: Zdrojov´ y k´od metody z tˇr´ıdy Bank Na prvn´ı pohled uveden´ y zdrojov´ y k´od neobsahuje chybu. Ale probl´em nast´av´a pˇri zmˇenˇe celkov´e ˇc´ astky v bance (Bank Total). Program´ator se mylnˇe domn´ıv´a, ˇze uveden´ a operace se prov´ ad´ı jako atomick´ a. Pˇri pˇrevodu do mezik´odu, kter´ y se posl´eze vykon´av´ a, m´a tato jednoduch´ a operace (pˇriˇcten´ı) ˇctyˇri Java byte-code instrukce: (1) z´ısk´an´ı hodnoty Bank Total, (2) z´ısk´ an´ı hodnoty sum, (3) seˇcten´ı hodnot a (4) uloˇzen´ı nov´e hodnoty Bank Total. Probl´em tedy nast´ av´ a pokud zadanou operaci prov´ad´ı dvˇe vl´akna najednou. Pokud si obˇe vl´ akna naˇctou hodnotu Bank Total, aktualizuj´ı jej´ı hodnotu a posl´eze zap´ıˇs´ı novou
35
hodnotu sekvenˇcnˇe. Druh´ y z´ apis do Bank Total pˇrep´ıˇse aktualizovanou hodnotu prvn´ım vl´aknem, a t´ım doch´ az´ı ke ztr´ atˇe informace a k chybˇe ve v´ ypoˇctu. C´ılem bounded model checkingu je nyn´ı ovˇeˇrit, ˇze v uveden´em m´ıstˇe programu m˚ uˇze opravdu doj´ıt k TrueRace“. Uveden´e m´ısto programu je povaˇzov´ano za podezˇrel´e. ” Nejprve se provede bˇeh programu s pˇrilinkov´an´ım listeneru pro z´aznam cesty. Jedn´ a se o testov´ y pˇr´ıklad, je moˇzn´e prov´est nejprve z´aznam cel´eho bˇehu programu pomoc´ı SaveCurChoice. Ze z´ aznamu listeneru je vidˇet v jak´e hloubce a v kter´em bˇehu se nach´ az´ı podezˇrel´ y stav, kter´ y m˚ uˇze zp˚ usobit probl´em. Tato hloubka a cesta je poznamenan´a do souboru. D´ ale jsou aplikov´ any listenery LoadCurChoice a RecordTrace, kter´e jsou vyuˇzity pro zaznamen´ an´ı cesty do poˇzadovan´e hloubky. Druh´ ym krokem je proveden´ı pˇrehr´an´ı uloˇzen´e cesty, kter´a vede do podezˇrel´eho stavu. K proveden´ı je pouˇzita prohled´ avac´ı strategie ReplayTraceHeuristicBMC a d´ale je pˇrilinkov´an nov´ y listener Races, kter´ y je navrˇzen pro z´aznam jednotliv´ ych pˇr´ıstup˚ u k podezˇrel´e promˇenn´e. Promˇenn´ a je identifikov´ana podle sv´eho um´ıstˇen´ı (bal´ıˇcek + tˇr´ıda) a identifik´atoru promˇenn´e. V tomto pˇr´ıpadˇe je podezˇrelou promˇenou Bank Total. Listener Races zaˇc´ın´ a uchov´ avat informace o pˇr´ıstupu ke sd´ılen´e promˇenn´e v okamˇziku spuˇstˇen´ı bounded model checkingu. Po kaˇzd´e proveden´e instrukci se kontroluje, zda neˇslo o instrukci pˇr´ıstupu ke sledovan´e promˇenn´e. Pokud doˇslo k pˇr´ıstupu k promˇenn´e, zaznamenaj´ı se n´ asleduj´ıc´ı informace: hloubka – aktu´aln´ı vl´akno – aktu´aln´ı metoda – stav syst´emu – ˇ ast z´ typ instrukce. C´ aznamu se zaznamenan´ ymi informacemi je na obr. 5.8. Z tˇechto informac´ı lze na z´ avˇer vyˇc´ıst, zda doˇslo k TrueRace“. ” First access: Depth:threadName@methodName: StepID-insn 33:[email protected]:67-getstatic 33:[email protected]:67-getstatic 33:[email protected]:67-putstatic ------------------------------------------------------------34:[email protected]:70-getstatic 34:[email protected]:70-putstatic 34:[email protected]:70-getstatic 34:[email protected]:70-putstatic 34:[email protected]:71-getstatic 34:[email protected]:71-putstatic ...
ˇ ast v´ Obr´ azek 5.8: C´ ystupu z listeneru Races pro ovˇeˇren´ı race Cel´ y proces pˇrehr´ an´ı cesty, bounded model checking a vyhodnocen´ı specifikace je zn´azornˇen na obr. 5.9. Obr´ azek zn´ azorˇ nuje pouze ˇc´ast cel´eho grafu, kter´ y reprezentuje generovan´ y stavov´ y prostor. Nejprve doˇslo k navigaci stavov´ ym prostorem do podezˇrel´eho stavu. Z podezˇrel´eho stavu se rozgenerov´ av´ a stavov´ y prostor a z´aroveˇ n se pomoc´ı listeneru ukl´adaj´ı informace o pˇr´ıstupu ke sd´ılen´e promˇenn´e. Nakonec byly ruˇcnˇe vyhodnoceny zaznamenane informace pomoc´ı listeneru. Na grafu je ˇcervenˇe uveden podezˇrel´ y stav, ze kter´eho byl ˇ zah´ajen bounded model checking. Cernˇe jsou vybarveny ty stavy, ve kter´ ych byl detekov´ an TrueRace“. ” Cel´ y proces pˇrehr´ an´ı cesty (bounded model checking a vyhodnocen´ı specifikace) je zn´ azornˇen na obr. 5.9. Obr´ azek zn´ azorˇ nuje pouze ˇc´ast cel´eho grafu, kter´ y reprezentuje generovan´ y stavov´ y prostor. Nejprve doˇslo k navigaci stavov´ ym prostorem do podezˇrel´eho 36
stavu. Z podezˇrel´eho stavu se rozgenerov´av´a stavov´ y prostor a z´aroveˇ n se pomoc´ı listeneru ukl´adaj´ı informace o pˇr´ıstupu ke sd´ılen´e promˇenn´e. Nakonec byly ruˇcnˇe vyhodnoceny zaznamenan´e informace pomoc´ı listeneru. V grafu je oznaˇcen podezˇrel´ y stav, ze kter´eho byl ˇ zah´ajen bounded model checking. Cernˇ e jsou vybarveny ty stavy, ve kter´ ych byl detekov´ an TrueRace“. ”
Obr´ azek 5.9: Graf bounded model checkingu a detekce TrueRace
5.3
Modifikace Replay trace pro projekt SHADOWS
Posledn´ı implementaˇcn´ı ˇc´ ast se zab´ yv´a u ´pravou strategie Record&Replay trace pro vyuˇzit´ı v projektu SHADOWS. Nahr´ av´ an´ı cesty programu se jiˇz neprov´ad´ı pomoc´ı JPF, ale mimo model checker. Pro z´ aznam cesty se vyuˇz´ıv´a n´astroj ConTest, kter´ y byl jiˇz zm´ınˇen na zaˇc´ ata se o n´astroj, pomoc´ı kter´eho se detekuj´ı a posl´eze l´eˇc´ı nalezen´e ku pr´ace v kapitole 2. Jedn´ chyby v programu. IBM ConTest je testovac´ı n´astroj, kter´ y prov´ad´ı instrumentaci Java byte-codu programu. ConTest obsahuje tak´e listenerovou architekturu a umoˇzn ˇuje zanesen´ı ˇsumu do programu pro lepˇs´ı odhalov´ an´ı chyb vznikl´ ych soubˇeˇznost´ı. Instrumentace k´odu spoˇc´ıv´ a ve vkl´ad´an´ı byte-code instrukc´ı do byte-codu monitorovan´eho programu. Pomoc´ı tˇechto vloˇzen´ ych instrukc´ı je moˇzn´e pˇrilinkov´avat listenery do bˇehu programu, zan´aˇset do programu ˇsum a dalˇs´ı. Na architektuˇre listener˚ u je zaloˇzen i mechanizmus pro detekci a n´aslednou opravu chyb v programu. Pomoc´ı tˇechto listener˚ u je moˇzn´e z´ıskat r˚ uzn´e informace o vykon´av´an´ı programu pˇr´ımo za bˇehu. Instrumentovan´ y k´ od programu se spouˇst´ı v bˇeˇzn´em Java virtu´aln´ım stroji. Pomoc´ı instrumentace a parametr˚ u se za bˇehu programu pˇrilinkov´avaj´ı poˇzadovan´e listenery ConTestu, kter´e vykon´ avaj´ı zadan´e ud´alosti. ConTest tedy m˚ uˇze stejn´ ym zp˚ usobem jako JPF pomoc´ı listener˚ u sledovat urˇcit´e vlastnosti nebo ˇc´asteˇcnˇe modifikovat prov´adˇen´ı programu za bˇehu.
37
Z´amˇerem je zaznamen´ avat cestu programu pˇri jeho prov´adˇen´ı s pˇrilinkovan´ ym ConTestem. Po aplikaci opravy ConTestem prov´est v okol´ı opravy bounded model checking v JPF a ovˇeˇrit korektnost opravy. C´ılem tedy je pˇrehr´at zaznamenanou cestu ConTestem v JPF. ast zaznamenan´e cesty z ConTestu. Z´aznam cesty se prov´ad´ı poNa obr. 5.10 je uvedena ˇc´ moc´ı speci´ aln´ıho listeneru, kter´ y byl pro tento u ´ˇcel navrˇzen. Listener zaznamen´av´a vˇsechny moˇzn´e informace, kter´e lze z ConTestu o bˇehu programu z´ıskat. Z´aznam cesty a implementace zm´ınˇen´eho listeneru nen´ı souˇc´asti diplomov´e pr´ace, ale je pˇrevzat z projektu SHADOWS. 3:main(java.lang.Thread@19134f4):BASICBLOCK:.../bank Bank.java () 14-14,20-20,24-24 1 9:main(java.lang.Thread@19134f4):THREAD_BEGIN:.../bank Bank.java main(java.lang.String[]) 35 1 10:main(java.lang.Thread@19134f4):BASICBLOCK:.../bank Bank.java main(java.lang.String[]) 35-35 1 .... 22:Thread-4(bank.Account@f4a24a):THREAD_END:null 23:Thread-3(bank.Account@17182c1):BASICBLOCK:.../bank Bank.java Service(int,int) 85-85,87-88 1 33:Thread-3(bank.Account@17182c1):BASICBLOCK:.../bank Account.java run() 54-54 2 34:Thread-3(bank.Account@17182c1):BASICBLOCK:.../bank Account.java run() 54-54 1 34:Thread-3(bank.Account@17182c1):BASICBLOCK:.../bank Account.java run() 62-63 1 ... 531:main(java.lang.Thread@19134f4):BASICBLOCK:.../bank Bank.java main(java.lang.String[]) 73-73 1 531:main(java.lang.Thread@19134f4):BASICBLOCK:.../bank Bank.java main(java.lang.String[]) 77-77 1 533:main(java.lang.Thread@19134f4):THREAD_END:null
ˇ ast z´ Obr´ azek 5.10: C´ aznamu cesty programu pomoc´ı ConTest listeneru Z´aznam cesty obsahuje informace o aktu´aln´ım vl´aknˇe (jm´eno, tˇr´ıda, index), dalˇs´ı informac´ı je ud´ alost ConTestu (bude d´ale rozepsan´e), informace o zdrojov´em k´odu (um´ıstˇen´ı a jm´eno zdrojov´eho souboru, aktu´ aln´ı metoda), posledn´ı informac´ı je rozsah ud´alosti ConTest a poˇrad´ı byte-code instrukce na ˇr´adku, kterou dan´a ud´alost ConTestu zaˇc´ın´a. Z hlediska pˇrehr´ an´ı cesty je pro n´as d˚ uleˇzit´e zaznamen´avat m´ısta nedeterminismu, kter´ a urˇcuj´ı smˇer dalˇs´ıho prov´ adˇen´ı programu. N´astroj ConTest program rozdˇeluje na tzv. BasicBlocky. BasicBlock tvoˇr´ı ˇc´ ast programu, ve kter´e nedoch´az´ı k nedeterminismu. Na uveˇ ısla na konci den´em z´ aznamu cesty programu je vidˇet nˇekolik BasicBlock˚ u s r˚ uznou d´elkou. C´ kaˇzd´eho ˇr´ adku z´ aznamu odpov´ıdaj´ı ˇc´ısl˚ um ˇr´adk˚ u ve zdrojov´em k´odu programu odkud – kam sah´ a BasicBlock. Posledn´ım ˇc´ıslem z´aznamu cesty je poˇradov´e ˇc´ıslo prvn´ı instrukce BasicBlock na zdrojov´em ˇr´ adku k´odu. Dalˇs´ı zaznamenanou ud´ alost´ı ConTestu je zaˇc´atek vl´akna Thread Begin nebo ukonˇcen´ı vl´akna Thread End. Tyto ud´ alosti jsou tak´e vznikem nedeterminismu a jsou tedy potˇrebn´e v z´aznamu cesty. V z´ aznamu cesty je patrn´ y rozd´ıl mezi informacemi z´ıskan´ ymi z JPF a informacemi, kter´e jsou z´ısk´ any z ConTestu. Dalˇs´ı odliˇsnost´ı je rozd´ıl mezi BasicBlocky ConTestu a stavy v JPF. BasicBlocky v podstatˇe tvoˇr´ı jednotliv´e stavy a pˇrechody v syst´emu, ty jsou ovˇsem odliˇsn´e od stav˚ u a pˇrechod˚ u v JPF. Po z´ısk´ an´ı z´ aznamu cesty z ConTestu je tˇreba danou cestu pˇrehr´at v JPF. Pro pˇrehr´ an´ı cesty je tˇreba naj´ıt koresponduj´ıc´ı informace v bˇehu programu pomoc´ı JPF. Po z´ısk´ an´ı n´avaznosti mezi uloˇzen´ ymi informacemi a informacemi za bˇehu programu je moˇzn´e aplikovat strategii pro navigaci stavov´ ym prostorem a n´asledn´ y bounded model checking. Pro pˇrehr´ an´ı koresponduj´ıc´ı cesty v JPF jsou dvˇe moˇznosti. Pˇri prvn´ı moˇznosti se v JPF spust´ı p˚ uvodn´ı program (bez instrumentace ConTestu) a vyhledaj´ı se souhlasn´e informace se zaznamenanou cestou ConTestem. Tyto informace slouˇz´ı k navigaci stavov´ ym prostorem. Druhou moˇznost´ı je pˇrehr´ an´ı instrumentovan´eho k´odu v JPF. Instrumentace ConTestem sice pˇrid´ av´ a do byte-codu programu dalˇs´ı instrukce, ale bˇeh programu se prov´ad´ı pomoc´ı 38
standardn´ıho virtu´ aln´ıho stroje. JPF je speci´aln´ım virtu´aln´ım strojem a je tedy teoreticky moˇzn´e pˇrehr´ an´ı instrumentovan´eho k´od.
5.3.1
Replay trace pomoc´ı p˚ uvodn´ım k´ odu
Pˇri prozkoum´ av´ an´ı prvn´ı moˇznosti byl postup n´asleduj´ıc´ı. Postupnˇe se specifikovaly informace z´ıskan´e ze z´ aznamu cesty a hledaly se odpov´ıdaj´ıc´ı instance tˇechto informac´ı v JPF. Protoˇze JPF vezme p˚ uvodn´ı byte-code instrukce a transformuje je na vlastn´ı byte-code instrukce, doch´ az´ı ke zmˇenˇe nejen instrukce, ale tak´e se mˇen´ı parametry a informace, kter´e lze z´ıskat. Ke vˇsem zaznamenan´ ym informac´ım z ConTestu byly nalezeny koresponduj´ıc´ı informace aˇz na identifikaci instrukce. V ConTestu se jednotliv´e byte-code instrukce identifikuj´ı pomoc´ı ˇc´ısla ˇr´adku ve zdrojov´em k´ odu (tato informace je v JPF obsaˇzena) a pomoc´ı poˇrad´ı instrukce na ˇr´adku, tuto informaci se nepodaˇrilo z´ıskat. Z d˚ uvod˚ u pˇreps´an´ı p˚ uvodn´ıch byte-code instrukc´ı na odpov´ıdaj´ıc´ı JPF instrukce se ztr´ac´ı nˇekter´e informace obsaˇzen´e v p˚ uvodn´ım mezik´odu. Pro z´ısk´ an´ı poˇrad´ı instrukce na ˇr´adku v p˚ uvodn´ım k´odu by byl nutn´ y hlubˇs´ı z´asah do fungov´ an´ı JPF. Poˇzadovan´a informace by se musela z´ıskat v pr˚ ubˇehu tranformace p˚ uvodn´ıch instrukc´ı na instrukce JPF. Transformace p˚ uvodn´ıho k´odu na instrukce JPF m´a nˇekolik f´ az´ı. Nejprve dojde k rozdˇelen´ı k´odu na d´ılˇc´ı ˇc´asti jako jsou metody, v dalˇs´ı f´azi se postupnˇe proch´ az´ı jednotliv´e instrukce, a ty se postupnˇe tranformuj´ı na instrukce JPF. Z´ aroveˇ n doch´ az´ı ke zmˇenˇe potˇrebn´ ych parametr˚ u, kter´e kaˇzd´a byte-code instrukce potˇrebuje pro spr´ avnou funkci. V t´eto f´azi doch´az´ı k z´asadn´ı zmˇenˇe. Nelze jiˇz zpˇetnˇe z´ıskat p˚ uvodn´ı informace instrukce. Pro uchov´ an´ı informace, kolik´atou insturkc´ı na ˇr´adku dan´a instrukce je, by bylo tˇreba zas´ahnout do superclass vˇsech JPF instrukc´ı a pˇridat nov´ y parametr. Nastaven´ı tohoto parametru by bylo tˇreba pˇridat do spr´avn´ ych“ konstruktor˚ u JPF instrukc´ı. D´ale by bylo ” nutn´e zas´ ahnout do jendnotliv´ ych ˇc´ast´ı tranformace p˚ uvodn´ıho k´odu na instrukce JPF a na vˇsechna potˇrebn´ a m´ısta zadat nejprve z´ısk´an´ı poˇzadovan´eho parametru a pak jeho pˇred´an´ı do nov´e instrukce JPF. Tento mechanizmus je n´aroˇcn´ y a zp˚ usobil by rozs´ahl´e zmˇeny v JPF. Vzhledem k tomu ,ˇze byte-code instrukce jsou jednou z hlavn´ıch informac´ı, kter´a je potˇrebn´ a pro opˇetovn´e pˇrehr´ an´ı bˇehu programu, byla snaha tento mechanizmus naimplementovat tak, aby byly z´ısk´ any potˇrebn´e informace bez velk´eho z´asahu do JPF. Nicm´enˇe po delˇs´ı dobˇe testov´ an´ı bylo od t´eto moˇznosti upuˇstˇeno a nebyla naimplementov´ana.
5.3.2
Replay trace pomoc´ı instrumentovan´ eho k´ odu
Druhou moˇznost´ı je pˇrehr´ an´ı instrumentovan´eho k´odu pˇr´ımo v JPF. C´ılem je pˇrehr´ at p˚ uvodn´ı Java byte-code bez instrumentace. Je nutn´e se nˇejak´ ym zp˚ usobem s pˇridan´ ymi instrukcemi ConTestu vypoˇr´ adat. Ponech´an´ı instrukc´ı k´odu pˇri verifikaci nen´ı moˇzn´e. Pomoc´ı pˇridan´ ych instrukc´ı ConTestu se volaj´ı r˚ uzn´e moduly ConTestu, kter´e nen´ı moˇzn´e pomoc´ı JPF zverifikovat. Vyˇrazen´ı tˇechto modul˚ u z verifikace pomoc´ı standardn´ıho mechanizmu JPF si vyˇzaduje z´ asah do zdrojov´eho k´odu a zmˇenu metod tˇechto modul˚ u na nativn´ı metody. Nativn´ı metody jiˇz nepodl´ehaj´ı verifikaci. N´astroj ConTest ovˇsem nen´ı moˇzn´e modifikovat a tud´ıˇz nelze dan´ y mechanizmus JPF vyuˇz´ıt. Jinou moˇznost´ı, jak se vypoˇr´ adat s pˇridan´ ymi instrukcemi ConTestu, je jejich pˇreskakov´ an´ı nam´ısto vykon´ an´ı. Princip pˇreskoˇcen´ı (skip) napl´anovan´e instrukce je podobn´ y jako u listeneru LoadCurChoice, kde se z napl´anovan´ ych moˇznost´ı CG provedla pouze jedna moˇznost a ostatn´ı se pˇreskoˇcily. 39
Principem nov´eho listeneru je pˇreskakov´an´ı vˇsech instrukc´ı ConTestu, kter´e byly do bytecodu pˇrid´ any a z´ aroveˇ n pˇreskakov´an´ı vˇsech souvisej´ıc´ıch instrukc´ı (parametr˚ u, n´avratov´ ych hodnot, atd.). Instrumentace ConTestem pˇrid´av´a do k´odu instrukce pro vol´an´ı statick´ ych metod ConTestu. Statick´e metody jsou vol´ any pomoc´ı instrukce invokestatic. Vˇsechny metody ConTestu jsou tedy vol´ any pomoc´ı instrukce invokestatic, nicm´enˇe kaˇzd´a metoda m´a jin´ y poˇcet parametr˚ u a jin´e typy parametr˚ u a n´avratov´e hodnoty. Je tedy nutn´e oˇsetˇrit jak´ekoliv vol´an´ı metody ConTestu a pˇreskoˇcit spr´avn´ y poˇcet byte-code instrukc´ı pˇred a za touto instrukc´ı. Kaˇzd´ a instrukce, kter´ a vol´ a metodu Contestu obsahuje informace o tom jak´a metoda ConTestu se vol´ a a odkud. D´ıky tomu lze pˇresnˇe urˇcit, kter´e instrukce byly pˇrid´any ConTestem. Z´ aroveˇ n tato instrukce obsahuje informaci pˇred kterou p˚ uvodn´ı instrukci byla pˇrid´ana a tak´e informaci o p˚ uvodn´ı instrukci (na jak´em ˇr´adku k´odu se nach´az´ı a kolik´atou instrukc´ı ˇr´adku je). C´ılem je dan´e instrukce bˇehem prov´adˇen´ı programu v JPF pouze pˇreskakovat a ne je zcela vymazat. Nov´ y listener SkipConTestInstruction je zaloˇzen na prohled´av´an´ı napl´anovan´ ych instrukc´ı a detekc´ı instrukc´ı ConTestu s jejich parametry. Po jejich detekci dojde k nastaven´ı jejich pˇr´ıznaku na pˇreskoˇcen´ı pˇri vykon´av´an´ı napl´anovan´ ych instrukc´ı. ConTest vˇzdy pˇrid´ av´ a instrukci pro vol´an´ı statick´e metody, nicm´enˇe kaˇzd´a metoda m˚ uˇze m´ıt jin´ y poˇcet parametr˚ u, a proto je potˇreba urˇcit, jak´a metoda m´a b´ yt vol´ana. V listeneru SkipConTestInstruction doch´az´ı pouze k detekci, zda se jedn´a o instrukci pˇridanou ConTestem. Urˇcen´ı poˇctu parametr˚ u volan´e metody a tedy poˇctu pˇreskakovan´ ych instrukc´ı doch´ az´ı ve tˇr´ıdˇe Skipping. Jednotliv´e typy metod, kter´e mohou b´ yt pomoc´ı ConTestu pˇrid´ any, jsou obsaˇzeny v intern´ı dokumentaci ConTestu. Bˇehem implementace pˇreskakov´ an´ı jednotliv´ ych typ˚ u metod se objevil n´asleduj´ıc´ı probl´em. Bˇehem instrumentace zdrojov´eho k´odu programu nedoch´az´ı pouze k pˇrid´an´ı dalˇs´ıch instrukc´ı ConTestu, ale tak´e ke zmˇenˇe urˇcit´ ych byte-code instrukc´ı. Zmˇena se t´ yk´a instrukc´ı pro vl´akna (start, stop, yield, join, atd.). ConTest p˚ uvodn´ı instrukce, kter´e pracuj´ı s vl´akny, nahradil vol´ an´ım vlastn´ıch metod, kter´e maj´ı dan´e vl´akno jako parametr. K proveden´ı p˚ uvodn´ı instrukce dojde bˇehem vykon´an´ı metody ConTestu. Pokud jsou tyto metody v JPF pˇreskakov´ any, p˚ uvodn´ı instrukce se neprovedou a nast´av´a probl´em. Je tedy tˇreba implementovat mechanizmus, pomoc´ı kter´eho se doc´ıl´ı proveden´ı, resp. obnoven´ı p˚ uvodn´ıch instrukc´ı, kter´e byly bˇehem instrumentace k´odu odstranˇeny a spr´avnˇe je zpˇet zaˇclenit do k´ odu. Z principu fungov´an´ı JPF se nab´ızej´ı dvˇe moˇznosti, jak vytvoˇrit poˇzadovanou instrukci: • Byte-code instrukce JPF. Princip spoˇc´ıv´a v pˇretransformov´an´ı instrukce ConTestu na p˚ uvodn´ı instrukci zdrojov´eho k´odu nebo vytvoˇren´ı nov´e instrukce JPF. Vˇzdy na zaˇc´ atku spuˇstˇen´ı programu v JPF dojde k transformaci p˚ uvodn´ıch bytecode instrukc´ı na byte-code instrukce JPF. JPF obsahuje mechanizmus pro vytv´aˇren´ı vlastn´ıch instrukc´ı z p˚ uvodn´ıch instrukc´ı. Pro transformaci instrukce ConTestu na jinou instrukci JPF je potˇreba zn´at informace, kter´e jiˇz instrukce JPF neobsahuj´ı. Pro vytvoˇren´ı resp. transformaci JPF instrukce je zapotˇreb´ı zadat jako parametry odkaz do ConstatPool tabulky (v´ıce informac´ı fungov´ an´ı JVM je uvedeno v [18]). Tento odkaz je zn´am pouze u p˚ uvodn´ıch byte-code instrukc´ı a nen´ı jiˇz k dispozici u instrukc´ı JPF (ty maj´ı vlastn´ı mechanizmus). Mechanizmus vytv´ aˇren´ı resp. modifikace instrukce JPF na jinou bez vyuˇzit´ı
40
naimplementovan´ ych metod by vyˇzadovala velk´ y z´asah do JPF. Z toho d˚ uvodu nen´ı tato moˇznost pro ˇreˇsen´ı probl´emu vyuˇzita. • Standardn´ı byte-code instrukce. Druhou moˇznost´ı je vytvoˇren´ı nov´e byte-code instrukce jeˇstˇe pˇred zmˇenou na instrukce JPF. Instrukce ConTestu se pˇretransformuje nebo se vytvoˇr´ı nov´ a byte-code instrukce m´ısto p˚ uvodn´ı a teprve posl´eze se transformuje na instrukci JPF. Vzhledem ke zmˇenˇe instrukce jeˇstˇe pˇred pˇrevodem na JPF instrukci, jsou k dispozici vˇsechny potˇrebn´e informace pro vytvoˇren´ı nov´e byte-code instrukce. Druh´ a z uveden´ ych moˇznost´ı byla hloubˇeji prostudov´ana. Pro vytvoˇren´ı nov´e funguj´ıc´ı instrukce je tˇreba pˇredat spr´ avn´e odkazy do ConstantPool tabulky, zadat spr´avnˇe parametry a v neposledn´ı ˇradˇe spr´ avnˇe zaˇclenit mezi ostatn´ı instrukce. Tato ˇc´ ast implementace – vytvoˇren´ı nov´e instrukce, nen´ı zcela funkˇcn´ı. Metoda pro vytv´aˇren´ı nov´e instrukce je v rozpracovan´e f´azi. Listener SkipConTestInstruction se tak´e nach´az´ı v rozpracovan´e f´azi. Listener je v tuto chv´ıli schopn´ y pˇreskoˇcit vykon´av´an´ı vˇsech instrukc´ı ConTestu i s jeho parametry, kter´e jsou do k´ odu pˇrid´ any nav´ıc. Avˇsak st´ale neumoˇzn ˇuje nahrazen´ı instrukc´ı ConTestu pro pr´ aci s vl´ akny za p˚ uvodn´ı instrukce. Je tedy moˇzn´e v JPF pˇrehr´at instrumentovan´ y program, kter´ y neobsahuje vl´ akna.
5.4
V´ ysledky a Testy
Funkˇcnost jednotliv´ ych ˇc´ ast´ı implementace listener˚ u a vyhled´av´ac´ıch strategi´ı byla testov´ana bˇehem jejich n´ avrhu a po jejich dokonˇcen´ı. Kaˇzd´a z v´ yˇse uveden´ ych ˇc´ast´ı implementace si vyˇzadovala jin´ y v´ ybˇer testov´ ych program˚ u. Testov´e programy byly vyb´ır´any podle poˇzadavk˚ u, kter´e maj´ı jednotliv´ı listenery a strategie splˇ novat. Nˇekter´e z testov´ ych pˇr´ıklad˚ u jsou souˇc´ ast´ı pˇriloˇzen´eho DVD media. Pro zhodnocen´ı dosaˇzen´ ych v´ ysledk˚ u byly vytvoˇreny r˚ uzn´e bˇehy vybran´ ych program˚ u. Jednotliv´e bˇehy se vykon´ av´ aly v uveden´ ych n´astroj´ıch: bˇeˇzn´ y Java virtu´aln´ı stroj (JVM), Java PathFinder (JPF) a ConTest. Z´ıskan´e informace z jednotliv´ ych bˇeh˚ u program˚ u jsou posl´eze porovn´ any. Vyhodnocen´ı bˇeh˚ u program˚ u slouˇz´ı k urˇcen´ı ˇcasov´e n´aroˇcnosti ovˇeˇren´ı opravy chyby v programu. V kaˇzd´em z uveden´ ych n´astroj˚ u trv´a bˇeh programu r˚ uznou dobu a z hlediska verifikace, kter´a je typicky n´aroˇcn´a na ˇc´as, je porovn´an´ı tˇechto bˇeh˚ u zaj´ımav´e. Jednotliv´e testy, kter´e zde budou uvedeny je moˇzn´e opˇetovnˇe spustit, jsou souˇc´ast´ı pˇriloˇzen´eho DVD. Pouze n´ astroj ConTest nen´ı volnˇe ˇs´ıˇriteln´ y a pˇriloˇzen´e DVD tedy obsahuje pouze v´ ysledky tˇechto test˚ u. Informace o ConTestu je moˇzn´e z´ıskat na [16]. Prvn´ım pˇr´ıkladem je jiˇz zmiˇ novan´ y program Bank Account uveden´ y v kapitole 5.2.1. Jeho zdrojov´ y k´ od je tak´e souˇca´sti pˇriloˇzen´eho DVD. Pˇr´ıklad je zaloˇzen na vz´ajemn´em prokl´ad´ an´ı jednotliv´ ych vl´ aken, kter´e simuluj´ı jednotliv´e u ´ˇcty v bance (Account). D´ıky vz´ajemn´emu prokl´ ad´ an´ı a pˇr´ıstupu do sd´ılen´e promˇenn´e je moˇzn´e pomoc´ı tohoto pˇr´ıkladu pozorovat vliv nedeterminismu na rychlost prov´adˇen´ı programu. Aplikace je vhodn´ ym pˇr´ıkladem programu s nutnost´ı pl´ anov´an´ı prokl´ad´an´ı jednotliv´ ych instrukc´ı r˚ uzn´ ych vl´aken. Pro testov´e u ´ˇcely bylo v programu vytvoˇreno deset vl´aken simuluj´ıc´ıch jednotliv´e u ´ˇcty. D´ıky nez´ avislosti vykon´ av´ an´ı jednotliv´ ych vl´aken na sobˇe vznik´a velk´e mnoˇzstv´ı moˇzn´ ych prokl´ad´ an´ı instrukc´ı jednotliv´ ych vl´aken. Druh´ ym pˇr´ıkladem je velice jednoduch´ y program SkipInstruction. Jedn´a se o u ´mˇele vytvoˇren´ y program pro testovn´ an´ı funkˇcnosti listeneru a pro pˇreskakov´an´ı instrukc´ı Con41
Testu, pˇridan´ ych do programu pomoc´ı instrumentace. Program byl vytvoˇren za u ´ˇcelem otestov´ an´ı pˇreskakov´ an´ı vˇsech moˇzn´ y instrukc´ı, kter´e mohou b´ yt ConTestem do programu pˇrid´any. ConTest vkl´ ad´ a instrukce pˇri vytv´aˇren´ı/zmˇenˇe promˇenn´ ych v programu, pˇri vol´ an´ı metod v programu a samozˇrejmˇe u vol´an´ı metod vl´aken (start(),stop(),join(), atd.). Program tedy obsahuje r˚ uzn´e typy promˇenn´ ych jako integer, double, tyto promˇenn´e mohou b´ yt statick´e nebo nestatick´e (instance promˇenn´ ych). Stejnˇe taky i vol´an´ı metod m˚ uˇze nab´ yvat r˚ uzn´ ych typ˚ u (statick´e, ...) a jednotliv´e metody mohou m´ıt r˚ uzn´e typy parametr˚ u. umˇern´e V´ ysledky test˚ u, kter´e jsou uveden´e v tabulk´ach 5.1 a 5.2 byly z´ısk´any jako pr˚ hodnoty ˇcas˚ u bˇehu program˚ u. Kaˇzd´ y typ bˇehu byl spuˇstˇen tis´ıckr´at a z namˇeˇren´ ych ˇcas˚ u byla vytvoˇrena pr˚ umern´ a hodnota. Bˇehy programu byly spuˇstˇeny na osobn´ım poˇc´ıtaˇci: Intel Centrino Duo, T2250 1.73GHz, 1GB RAM.
5.4.1
Rychlost bˇ ehu programu ve pouˇ zit´ ych n´ astroj´ıch
C´ılem n´ asleduj´ıc´ıho testov´ an´ı je porovnat rychlost jednotliv´ ych bˇeh˚ u programu v n´ asleduj´ıc´ıch n´ astroj´ıch. Nejprve byl program spuˇstˇen v obyˇcejn´em Java virtu´aln´ım stroji (JVM). Pr˚ umˇern´ a d´elka bˇehu v JVM je br´ana jako refernˇcn´ı. N´aslednˇe byly programy spuˇstˇeny v model checkeru Java PathFinder (JPF), kter´ y byl nastaven pro vykon´an´ı jednoho n´ ahodn´eho bˇehu programu. Pak byla vytvoˇrena instrumentace k´odu programu pomoc´ı n´astroje ConTest a program opˇet spuˇstˇen v JVM s instrumentac´ı. Posledn´ım testem bˇehu bylo pˇrehr´ an´ı instrumentovan´eho k´odu v JPF. Tento test byl spuˇstˇen pouze pro pˇr´ıklad SkipInstruction, kter´ y obsahuje pouze ty instrumentovan´e instrukce, kter´e je moˇzn´e v t´eto f´azi implementace pˇreskakovat. Pr˚ umˇern´e hodnoty namˇeˇren´ ych ˇcas˚ u bˇehu program˚ u jsou uvedeny v tabulce 5.1. Tabulka 5.1: Bˇeh zvolen´ ych pˇr´ıklad˚ u v pouˇzit´ ych n´astroj´ıch (JVM, JPF, ConTest) Bank Account
SkipInstruction
JVM
217 ms
1 ×
50 ms
1 ×
JPF (RandomSearch)
324 ms
1,5 ×
596 ms
11,9 ×
JVM s ConTestem
217 ms
1 ×
58 ms
1,2 ×
—
674 ms
13,5 ×
JPF s ConTest
—
Z namˇeˇren´ ych ˇcas˚ u v r˚ uzn´ ych n´astroj´ıch je vidˇet, ˇze JPF nen´ı navrˇzen´ y pro jednoduch´ y bˇeh programu. Pˇri simulov´an´ı bˇehu programu v JPF doch´az´ı ke znaˇcn´emu zpomalen´ı cel´e aplikace. Oproti tomu bˇeh programu, kter´ y byl instrumentov´an pomoc´ı ConTestu nen´ı tolik zpomalen. Je ovˇsem nutn´e br´at v potaz fakt, ˇze pˇri testov´em bˇehu nebylo instrumentace vyuˇzito (ConTest nepˇridal k bˇehu programu ˇz´adny listener ani nezasahoval do bˇehu aplikace). Posledn´ım z uveden´ ych ˇcas˚ u je pˇrehr´an´ı instrumentovan´eho k´odu v JPF. Z dosaˇzen´ ych ˇcas˚ u je vidˇet, ˇze pˇri pˇrehr´av´an´ı programu v JPF s instrumentac´ı jiˇz k velk´emu zpoˇzdˇen´ı nedoch´ az´ı. To je v´ yhodn´ ym faktem pro dalˇs´ı v´ yvoj. Je moˇzn´e verifikovat p˚ uvodn´ı zdrojov´ y k´ od programu nebo instrumentovan´ y k´od za stejnou cenu. Z uveden´e tabulky tak´e vypl´ yv´a z´avˇer, ˇze doba prov´adˇen´ı bˇehu programu v JPF znaˇcnˇe z´aleˇz´ı na struktuˇre programu a na typu nedeterminismu. Pokud program obsahuje velk´e mnoˇzstv´ı nedeterminismu a prokl´ad´an´ı instrukc´ı, kter´e je potˇreba ˇreˇsit, doch´az´ı ke znaˇcn´emu
42
zpomalen´ı bˇehu programu. U prvn´ıho pˇr´ıkladu Bank Account, kter´ y obsahuje velk´e mnoˇzstv´ı moˇzn´eho prokl´ ad´ an´ı, doch´ az´ı k menˇs´ımu zpomalen´ı aplikace, z d˚ uvodu velk´eho poˇctu nez´avisl´ ych instrukc´ı.
5.4.2
Rychlost metody Record&Replay trace
Dalˇs´ı testov´ an´ı bylo zamˇeˇreno na zjiˇstˇen´ı rychlosti zaznamen´av´an´ı a pˇrehr´an´ı cesty programu v JPF nebo ConTestu. Testy byly opˇet prov´ adˇeny nad stejn´ ymi programy jako pˇredchoz´ı. Referenˇcn´ı rychlost prov´adˇen´ı z˚ ust´ av´ a stejn´ a – jednoduch´ y bˇeh programu v JVM. Pro testov´an´ı strategie Record&Replay trace byly pouˇzity naipmlementovan´e listenery kapitola 5. Prvn´ı testy bˇehu program˚ u (v tabulce 5.2 oznaˇceny jako SaveChoice v JPF) byly spuˇstˇeny v JPF s listenerem SaveCurChoice, kter´ y bˇehem prov´adˇen´ı programu zaznamen´av´a volby ChoiceGener´ator˚ u. Druh´e testy (Record v JPF I) byly spuˇstˇeny v JPF s listenerem LoadCurChoice a RecordTrace. Pomoc´ı tˇechto test˚ u tedy doch´azelo z´aroveˇ n k pˇrehr´av´an´ı bˇehu aplikace pomoc´ı ChoiceGener´ ator˚ u a z´ aroveˇ n k z´aznamu cesty s byte-code instrukcemi. Tˇret´ı testy (Record v JPF II) byly spuˇstˇeny v JPF pouze s listenerm RecordTrace, nedoch´azelo tedy k navigaci stavov´ ym prostorem pomoc´ı cesty, ale k n´ahodn´emu bˇehu pomoc´ı implementovan´e strategie RandomSearch. Ve ˇctvrt´ ych testech (Record v ConTestu) byla cesta nahr´av´ana pomoc´ı listeneru ConTestu. Posledn´ı dva druhy test˚ u (Replay v JPF I, II) byly opˇet spuˇstˇeny v JPF se strategi´ı pro pˇrehr´ an´ı cesty ReplayTraceHeuristic. U programu Bank Account byl nejprve pˇrehr´ av´ an n´ ahodn´ y bˇeh programu, kter´ y vedl ke korektn´ımu ukonˇcen´ı aplikace. Posledn´ı testy jsou pˇrehr´ av´an´ım chybov´eho bˇehu programu. U druh´eho programu SkipInstruction nedoch´ az´ı k chybov´emu bˇehu programu, a proto nebylo druh´e testov´ an´ı pˇrehr´av´ an´ı cesty zapotˇreb´ı. Namˇeˇren´e ˇcasy bˇehu program˚ u jsou uvedeny v tabulce 5.2.
Tabulka 5.2: Record&Replay trace v JPF a ConTestu Bank Account
SkipInstruction
SaveChoice v JPF
326 ms
1,6 ×
1 028 ms
20,6 ×
Record v JPF I
434 ms
2×
1 258 ms
25,2 ×
Record v JPF II
438 ms
2,1 ×
1 276 ms
25,5 ×
Record v ConTestu
269 ms
1,3 ×
375 ms
7,5 ×
Replay v JPF I
1 135 ms
5,3 ×
648 ms
11,7 ×
Replay v JPF II
1 128 ms
5,2 ×
—
—
Z tabulky jsou opˇet vidˇet rozd´ıln´e pomˇery ˇcas˚ u zvolen´ ych program˚ u. Rozd´ıl v ˇcase pro simulov´an´ı pˇrehr´ av´ an´ı programu v JPF z˚ ust´av´a i u implementovan´e strategie Record&Replay trace. Z tabulky je patrn´e dalˇs´ı zpomalen´ı, kter´e nast´av´a v d˚ usledku nahr´av´an´ı bˇehu programu. Velikost zpomalen´ı nahr´ av´an´ı v JPF je zhruba dvojn´asobn´e oproti n´ahodn´emu bˇehu v JPF. Oproti tomu pomˇer pˇrehr´ av´an´ı cesty oproti zaznamen´av´an´ı cesty je u r˚ uzn´ ych program˚ u odliˇsn´ y. Tento fakt vypl´ yv´a z principu strategie pˇrehr´av´an´ı cesty. Pˇri pˇrehr´av´ an´ı cesty je tˇreba zkontrolovat, kter´e kroky programu koresponduj´ı s uloˇzenou cestou. Pokud program obsahuje velk´e mnoˇzstv´ı nedeterminismu a velk´e mnoˇzstv´ı moˇzn´ ych jednotliv´ ych
43
voleb nedeterminismu, je tˇreba urˇcit koresponduj´ıc´ı cestu z mnoha moˇznost´ı a t´ım doch´ az´ı k vˇetˇs´ımu zpomalen´ı, neˇz pokud se vol´ı pouze ze dvou nebo tˇr´ı moˇznost´ı. Nahr´ av´ an´ı cesty programu pomoc´ı ConTestu, kter´ y nezanamen´av´a vˇsechny vykonan´e instrukce byte-codu, ale pouze m´ısta vˇetven´ı, je rychlejˇs´ı. Je tak´e c´ılem zaznamenat bˇeh programu mimo JPF a v JPF prov´est pouze pˇrehr´an´ı cesty.
44
Kapitola 6
Z´ avˇ er C´ılem diplomov´e pr´ ace bylo navrhnout a posl´eze implementovat metodu pro ovˇeˇren´ı opravy v projektu SHADOWS. Oprava chyb v uvedn´e ˇc´asti projektu SHADOWS se specializuje na chyby v Java programech. Konkr´etnˇe se jedn´a o chyby, kter´e vznikaj´ı v d˚ usledku parelelismu. Pro kontrolu opravy chyby byla zvolena modifikace form´aln´ı metody model checkingu. Nejprve bylo nutn´e nastudovat model checking, jak´e m´a vlastnosti a principy. Po prostudov´ an´ı model checkingu bylo moˇzn´e navrhnout metodu zaloˇzenou na modifikaci model checkingu takov´ ym zp˚ usobem, aby splˇ novala zadan´e poˇzadavky pro ovˇeˇren´ı opravy. Navrˇzen´ a metoda pro ovˇeˇren´ı opravy je zaloˇzena na vykon´av´an´ı bounded model checkingu v okol´ı opravy. Bounded model checking vznikl omezen´ım prov´adˇen´ı verifikace pomoc´ı model checkingu do zadan´e hloubky stavov´eho prostoru. Tato modifikace model checkingu lze pro ovˇeˇrov´ an´ı opravy chyby vyuˇz´ıt. Oprava se vˇenuje chyb´am vznikl´ ym soubˇeˇznost´ı, kter´e jsou zaloˇzeny na zp˚ usobu prokl´ad´an´ı jednotliv´ ych instrukc´ı. T´ım tedy dojde ˇcasem k vykon´ an´ı vˇsech relevantn´ıch instrukc´ı, kter´e mohou m´ıt vliv na opravu. K vykon´an´ı tˇechto relevatn´ıch instrukc´ı vˇetˇsinou doch´az´ı v pˇrijateln´em ˇcase a je tedy moˇzn´e pouˇz´ıt bounded model checking. Nicm´enˇe z´ asadn´ım probl´emem pro vyuˇzit´ı bounded model checkingu v okol´ı chyby je navigace stavov´ ym prostorem do poˇzadovan´eho stavu syst´emu. Pro navigaci stavov´ ym syst´emem existuj´ı r˚ uzn´e strategie, kter´e byly studov´any a z nich byla zvolena strategie Record&Replay trace. Podsatou metody je uloˇzen´ı bˇehu programu, kter´ y vede k chybˇe a n´asledn´e pˇrehr´ an´ı tohoto bˇehu ve zvolen´em model checkeru. Uloˇzen´a cesta tedy slouˇz´ı k navigaci stavov´ ym prostorem do poˇzadovan´eho stavu, ze kter´eho je vykon´an bounded model checking pro zverifikov´ an´ı poˇzadovan´ ych vlastnost´ı. Diplomov´ a pr´ ace obsahuje jednotliv´e ˇc´asti implementace metody Record&Replay trace a strategie pro vykon´ an´ı bounded model checkingu v JPF. Implementaci metody Record&Replay trace, lze rozdˇelit na dvˇe hlavn´ı ˇc´asti, na implementaci mechanizmu pro z´ aznam cesty a na strategii pro pˇrehr´an´ı zaznamenan´e cesty. Pro implementaci mechanizmu pro z´ aznam cesty bylo hlavn´ım bodem urˇcen´ı jak´e informace je tˇreba zaznamen´ av´ at, aby bylo moˇzn´e zaznamenanou cestu pozdˇeji pˇrehr´at. Potom byly postupnˇe navrˇzeny a implementov´any listenery model checkeru, kter´e slouˇz´ı pro z´aznam cesty, kter´ a obsahuje informace podle pouˇzit´eho listeneru. Po naimplementov´an´ı mechanizmu pro z´ aznam cesty bylo moˇzn´e pˇristoupit k implementaci strategie pro pˇrehr´an´ı cesty. Pˇrehr´an´ı cesty bylo u ´spˇeˇsn´e u cesty zaznamenan´e pomoc´ı listener˚ u Java PathFinderu. Zat´ım nen´ı hotov´e pˇrehr´ av´ an´ı cesty, kter´a byla zaznamen´ana pomoc´ı n´astroje ConTest. Ten v pro-
45
jektu SHADOWS slouˇz´ı pro opravu chyby. Tato ˇc´ast implementace pro vytvoˇren´ı strategie pˇrehr´avaj´ıc´ı cestu zaznamenanou pomoc´ı ConTestu je v rozpracovan´e f´azi. Dalˇs´ı pr´ ace bude vˇenov´ ana dokonˇcen´ı t´eto strategie. Po dokonˇcen´ı implementace strategie pro pˇrehr´ an´ı cesty bude moˇzn´e celou metodu otestovat na re´aln´ ych datech. A prov´est bounded model checking pro ovˇeˇren´ı opravy. Pro vlastn´ı verifikaci byl zvolen model checker Java PathFinder, kter´ y umoˇznuje r˚ uzn´e rozˇs´ıˇren´ı. Umoˇznuje tedy nejen verifikaci vlastnost´ı pro kter´e Java PathFinder jiˇz obsahuje moduly, ale tak´e doimplementov´an´ı dalˇs´ıch modul˚ u pro verifikaci konkr´etn´ıch speci´aln´ıch vlastnost´ı syst´emu. Implementace tˇechto modul˚ u do Java PathFinderu jiˇz nen´ı obt´ıˇzn´a. Napˇr´ıklad modul pro detekci TrueRace“ je jiˇz ” implementov´ an.
46
Literatura [1] B. Kˇrena and Z. Letko and R. Tzoref and S. Ur and T. Vojnar. Healing data races on-the-fly. In PADTAD ’07, pages 54–64. ACM, 2007. [2] W. Beaton and J. d. Rivieres. Eclipse platform technical overview. Technical report, The Eclipse Foundation, 2006. [3] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking, 2003. [4] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. [5] O. Edelstein, E. Farchi, E. Goldin, Y. Nir, G. Ratsaby, and S. Ur. Framework for testing multi-threaded java programs. 15(3–5):485–499, March/April 2003. [6] Orit Edelstein, Eitan Farchi, Evgeny Goldin, Yarden Nir, Gil Ratsaby, and Shmuel Ur. Framework for testing multi-threaded java programs. Concurrency and Computation: Practice and Experience, 15(3-5):485–499, 2003. [7] E.M. Clarke, O. Grumberg, M. Minea, D. Peled. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer 2, 3:279–287, 1999. [8] M. Dwyer et al. Bandera. http://bandera.projects.cis.ksu.edu. [9] P. Mehlitz et al. Java pathfinder. http://javapathfinder.sourceforge.net. [10] Robby et al. Bogor software model checking framework. http://bogor.projects.cis.ksu.edu. [11] Z. Letko et al. Java race detector & healer. http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/document.html. [12] B. Kˇrena et.al. Deliverable D3.2.3: Report on Safety of Program Modifications. Technical Report FP6 IST-035157 SHADOWS: Deliverable D3.2.3, Brno University of Technology and IBM Haifa Research Lab, Aug 2007. [13] G. Lindstrom,P.C. Mehlitz, and W. Visser. Model checking real time java using java pathfinder. pages 444–456. 2005. [14] G. Xu, A. Rountev, Y. Tang, and F. Qin. Efficient checkpointing of java software using context-sensitive capture and replay. In ESEC-FSE ’07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pages 85–94, New York, NY, USA, 2007. ACM Press. 47
[15] G.J. Holzmann, and D. Peled. An improvement in formal verification. In Proc. Formal Description Techniques, FORTE94, pages 197–211, Berne, Switzerland, October 1994. Chapman & Hall. [16] IBM Haifa Labs Home. Contest - a tool for testing multi-threaded java applications. http://www.haifa.il.ibm.com/projects/verification/contest/index.html. [17] K. Havelund, and T. Pressburger. Model checking java programs using JAVA pathfinder. International Journal on Software Tools for Technology Transfer, 2(4):366–381, 2000. [18] Tim Lindholm and Frank Yellin. The Java(TM) Virtual Machine Specification (2nd Edition). Prentice Hall PTR, April 1999. [19] M.Mansouri-Samani et al. Program Model Checking, A Practitioner’s Guide. Intelligent System Division NASA Ames Research Center, April 2007. [20] V. Hrub´ a, and B. Kˇrena and Z. Letko and T. Vojnar. Shadows - deliverable d3.2.3: Report on safety of program modifications. Technical report, 2007. [21] A. Valmari. The state explosion problem. In Lectures on Petri Nets I, 1998. [22] P. Mehlitz W. Visser. Model checking java programs using java pathfinder. http://www.visserhome.com/willem/presentations/ase06jpftut.ppt . [23] X. Zhang, H. He, N. Gupta, and R. Gupta. Experimental evaluation of using dynamic slices for fault location. In AADEBUG’05: Proceedings of the sixth international symposium on Automated analysis-driven debugging, pages 33–42, New York, NY, USA, 2005. ACM.
48