BOUNDED MODEL CHECKING V NÁSTROJI JAVA PATHFINDER

ˇ ´ UCEN Í TECHNICKE ´ V BRNE ˇ VYSOKE BRNO UNIVERSITY OF TECHNOLOGY

ˇ ÍCH TECHNOLOGIÍ FAKULTA INFORMACN ´ ´ U ˚ USTAV INTELIGENTNÍCH 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 Í TECHNICKE ´ V BRNEˇ VYSOKE BRNO UNIVERSITY OF TECHNOLOGY

ˇ ÍCH TECHNOLOGIÍ FAKULTA INFORMACN ´ ´ U ˚ USTAV INTELIGENTNÍCH 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Í PRACE SUPERVISOR

BRNO 2008

ˇ Ing. BOHUSLAV KRENA, Ph.D.

Abstrakt Diplomov´ a pr´ ace je vˇenovan´ a aplikaci formáln´ı metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se soubˇeˇznost´ı. Práce je zamˇeˇrena na programy napsané 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á v aplikaci strategie pro navigaci stavov´ ym prostorem do m´ısta verifikace. Z daného 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áln´ıch vlastnost´ı systému, které ovˇeˇruj´ı koreknost opravy chyby. Bounded model checking se provád´ı 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án´ı 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ástroji Java PathFinder, diplomová práce, 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áci 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é své rodinˇe, prátel˚ um a spoluˇzák˚ um za jejich podporu a pomoc pˇri studiu. Tato pr´ ace byla podpoˇrena Evropskou uni´ı v rámci FP6-IST projektu SHADOWS (ˇc. smlouvy IST-035157). Za obsah pr´ ace odpov´ıdá pouze jej´ı autor. Tato práce nevyjadˇruje názor Evropské unie a Evropsk´ a unie nen´ı odpovˇedná za uˇzit´ı jakékoliv informace v práci uvedené.

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ém uˇcen´ı technickém v Brnˇe, Fakultˇe informaˇcn´ıch technologi´ı. Pr´ ace je chr´ anˇena autorským z´ akonem a jej´ı uˇzit´ı bez udˇelen´ı opr´ avnˇen´ı autorem je nez´ akonné, s výjimkou z´ akonem definovaných pˇr´ıpad˚ u.

Obsah ´ 1 Uvod

3

2 Rozbor problematiky 2.1 Proces automatické opravy . . . 2.1.1 Princip opravy problému 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ému . . . . . . . . 3.2 Specifikace systému . . . . . . 3.3 V´ ystup verifikace . . . . . . . 3.4 Problém stavové 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ého 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átor˚ 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ódu . . . . . . . 5.3.2 Replay trace pomoc´ı instrumentovaného kódu . . 5.4 V´ ysledky a Testy . . . . . . . . . . . . . . . . . . . . . . 5.4.1 Rychlost bˇehu programu ve pouˇzit´ ych nástroj´ı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émˇeˇr na kaˇzdém kroku. At’ uˇz se jedn´ a o mobiln´ı telefony, bankovn´ı u ´ˇcty, pr˚ umyslové stroje nebo ˇr´ıd´ıc´ı stˇrediska. Vˇzdy chceme, aby n´ am naˇse pˇr´ıstroje pracovaly správnˇe, coˇz ale jiˇz z principu nelze. O ˇz´ adném rozs´ ahlejˇs´ım programu nem˚ uˇzeme prohlásit, ˇze neobsahuje chyby, lze pouze ˇr´ıci, jaké chyby neobsahuje. Jsou pˇr´ıpady, kdy nám nevad´ı, ˇze program zatuhne“ nebo ” provede neplatnou akci, napˇr. pˇri pos´ılán´ı emailu se nepodaˇr´ı komunikace se serverem, email se neodeˇsle a jeho obsah je ztracen. V takovém pˇr´ıpadˇe nás chyba zamrz´ı, mus´ıme email napsat znova. M˚ uˇze ovˇsem nastat situace, kdy se jedná o d˚ uleˇzité události, které mohou zp˚ usobit z´ avaˇznˇejˇs´ı problémy – nepˇriˇcten´ı správné ˇcástky na bankovn´ı u ´ˇcet, porucha na lékaˇrsk´ ych pˇr´ıstroj´ıch, atd. V takovém pˇr´ıpadˇe rozhodnˇe nechceme, aby program zatuhl nebo vykonal neoˇcek´ avanou akci. Z toho d˚ uvodu se vynakládá spousta penˇez na testov´ an´ı a ovˇeˇrov´ an´ı korektnosti program˚ u, aby programy vykonávaly pouze poˇzadované události. I pˇres veˇskeré snahy v programech z˚ ustávaj´ı chyby, které se dostanou aˇz k uˇzivateli. Dává tedy smysl se zab´ yvat opravou tˇechto chyb, které se neodhal´ı pˇri testován´ı a snaˇzit se je opravit za bˇehu aplikace. Právˇe o to se snaˇz´ı projekt SHADOWS, jehoˇz souˇcást´ı 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á procesem automatické opravy (selfhealing approach). Princip procesu a jeho c´ıl se daj´ı specifikovat pomoc´ı následuj´ıc´ıch ˇctyˇr základn´ıch krok˚ u: 1. zjiˇ stˇ en´ı probl´ emu (problem detection) – pˇredt´ım neˇz se zaˇcne s opravou (léˇcen´ım) je potˇreba urˇcit, zda je v systému nˇejak´ y problém a ˇceho se t´ yká, 2. nalezen´ı pˇ r´ıˇ ciny probl´ emu (problem localization) – druh´ ym krokem po urˇcen´ı moˇzného problému v systému je tˇreba tento problém lokalizovat resp. urˇcit m´ısto v programu (sledovaném systému), kde se problém vyskytuje, 3. oprava probl´ emu (problem healing) – dalˇs´ım krokem je v´ ybˇer akce, ze seznamu nab´ızen´ ych léˇc´ıc´ıch akc´ı, které je moˇzné pro opravu detekovaného problému pouˇz´ıt, 4. ovˇ eˇ ren´ı opravy (problem assurance) – posledn´ım krokem je ovˇeˇren´ı, zda provedn´ı opravné akce nezp˚ usobilo v systému jin´ y problém. Léˇc´ıc´ı akce zmˇen´ı chov´ an´ı systému, pˇredpokl´ ad´ ame, ˇze se nyn´ı systém bude chovat korektnˇe vzhledem k urˇcen´ ym poˇzadavk˚ um. Nicménˇe opravná akce m˚ uˇze zmˇenit chován´ı systému takov´ ym zp˚ usobem, ˇze se objev´ı jin´ y problém. Z toho d˚ uvodu je potˇreba provést 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ého provádˇen´ı v programu. Fakulta informaˇcn´ıch technologi´ı se v projektu vˇenuje ˇc´ asti zamˇeˇrené na soubˇeˇzné provádˇen´ı (concurrency). Pˇresnˇeji se vˇenuje léˇcen´ı chyb, které vznikaj´ı pomoc´ı paralelismu resp. soubˇeˇznosti v systému. Jedná se o chyby typu deadlocks, data races, lost notification, atd. Léˇcen´ı se zamˇeˇruje na opravy chyb v Java programech, ve kter´ ych se soubˇeˇznost implementuje velice snadno pomoc´ı vláken. Tato diplomov´ a pr´ ace je vˇenovaná posledn´ımu z uveden´ ych krok˚ u opravného procesu – ovˇeˇren´ı léˇc´ıc´ı akce. K tomu, aby bylo moˇzné navrhnout vhodnou metodu pro ovˇeˇren´ı léˇc´ıc´ı akce, je zapotˇreb´ı zn´ at, co léˇc´ıc´ı akce provád´ı a jak´ ym zp˚ usobem funguje. Pokud známe princip opravné akce, je moˇzné navrhnout a posléze implementovat metody pro ovˇeˇren´ı korektnosti opravy. Dalˇs´ı text je dˇelen do n´ asleduj´ıc´ıch kapitol. V druhé kapitole jsou podrobnˇeji rozepsány jednotlivé kroky opravného procesu pro lepˇs´ı porozumˇen´ı celého procesu opravy. Dále 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ákladech a principu pojednává tˇret´ı kapitola. Zde jsou také pops´ any jeho modifikace, problém stavové exploze a jeho moˇzná ˇreˇsen´ı. Ve ˇctvrté kapitole jsou nejprve uvedeny r˚ uzné model checkery, ze kter´ ych byl pro verifikaci zvolen model checker – Java PathFinder. Jeho popis a nastaven´ı jeho vlastnost´ı jsou v této kapitole také uvedeny. Dalˇs´ı kapitola popisuje hloubˇeji zvolenou metodu pro verifikaci systému z hlediska implementace v Java PathFinderu. Jsou zde uvedeny pˇr´ıklady a dosaˇzené v´ ysledky. Posledn´ı kapitolou je z´ avˇer, kter´ y obsahuje shrnut´ı v´ ysledk˚ u a nástin dalˇs´ı práce na projektu.

4

Kapitola 2

Rozbor problematiky 2.1

Proces automatick´ e opravy

V následuj´ıc´ıch odstavc´ıch budou podrobnˇeji rozepsány jednotlivé kroky procesu automatické opravy. Kroky procesu popisuj´ı princip léˇcen´ı chyb, které vznikaj´ı soubˇeˇznost´ı v Java programech [12]. Zjiˇ stˇ en´ı probl´ emu. V prvn´ım kroku se monitoruje vykonáván´ı programu. Monitorován´ı 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á pravdˇepodobnost, ˇze chyba nebude nalezena. Program na u ´rovni byte-codu umoˇzn ˇuje velké mnoˇzstv´ı moˇznost´ı proklád´ an´ı instrukc´ı a t´ım se sniˇzuje pravdˇepodobnost nalezen´ı chyby bˇehem testován´ı. Pomoc´ı instrumentace se do programu zav´ ad´ı také ˇsum (dalˇs´ı instrukce), pomoc´ı kter´ ych se zvyˇsuje pravdˇepodobnost odhalen´ı chyb vznikl´ ych nesprávn´ ym prokládán´ım instrukc´ı (data race). Instrumentace k´ odu se prov´ ad´ı pomoc´ı nástroje ConTest, kter´ y pracuje nad Java bytecodem a jehoˇz bliˇzˇs´ı popis a specifikace jsou uvedeny v [5]. ConTest je nástroj vyv´ıjen´ y v´ yzkumnou laboratoˇr´ı IBM pro testován´ı Java program˚ u, které obsahuj´ı v´ıce vláken [6]. Nalezen´ı pˇ r´ıˇ ciny probl´ emu. Nalezen´ı pˇr´ıˇciny problému 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é akce ze speciáln´ıho seznamu, kter´ y byl navrˇzen pro v´ ybˇer spr´ avné opravy chyb vznikl´ ych soubˇeˇznost´ı. Jedná se o následuj´ıc´ı detektory: dataRace detektor, atomRace detektor nebo deadlock detektor. Jinou moˇznost´ı je provádˇen´ı velkého mnoˇzstv´ı test˚ u s r˚ uzn´ ymi body instrumentace a následné statistické vyhodnocen´ı dosaˇzen´ ych v´ ysledk˚ u. Pomoc´ı z´ıskan´ ych statistick´ ych dat a korektnosti chován´ı programu v daném testu se d´ a urˇcit problém. Oba v´ yˇse popsané pˇr´ıstupy lze kombinovat s formáln´ı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án problém, kter´ y ve skuteˇcnosti v programu nen´ı. Z principu funkce formáln´ıch metod, by se tyto metody daly aplikovat na samotnou lokalizaci problému v systému. Nicménˇe jejich aplikace na reáln´ y systém je problematick´ a z d˚ uvodu stavové exploze. Ta je kritick´ ym problémem formáln´ıch metod, kter´ y br´ an´ı jejich nasazen´ı na reálné systémy a proveden´ı jejich celkové verifikaci. Oprava probl´ emu. N´ astroj (tool) pro opravu problému m˚ uˇze b´ yt zaloˇzen na v´ ybˇeru opravné akce, které jsou vyjmenovány ve speciáln´ım seznamu. Zvolená oprava detekovaného problému m˚ uˇze b´ yt nab´ıdnuta v´ yvojáˇri jako moˇzné ˇreˇsen´ı bˇehem v´ yvoje systému. V´ yvoj´ aˇr se pak s´ am rozhodne, zda nab´ızenou akci provede ˇci nikoliv. C´ılem projektu je ovˇsem 5

léˇcit chyby, které se projev´ı u uˇzivatele. Zámˇerem je tedy léˇcit chyby, které se jiˇz jednou v systému vyskytly a na nˇe aplikovat opravu, a t´ım zamezit jejich opˇetovnému v´ yskytu v aplikaci u uˇzivatele. Prozat´ım se léˇc´ıc´ı akce zamˇeˇruj´ı na problémy typu data races. Data races vznikaj´ı v d˚ usledku paraleln´ıho pˇr´ıstupu ke sd´ılené promˇenné ve stejn´ y ˇcasov´ y okamˇzik z v´ıce m´ıst, jehoˇz d˚ usledkem je konfliktn´ı zápis do sd´ılené promˇenné. Moˇzn´ ym ˇreˇsen´ım odstranˇen´ı problému data race je pˇridán´ı zámk˚ u (locks). Pˇresnˇejˇs´ı popis jednotliv´ ych oprav i samotného problému data race je bl´ıˇze uveden v [1, 12]. Ovˇ eˇ ren´ı opravy. Posledn´ım krokem procesu je ovˇeˇren´ı opravné akce. Bylo by chybné pˇredpokl´ adat, ˇze lze navrhnout univerzáln´ı opravu urˇcitého problému, která by fungovala za vˇsech okolnost´ı. Z toho d˚ uvodu jsou navrˇzeny speciáln´ı léˇc´ıc´ı akce pro konkrétn´ı pˇr´ıpady v´ yskytu urˇcitého problému. Proto je také potˇreba ovˇeˇrit, zda zvolená oprava chyby byla u ´spˇeˇsn´ a a bezpeˇcn´ a (napˇr. ovˇeˇren´ı zda pˇridán´ı zámk˚ u pro odstranˇen´ı problému data race, nezp˚ usobilo jin´ y problém – deadlock, apod.). Ke kontrole opravy je vhodné pouˇz´ıt formáln´ı verifikaci, jedn´ a se efektivn´ı metody pro ovˇeˇrován´ı správnosti systému. Mezi formáln´ı metody patˇr´ı model checking, statická anal´ yza nebo theorem proving. V pˇr´ıpadˇe jejich omezen´ı resp. modifikace je lze aplikovat na reáln´ y systém a zverifikovat ho. Jak jiˇz bylo uvedeno v u ´vodu, k tomu aby bylo moˇzné navrhnout správnou metodu pro ovˇeˇren´ı opravy, je potˇreba zn´ at jej´ı podstatu a zp˚ usob aplikace na problém resp. chybu.

2.1.1

Princip opravy probl´ emu

Pˇredpokl´ adejme, ˇze v monitorovaném systému byl lokalizován problém. Ten se nach´ az´ı ve speci´ aln´ım seznamu problém˚ u, pro které jsou navrˇzeny léˇc´ıc´ı akce. Posléze se zvolen´ a léˇc´ıc´ı akce aplikuje na detekovan´ y problém, a ta problém v programu oprav´ı [1]. Existuj´ı dvˇe moˇznosti jak opravu na problém aplikovat. Prvn´ı moˇznost´ı je pouze navrˇzen´ı opravy v´ yvojáˇ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án´ı systému za jeho bˇehu bez nutnosti explicitn´ıho zásahu do zdrojového kódu. Architektura listener˚ u je souˇc´ ast´ı jiˇz zmiˇ novaného n´ astroje ConTest [5, 16]. Oprava pomoc´ı pl´ anov´ an´ı. D´ıky monitorován´ı (sledován´ı) systému za jeho bˇehu vzniká v bˇehu programu ˇsum, resp. v programu se vykonává v´ıce instrukc´ı neˇz v bˇeˇzném bˇehu programu bez monitorov´ an´ı. Pomoc´ı tohoto mechanizmu je snadnˇejˇs´ı odhalit chyby vzniklé soubˇeˇznost´ı, které se projevuj´ı pouze pˇri urˇcitém prokládán´ı instrukc´ı. K nesprávnému prokl´ ad´ an´ı instrukc´ı vedouc´ı k chybˇe docház´ı napˇr´ıklad pˇri vyt´ıˇzen´ı procesoru jin´ ymi programy, které nejsou bˇeˇznˇe pˇri testován´ı programu spuˇstˇeny. Proto monitorován´ı, které také 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án´ı metody yield(). Metoda se zavolá pˇred kritickou seck´ı, kde docház´ı k chybˇe. Princip metody yield() spoˇc´ıvá v pˇrepnut´ı kontextu na jiné vl´ akno (aktu´ aln´ı vlákno se vzdává procesoru), pˇri dalˇs´ım pˇridˇelen´ı procesoru je jiˇz dostatek ˇcasu na vykonán´ı kritické sekce vcelku (bez pˇrepnut´ı kontextu). Uvedenou techniku lze kombinovat s pˇridˇelován´ım r˚ uzn´ ych priorit vlákn˚ um. V takovém pˇr´ıpadˇe do kritické sekce m˚ uˇze vstoupit nebo ji pˇreruˇsit pouze vlákno se stejnou nebo vyˇsˇs´ı prioritou. Oprava pomoc´ı synchronizace. Zmiˇ novaná ˇcást projektu SHADOWS je zamˇeˇrena na chyby, které jsou zp˚ usobeny nevhodn´ ym pouˇzit´ım synchronizace, nebo kdyˇz synchronizace zcela chyb´ı. V pˇr´ıpadˇe chybného pouˇzit´ı synchronizace obsahuje oprava vhodnou zmˇenu v synchronizaci. Pokud se jedn´ a o problém chybˇej´ıc´ı synchronizaci nad sd´ılenou promˇennou, je tˇreba vˇenovat dostateˇcnou pozornost pˇridán´ı zámku. Zámek je potˇreba vloˇzit takov´ ym

6

zp˚ usobem, aby jeho pˇrid´ an´ı nezp˚ usobilo jin´ y problém v systému, typick´ ym problémem je vznik deadlocku. Je tedy nutno ovˇeˇrit, zda pˇridán´ı zámk˚ u skuteˇcnˇe vyˇreˇsilo problém (data race) a d´ ale zverifikovat, ˇze zm´ınˇená oprava nezp˚ usobila v systému jin´ y problém.

2.1.2

Princip ovˇ eˇ ren´ı opravy

Pro ovˇeˇren´ı opravy je moˇzné pouˇz´ıt techniky formáln´ı verifikace jako model checking, statickou anal´ yzu atd. K tomu, aby bylo moˇzné formáln´ı metody aplikovat na reáln´ y systém, je tˇreba udˇelat jejich omezen´ı nebo urˇcitou modifikaci. V tomto pˇr´ıpadˇe – ovˇeˇrován´ı opravy, nen´ı c´ılem zverifikovat cel´ y systém, ale pouze okol´ı léˇcené chyby. Jde tedy o aplikaci formáln´ı metody na konkrétn´ı ˇc´ ast programu a na kompletn´ı reáln´ y systém. Aplikace formáln´ı metody m˚ uˇze vypadat n´ asledovnˇe. Pouˇzit´ı statické anal´ yzy nad byte-codem: v pˇr´ıpadˇe pouˇzit´ı opravné akce – pˇridán´ı zámk˚ u (lock/unlock) je tˇreba ovˇeˇrit, zda nové zámky nejsou v kolizi s jiˇz naimplementovanou synchronizac´ı. Pˇr´ıpadn´ a kolize synchronizace by mohla zp˚ usobit deadlock. Problém data races se ˇcasto vyskytuje nad jednoduch´ ymi pˇr´ıkazy (malá ˇcást kódu). Provést statickou anal´ yzu nad malou ˇc´ ast´ı k´ odu nen´ı problém a tud´ıˇz odhalen´ı daného problému je moˇzné. Pro pouˇzit´ı model checkingu se je nejprve potˇreba dostat do poˇzadovaného stavu resp. do jeho okol´ı a zde posléze provést bounded model checking. Bounded model checking se provede do pˇredem urˇcené hloubky stavového prostoru. K prohledáván´ı stavového prostoru existuj´ı r˚ uzné heurisitiky, d´ ale je potˇreba pro prohledáván´ı stavového prostoru zadat r˚ uzné specifikace, které maj´ı b´ yt v systému splnˇeny (verifikovány). Pokud opravn´ a akce zp˚ usob´ı jin´ y problém a pomoc´ı ovˇeˇrován´ı opravy se dan´ y problém zjist´ı, je potˇreba upravit léˇc´ıc´ı akci tak, aby k nové chybˇe nedocházelo nebo zvolit jinou léˇc´ıc´ı akci. Po zmˇenˇe opravy je tˇreba provést nové ovˇeˇren´ı bˇehu programu, zda se jiˇz systém chov´ a korektnˇe. St´ ale zde ale pˇretrv´ av´ a problém moˇzného v´ yskytu chyb. Verifikace systému nebo ˇcásti systému se prov´ ad´ı vˇzdy vzhledem k nˇejak´ ym konkrétn´ım vlastnostem a specifikac´ım. Stále tedy neˇreˇs´ı problém, kdy o ˇzádném systému nelze ˇr´ıci, ˇze je bezchybn´ y. O programu lze pouze ˇr´ıci, které chyby neobsahuje. Pokud je znám princip opravy, je moˇzné navrhnout a posléze implementovat takovou metodu pro ovˇeˇren´ı korektnosti opravy, která ovˇeˇr´ı ty specifikace, u kter´ ych bˇehem léˇcen´ı doˇslo ke zmˇenˇe.

2.2

Form´ aln´ı metody

Formáln´ı metody jsou zaloˇzeny na matematick´ ych metodách, um´ı dokázat/vyvrátit urˇcité specifikace systému. Form´ aln´ımi metodami rozum´ıme verifikaˇcn´ı nebo analytické metody. Verifikace ovˇeˇruje zadané vlastnosti v systému. Napˇr´ıklad v paraleln´ıch programech m˚ uˇze verifikace odpovˇedˇet na otázku, zda se v programu vyskytuje deadlock. Verifikace tedy vrac´ı odpovˇed’ ano/ne podle toho, jestli je verifikovaná vlastnost v systému splnˇena nebo ne. Existuj´ı ale také specifikace, které ovˇeˇrit nelze. Analýza poskytuje odpovˇedi na obecnˇejˇs´ı otázky o systému, neodpov´ıdá tedy ano/ne, zda je vlastnost v systému splnˇena, ale podává komplexnˇejˇs´ı informace o chován´ı systému jako optimalizace, syntéza, apod. Rozd´ıl mezi form´ aln´ımi metodami a testován´ım spoˇc´ıvá v odpovˇedi na otázku, zda systém obsahuje danou chybu. Pokud se bˇehem testován´ı objev´ı chyba, je zˇrejmé, ˇze program danou chybu obsahuje, ale pokud se bˇehem testován´ı chyba neprojev´ı, neznamen´ a to, ˇze v programu zadan´ a chyba nen´ı. Narozd´ıl od formáln´ı verifikace, jestliˇze se bˇehem

7

verifikace chyba neprojev´ı a byla provedena verifikace celého systému, uvedená chyba se v systému opravdu nevyskytuje. Ide´ aln´ı form´ aln´ı verifikace splˇ nuje následuj´ıc´ı vlastnosti. Ideáln´ı formáln´ı verifikace je plnˇe automatick´ a, spolehliv´ a (pokud dojde k závˇeru, mus´ı b´ yt správn´ y), u ´plná (pokud najde chybu, jedn´ a se o skuteˇcnou chybu – nejede o false alarm), koneˇcná (verifikace vˇzdy skonˇc´ı s urˇcit´ ym z´ avˇerem). Bohuˇzel v praxi ideáln´ı verifikace neexistuje, kritick´ ym problémem verifikace je stavov´ a exploze. V pˇripadˇe systému s koneˇcn´ ym stavov´ ym prostorem a moˇznost´ı vyuˇz´ıt´ı dostateˇcnˇe v´ ykonného poˇc´ıtaˇce – verifikace vˇzdy dojde k závˇeru. V praxi se ale ˇcasto setkáv´ 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álné verifikace maj´ı tedy n´ asleduj´ıc´ı vlastnosti: produkuj´ı false alarmy, nekonˇc´ı vˇzdy korektnˇe, nejsou plnˇe automatické a nejsou stoprocetnˇe spolehlivé. K tomu, aby bylo moˇzné provádˇet verifikace, je nejprve zapotˇreb´ı nadefinovat systém, kter´ y bude verifikov´ an a jeho vlastnosti, které se maj´ı zkontrolovat. Vstupn´ı systém m˚ uˇze b´ yt pops´ an pomoc´ı modelu (petri net, promela, SMV, atd.) nebo jako reáln´ y systém (programy v r˚ uzn´ ych programovac´ıch jazyc´ıch, Verilog, hardware pospan´ y ve VHDL, atd.). Vlastnosti, které se maj´ı verifikovat, mohou b´ yt napˇr. ˇzivost promˇenn´ ych, invarianty, ukonˇcen´ı systému pouze v poˇzadovaném m´ıstˇe. Vlastnosti, které se verifikuj´ı, lze rozdˇelit do dvou skupin: bezpeˇcnost a ˇzivost. Bezpeˇcnost nám ˇr´ıká, ˇze v systému nikdy nenastane nic ˇspatného, protipˇr´ıklad takové vlastnosti je koneˇcn´ y – nˇekdy nastane nˇeco ˇspatného. Oproti tomu ˇzivost systému ˇr´ık´ a, ˇze v systému nˇekdy nastane nˇeco dobrého a protipˇr´ıklad je nekoneˇcn´ y– nikdy nenastane nic ˇspatného. Lze tedy uvést, ˇze bezpeˇcnost se verifikuje snadnˇeni neˇz ˇzivost. Pro popis vlastnost´ı je moˇzné pouˇz´ıt napˇr´ıklad formule temporáln´ıch logik,µ-calcul, labels, atd. Dalˇs´ı d˚ uleˇzitou charakteristikou vlastnost´ı pro verifikaci je ˇcas, kter´ y má dvˇe základn´ı rozdˇelen´ı na ˇcas logick´ y/fyzick´ y a lineárn´ı/vˇetv´ıc´ı se. Logický ˇcas ukazuje ˇcasov´ y sled jednotliv´ ych ud´ alost´ı podle bˇehu, kdeˇzto fyzický ˇcas slouˇz´ı k urˇcen´ı kolik ˇcasu na jakou událost bylo potˇreba vzhledem ke zvolenému 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áhled na dva bˇehy, které se rozcházej´ı aˇz posléze. Nejpouˇz´ıvanˇejˇs´ımi metodami pro formáln´ı anal´ yzu a verifikaci jsou model checking, statick´ a analýza a theorem proving. Model checking. Model checking je algoritmická technika, která ovˇeˇruje, zda systém y systém m˚ uˇze b´ yt popsán jak modelem, tak splˇ nuje poˇzadované vlastnosti [4]. Verifikovan´ reáln´ ym systémem. Model checking umoˇzn ˇuje verifikovat systémy s koneˇcn´ ym stavov´ ym prostorem. Kritick´ ym problémem model checkingu je exploze stavového prostoru, kde velikost stavového prostoru roste exponenciálnˇe s velikost´ı verifikovaného systému [21]. Vlastnosti jsou typicky specifikov´ any pomoc´ı temporáln´ıch logik. V´ yhodami model checkingu jsou: vysok´ y stupeˇ n automatizace, snadné pouˇzit´ı (pokud to umoˇzn ˇuje systém), pomˇernˇe vˇseobecné pouˇzit´ı pro verifikaci r˚ uzn´ ych vlastnost´ı systému. Oproti tomu hlavn´ı nev´ yhodou je jiˇz zmiˇ novaná exploze stavového prostoru, kter´ y se d´ a ˇreˇsit r˚ uzn´ ymi metodami jako redukce, abstrakce, kompozice systému z ˇcást´ı, atd. Dalˇs´ı nev´ yhodou je nutnost modelovat okol´ı verifikovaného systému jako jsou vstupy. Statick´ a anal´ yza. Statick´ a anal´ yza se neprovád´ı nad skuteˇcn´ ym bˇehem systému, ale pouze nad zdrojov´ ym k´ odem. T´ım umoˇzn ˇuje zjistit informace o programu ze zdrojového kódu, aniˇz by bylo nutné program spouˇstˇet. Statické anal´ yzy jsou r˚ uzné druhy (typov´ a 8

anal´ yza, vyhled´ av´ an´ı chybov´ ych vzor˚ u – bug pattern, dataflow anal´ yza, apod.). V´ yhodami statické anal´ yzy je moˇznost verifikovat obrovské systémy, zároveˇ n nen´ı nutné modelovat okol´ı systému a nab´ız´ı velk´ y stupeˇ n automatizace. Nev´ yhodou je velká specializace jednotliv´ ych statick´ ych anal´ yz na konkrétn´ı problémy. Pokud je c´ılem zverifikovat novˇe zadan´ y problém, mus´ı se nejprve navrhnout nová statická anal´ yza pro jeho ovˇeˇren´ı. Dalˇs´ı nev´ yhodou je vznik false alarm˚ u. D´ıky tomu, ˇze se statická anal´ yza provád´ı nad zdrojov´ ym kódem, m˚ uˇze nadetekovat chybu, kter´ a pˇri skuteˇcném bˇehu nikdy nenastane (false positive). Theorem proving. Jedn´ a se o deduktivn´ı verifikaci, která vycház´ı z axiom˚ u a pomoc´ı pouˇzit´ı r˚ uzn´ ych pravidel produkuje vlastnosti systému. Uˇzit´ı jednotliv´ ych pravidel nen´ı automatické, je potˇreba z´ asahu uˇzivatele experta“, kter´ y vede d˚ ukaz. Jedná se tedy ” o ˇcásteˇcnˇe automatickou metodu, která je velmi obecná, coˇz je jej´ı v´ yhodou. Nev´ yhodou je problém s diagnostickou informac´ı, která m˚ uˇze, ale také nemus´ı b´ yt k dispozici. Pro ovˇeˇren´ı opravy byla zvolena fromáln´ı metoda – model checking. Ta umoˇzn ˇuje verifikovat systém dynamicky, a tedy hledat pouze chyby, které mohou v systému reálnˇe nastat oproti statické 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ém splˇ nuje poˇzadovanou akladn´ı schéma verifikaˇcn´ıho procesu je znázornˇené na obr. 3.1. Vstupem vlastnost [4]. Z´ pro verifikace je verifikovan´ y systém, kter´ y je typicky popsán pomoc´ı formáln´ıho modelu systému. Druh´ ym vstupem je formáln´ı specifikace vlastnost´ı, které se maj´ı ovˇeˇrit. Model systému a specifikované vlastnosti vstupuj´ı do model checkeru, kter´ y ovˇeˇruje resp. verifikuje zadané vlastnosti. V ide´ aln´ım pˇr´ıpadˇe nám model checker vrát´ı odpovˇed’ ano/ne, podle toho jestli je vlastnost splnˇena. V praxi ovˇsem m˚ uˇze nastat i situace, kdy nám model checker ’ nen´ı schopen poskytnout odpovˇed , napˇr. z d˚ uvodu nedostatku pamˇeti.

Obr´ azek 3.1: Z´ akladn´ı schéma procesu verifikace pomoc´ı model checkeru

Principem model checkingu je systematické prohledáván´ı stavového prostoru. Stav (state) je sn´ımek systému v ˇcase, zachycuje hodnoty promˇenn´ ych v daném ˇcasovém okamˇziku. Zároveˇ n chceme zn´ at, jak se stavy mˇen´ı – popis zmˇeny mezi jednotliv´ ymi stavy (stav pˇred událost´ı a stav po ud´ alosti) se naz´ yvá pˇrechod (transition). Výpoˇcet (computation) je sekvence stav˚ u, kde se n´ asleduj´ıc´ı stav z´ıská z pˇredchoz´ıho stavu pomoc´ı pˇrechodu.

10

3.1

Model syst´ emu

Reálné systémy jsou vˇetˇsinou zadány pomoc´ı textu programu (zdrojov´ y kód) nebo diagramem cest. Je tedy potˇreba mechanizmus, kter´ y je schopen popsat vˇsechny typy systém˚ u tak, aby mohli b´ yt verifikov´ any. Jednou moˇznost´ı popisu chován´ı systému je Kripkeho struky popisuje stavy systému a jeho tura (Kripke structure) obr. 3.2(a) . Jedná 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á, ˇze ∀s ∈ S : ∃s0 ∈ S : R(s, s0 ) • L : S → 2AP je funkce pˇriˇrazuj´ıc´ı kaˇzdému stavu mnoˇzinu vˇsech atomick´ ych tvrzen´ı, kter´ a v daném stavu plat´ı, AP = {v = d | v ∈ V ∧ d ∈ D}, kde V je mnoˇzina promˇenn´ ych nad doménou D. Pro popis sekvenˇcn´ıho chov´ an´ı Kripkeho struktury M jsou definovány cesty (paths). Cesta (path) v Kripkeho struktuˇre M ze stavu s je nekoneˇcná sekvence stav˚ u π = s0 s1 s2 ..., která je ˇrazen´ a s ohledem na pˇrechodovou relaci v M . Pˇrechodová relace R(si , si+1 ) plat´ı pro vˇsechny 0 ≤ i < |π| − 1. Jestliˇze I(s0 ) t.j. s0 je poˇcáteˇcn´ı stav, potom se cesta naz´ yv´ a poˇcáteˇcn´ı (initialized). Délka cesty (length) |π| m˚ uˇze b´ yt jak koneˇcná, 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é poˇcáteˇcn´ı cesty systému, lze z Kripkeho struktury ypoˇcetn´ı strom tedy zapsat pomoc´ı výpoˇcetn´ıho stromu (computation tree) obr. 3.2(b). V´ vznikne rozeps´ an´ım Kripkeho struktury z poˇcáteˇ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ásadn´ıch nastaven´ı verifikace je urˇcen´ı granularity pˇrechod˚ u systému. 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ádˇej´ı se jako jedna jedin´ a atomick´ a operace. Bˇeˇznou chybou je nastaven´ı hrubé granularity, kdy se za atomické pˇrechody povaˇzuj´ı i takové pˇrechody, které v reálném systému atomické nejsou. T´ım m˚ uˇze doj´ıt k chybˇe pˇri verifikaci, model checking neodhal´ı chyby (errors), které v systému jsou. Oproti tomu nastaven´ı velmi jemné granularity m˚ uˇze zp˚ usobit detekován´ı chyb, které v reálném bˇehu systému nemohou nikdy nastat. a 2 promˇenné x, y a dva soubˇeˇznˇe proveditelné pˇrechody α, β. Pˇr´ıklad z [4]: Systém m´ α : x := x + y β : y := y + x s poˇcáteˇ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é slouˇz´ı pro práci 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ává 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ému, dále pˇredpokládejme, ˇze systém je implementov´ an pro pˇrechod α a β. V tom pˇr´ıpadˇe je nemoˇzné z´ıskat v´ ysledek x = 3 ∧ y = 3. Potom s granularitou α0 α1 α2 β0 β1 β2 m˚ uˇzeme dostat stavy, které v systému nikdy nenastanou. Na druhou stranu máme implementaci α0 α1 α2 β0 β1 β2 , ale systém modelujeme s α a β, potom nikdy nenalezneme chybu v systému. Syst´ emy se soubˇ eˇ znost´ı. Takové systémy se skládaj´ı z mnoˇziny komponent, které bˇeˇz´ı souˇcasnˇe. Jednotlivé komponenty si mezi sebou pˇredávaj´ı r˚ uzná data – komunikuj´ı. Zp˚ usob komunikace je v jednotliv´ ych systémech r˚ uzn´ y. Komunikace m˚ uˇze prob´ıhat asynchronnˇe – v ˇcasovém okamˇziku pracuje pouze jedna komponenta, nebo synchronnˇe – vˇsechny komponenty dˇelaj´ı krok ve stejném ˇcase. Komunikace prob´ıhá za pomoci sd´ılených promˇenných (shared variables) nebo zas´ıl´ an´ı zpr´ av (exchanging messages). Pokud program obsahuje sd´ılené promˇenné resp. promˇenné, ke kter´ ym má pˇr´ıstup v´ıce neˇz jeden proces, je tˇreba zajistit, aby ke sd´ılené promˇenné mˇel v dan´ y ˇcasov´ y okamˇzik pˇr´ıstup pouze jeden proces. V opaˇcném pˇr´ıpadˇe m˚ uˇze doj´ıt k nekonzistenci dat. Pro tyto u ´ˇcely slouˇz´ı synchronizaˇcn´ı pˇr´ıkazy, které jsou atomické a mohou m´ıt podobu pˇr´ıznaku ˇcekán´ı (wait) nebo zámk˚ u (lock/unlock).

3.2

Specifikace syst´ emu

Po form´ aln´ım nadefinov´ an´ı systému je tˇreba také formálnˇe nadefinovat vlastnosti, které se maj´ı verifikovat. Typickou formou specifikace vlastnost´ı pro model checking jsou následuj´ı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áln´ıch logik, pomoc´ı nichˇz se daj´ı nadefinovat formule, které vyajdˇruj´ı urˇcitou vlastnost systému. V temporáln´ı 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á se o logick´ y ˇcas. Vlastnosti typu nˇekdy (sometimes) nebo nikdy (never) jsou popsány speciáln´ımi temporáln´ımi operátory. Tempor´ aln´ı oper´ atory mohou b´ yt kombinovány libovolnˇe s booleovsk´ ymi spojkami nebo 12

vzájemnˇe vnoˇreny. Jednotlivé temporáln´ı logiky se liˇs´ı v operátorech, které poskytuj´ı a také v jejich sémantice. 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é v´ yroky (AP), booleovské spojky (∧, ∨, ¬), kvantifik´ atory cesty, temporáln´ı operátory. 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ákladn´ıch tempor´ aln´ıch oper´ ator˚ u: • Xp (next time) vlastnost p bude splnˇena v následuj´ıc´ım stavu dané cesty, • Fp (eventually) vlastnost p bude splnˇena nˇekdy na dané cestˇe, • Gp (globally) vlastnost p je splnˇena ve vˇsech stavech dané 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ém plat´ı formule p. V CT L∗ logice existuj´ı dva typy formul´ı stavové formule (state formulas) a formule cesty (path formulas). Logika CTL a LTL. Jsou podlogiky CT L∗ , rozd´ıl mezi nimi je v upoˇrádán´ı 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é jsou moˇzné z daného stavu obr. 3.3(b). Oproti tomu LTL (Linear Temporal Logic) je logika s lineárn´ım ˇcasem a operátory urˇcuj´ı události, které 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ázku model checkingu: Necht’, je dána Kripkeho struktura M = (S, S0 , R, L), pomoc´ı které je popsán verifikovan´ y systém a temporáln´ı formule f , reprezentuj´ıc´ı poˇzadovanou vlastnost, kterou má systém 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ému 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á 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á u nejvnitˇrenjˇs´ıch (dále nedˇeliteln´ ych) podformul´ı a postupuje se smˇerem ven k z´ıskán´ı mnoˇziny stav˚ u p˚ uvodn´ı formule ϕ. Typicky se prov´ ad´ı model checking z poˇcáteˇcn´ıho stavu (stav˚ u) systému, d´ıky tomu se ovˇeˇr´ı, zda je specifikace splnˇena v celém systému (S0 ⊆ Sϕ ) nebo jeho ˇcásti – formule je splnˇena v poˇzadovan´ ych stavech. Existuj´ı r˚ uzné algoritmy, pomoc´ı nichˇz se urˇcuj´ı mnoˇziny stav˚ u, ve kter´ ych je poˇzadovan´ a formule splnˇena. Nicménˇe pro v´ ypoˇcet mnoˇziny u r˚ uzn´ ych formul´ı, které obsahuj´ı jiné temporáln´ı oper´ atory je tˇreba aplikovat r˚ uzné algoritmy, jednotlivé algoritmy lze naj´ıt napˇr´ıklad v [4]. Algoritmy pro ovˇeˇren´ı formule jsou zaloˇzeny na procházen´ı stavov´ ym prostorem a jejich hlavn´ım problém se tedy st´ av´ a exploze stavového prostoru.

3.4

Probl´ em stavov´ e exploze

Exploze stavového prostoru je kritick´ ym problémem model checkingu (state space explosion problem), kde verifikace spoˇc´ıvá v generován´ı stavového prostoru. Velikost stavového prostoru roste exponenci´ alnˇe s velikost´ı verifikovaného modelu resp. systému [21]. Z toho d˚ uvodu je prakticky model checking bez redukce stavového prostoru v praxi nepouˇziteln´ y. Exploze stavového prostoru spoˇc´ıvá v nedeterminismu – ve velkém mnoˇzstv´ı moˇznost´ı stav˚ u, kter´ ymi m˚ uˇze systém pokraˇcovat z aktuáln´ıho stavu. Pro ˇreˇsen´ı problému stavové exploze existuj´ı r˚ uzné pˇr´ıstupy [7, 15, 21, 23]. Jedn´ım z moˇzn´ ych dˇelen´ı tˇechto pˇr´ıstup˚ u je následuj´ıc´ı: • Pˇ redzpracov´ an´ı (preprocessing). Jeˇstˇe pˇred zaˇcátkem provádˇen´ı model checkingu se vykon´ a pˇredzpracov´ an´ı verifikovaného systému. Do této skupiny patˇr´ı: slicing a jemu podobné techniky zaloˇzené na statické analýze, jejich podstatou je oˇr´ıznut´ı“ ve” rifikovaného systému pouze na tu ˇcást, která m˚ uˇze ovlivnit verifikovanou vlastnost. Vlastn´ı model checking se provád´ı pouze nad oˇr´ıznutou“ ˇcást´ı systému. Dalˇs´ı meto” dou je nad aproximace, pomoc´ı n´ı je moˇzné zjistit, co ovlivˇ nuje zkoumanou oblast a d´ ale pracovat se zvolenou ˇcást´ı systému. Dále je moˇzné pouˇz´ıt explicitn´ı urˇcen´ı atomické sekce. Uˇzivatel s´ am zadá oblasti, které maj´ı b´ yt vykonány atomicky a nemá se rozgenerov´ avat jejich stavov´ y prostor. V tom pˇr´ıpadˇe sám uˇzivatel zaruˇcuje, ˇze j´ım zadan´ a atomick´ a sekce nezp˚ usob´ı nenalezen´ı chyby. Existuj´ı i metody, které dok´ aˇz´ı urˇcit atomické sekce automaticky. Tyto sekce jsou ovˇsem vˇetˇsinou velice jednoduché a 14

neefektivn´ı vzhledem k redukci stavového 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ádat se stavovou exploz´ı je komprimace stavového prostoru. BDD (binary decision diagram) je jednou z moˇznost´ı jak komprimovat stavov´ y prostor, jednotlivé stavy jsou reprezentov´ any pomoc´ı formul´ı. Dalˇs´ı moˇznost´ı je efektivn´ı uloˇzen´ı stavu v pamˇeti, neukládaj´ı se celé novˇe generované stavy, ale pouze zmˇeny mezi jiˇz uloˇzen´ ym stavem a novˇe generovan´ ym. Abstrakce stav˚ u je metoda, která redukuje informace o procesech. Neuchov´ av´ a se informace o pˇresném poˇctu proces˚ u, ale pouze informace zda na daném ˇr´ adku k´ odu je 0, 1 nebo ∞ proces˚ u, jedná se o nadaproximaci. • Redukce stavov´ eho prostoru. Redukce stavového prostoru neznamená pouze efektivn´ı proch´ azen´ı stavového prostoru, ale také redukce poˇctu stav˚ u. Redukce stav˚ u m˚ uˇze prob´ıhat bud’ pˇredem nebo za bˇehu programu – nˇekteré generované stavy nejsou z hlediska verifikované vlastnosti zaj´ımavé. Metody pro redukci stavového prostoru jsou: symmetry reduction, Petri-net unifolding (rozvinut´ı petriho s´ıtˇe do lineárn´ıho stromu). Zaj´ımavé redukce pro programy se soubˇeˇznost´ı jsou Partial order reduction“ (POR) ” a on-the-fly model checking“. POR je zaloˇzená na redukován´ı generován´ı stavového ” prostoru. V programech existuj´ı nezávislé pˇrechody u kter´ ych nezáleˇz´ı na poˇrad´ı jejich vykon´ an´ı, po jejich proveden´ı se verifikace dostává do shodného stavu. Takové pˇrechody (operace) se typicky vyskytuj´ı u v´ıce vláknov´ ych aplikac´ı, kdy r˚ uzná válkna prov´ ad´ı na sobˇe nez´ avislé operace a nezáleˇz´ı tedy na poˇrad´ı jejich provádˇen´ı. Ukázka ˇc´ asti vygenerovaného stavového prostoru, kde je moˇzné tuto generovanou ˇcást redukovat pouze na proveden´ı jednoho pr˚ uchodu je na obr. 3.4.

Obr´ azek 3.4: Uk´ azka redukce stavového prostoru pomoc´ı POR Metoda on-the-fly je zaloˇzena na souˇcasném generován´ı stavového prostoru a ovˇeˇrov´ an´ı vlastnosti systému najednou. Pˇri generován´ı stavového prostoru se souˇcasnˇe verifikuje, zda je vlastnost v daném generovaném stavu splnˇena. Pokud dojde k nalezen´ı protipˇr´ıkladu verifikované vlastnosti, generován´ı stavového prostoru konˇc´ı. Verifikace dospˇela k z´ avˇeru bez nutnosti rozgenerovávávat cel´ y stavov´ y prostor a t´ım k jeho redukci.

15

• Kompoziˇ cn´ı model checking (Compositional of MC). Jedná se o rozdˇelen´ı systému na komponenty, kde u kaˇzdé komponenty sledujeme urˇcité vlastnosti. Nakonec z tˇechto d´ılˇc´ıch vlastnost´ı komponent odvod´ı vlastnosti celého systému. Existuj´ı i dalˇs´ı metody pro redukci stavového prostoru, které zde nejsou uvedeny. Také je moˇzné jednotlivé metody vhodn´ ym zp˚ usobem kombinovat, a t´ım doc´ılit vyˇsˇs´ı efektivnosti pˇri redukci stavového prostoru.

3.5

Bounded Model Checking

Bounded model checking resp. ohraniˇcen´ y model checking se pouˇz´ıvá pro verifikaci koneˇcnˇe stavov´ ych systém˚ u. Bounded model checking m˚ uˇze u ´ˇcinnˇe redukovat problém splnitelnosti booleovské formule – SAT . Tento problém byl jedn´ım z d˚ uvod˚ u pro vytvoˇren´ı této metody [3]. Základn´ı myˇslenkou bounded model checkingu je ovˇeˇren´ı urˇcité vlastnosti systému pouze za pomoci koneˇcného prefixu cesty v systému. Nalezen´ı d˚ ukazu o splnˇen´ı nebo vyvrácen´ı urˇcité vlastnosti systému se provád´ı v koneˇcném poˇctu krok˚ u. Prohledáván´ı stavového systému je omezeno na pˇredem danou délku k. Pomoc´ı omezen´ı prohledáván´ı stavového systému se omez´ı i verifikace poˇzadované vlastnosti. Verifikace je omezena na verifikaci prefixu cesty, kter´ a m´ a délku k. V praxi se vˇetˇsinou omezená délka cesty prodluˇzuje na takovou dobu, dokud se nez´ısk´ a d˚ ukaz o splnˇen´ı/vyvrácen´ı verifikované 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ého z pˇredchoz´ıch stav˚ u (obr. 3.5(b)) jedná se o reprezentaci nekoneˇcné cesty pomoc´ı koneˇcného 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ém chován´ı systému. Nelze zverifikovat vlastnosti, které poˇzaduj´ı, aby urˇcit´ a vlastnost byla platná nekonˇcnˇe dlouho. Pokud prefix neobsahuje zpˇetnou smyˇcku nen´ı zn´ amé chován´ı systému za stavem sk .

Obr´ azek 3.5: Dvˇe moˇznosti omezené cesty Definice pro cestu, kter´ a obsahuje zpˇetnou smyˇcku je následuj´ı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é je cesta π: (k, l)-loop, pak naz´ yv´ ame cestu π: k-loop. Pokud na cestˇe délky k existuje pˇrechod z posledn´ıho stavu cesty sk do nˇekterého z pˇredeˇsl´ ych stav˚ u cesty sl , pak je moˇzné danou ˇcást cesty neomezenˇe krát opakovat k-loop. Sémantika model checkingu na limitovan´ ych cestách se naz´ yvá bounded semantics. Vyuˇz´ıvá se prvn´ıch k + 1 stav˚ u cesty (s0 , . . . , sk ), jedná 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áln´ı sémantika model checkingu. Tato sémantika lze vyuˇz´ıt vzhledem k faktu, ˇze pokud cesta obsahuje zpˇetnou smyˇcku jsou nekoneˇcné vlastnosti 16

cesty obsaˇzeny v jej´ım koneˇcném prefixu. Formálnˇ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élky 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é ) sémantice, jestliˇze existuje index i ≥ 0, takov´ y, kde p je splnˇena na sufixu (πi ) cesty π. Pokud je pouˇzita omezen´ a sémantika, potom k+1-n´ı stav π(k) nem´ a n´ asledovn´ıka a nen´ı tedy moˇzné tuto sémantiku definovat rekurzivnˇe pomoc´ı sufix˚ u cesty (πi ). Z toho d˚ uvodu se zavád´ı znaˇcen´ı π |=ik f , kde i je aktuáln´ı 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ásledovnˇe: Necht’ k ≥ 0, cesta π nen´ı k-loop. Potom LT L formule f je splnˇena na cestˇe π délky 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éto kapitoly o bounded model checkingu zle uvést následuj´ı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ásleduj´ıc´ı theorém 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ém ˇr´ık´ a, pokud zle z´ıskat takovou délku k, na které je formule splnˇena, potom omezen´ a a neomezen´ a sémantika jsou ekvivalentn´ı.

3.6

Navigace stavov´ ym prostorem

V projektu SHADOWS se bounded model checking vyuˇz´ıvá pro zverifikován´ı okol´ı léˇcené chyby, nen´ı tedy c´ılem provést bounded model checking z poˇcáteˇcn´ıho stavu (s0 ), ale z nˇejakého konkrétn´ıho stavu ve stavovém prostoru systému. Aby bylo moˇzné z toho stavu provést bounded model checking, je potˇreba nejprve daného stavu dosáhnout, proj´ıt stavov´ y prostor do konkrétn´ıho stavu. K tomuto u ´ˇcelu existuj´ı r˚ uzné metody [14, 20], které slouˇz´ı k navigaci stavov´ ym prostorem do poˇzadovaného stavu. Tyto metody mohou b´ yt následuj´ıc´ı. • Record&Replay trace. Tato strategie pro navigaci stavov´ ym prostorem je zaloˇzena na zaznamen´ an´ı bˇehu programu (trace) a posléze pˇrehrán´ı této cesty ve zvoleném 17

model checkeru. Pomoc´ı z´ aznamu bˇehu programu se je moˇzné navádˇet stavov´ ym prostorem aˇz do m´ısta opravy chyby, ze kterého je moˇzné spustit bounded model checking. V´ yhodou této metody je zaznamenán´ı celé cesty provádˇen´ı programu. D´ıky tomu je moˇzné provést bounded model checking ne pouze z chybového stavu programu, ale z kteréhokoliv stavu, kter´ y mu na cestˇe pˇredcház´ı. Zásadn´ı nev´ yhodou této metody je nutnost ukl´ adán´ı celého bˇehu programu, a t´ım zpomalen´ı chodu aplikace. Dalˇs´ı nev´ yhodou je pamˇet’ová nároˇcnost, pro záznam cesty programu je zaˇ ım delˇs´ı dobu program bˇeˇz´ı, t´ım je potˇreba v´ıce pamˇeti potˇreb´ı velké mnoˇzstv´ı dat. C´ pro z´ aznam cesty. Minim´ alnˇe stejnˇe dlouhá doba jako pro záznam cesty je také potˇreba pro pˇrehr´ an´ı zaznamenané cesty. Proto se tato metoda nehod´ı pro navigaci stavov´ ym prostorem u systém˚ u, které jsou dlouhodobˇe v chodu. Aby bylo moˇzné pˇrehr´ at zaznamenanou cestu bˇehu programu, je tˇreba ukládat relevantn´ı informace jako informace o aktuáln´ım vláknˇe, vykonané byte-code instrukci atd. • Store&Restore state. Dalˇs´ı strategie pro z´ıskán´ı poˇzadovaného stavu ze stavového prostoru systému je zaloˇzena na uloˇzen´ı a opˇetovném obnoven´ı stavu. Neprve se uloˇz´ı aktu´ aln´ı stav bˇeˇz´ıc´ıho programu a následnˇe se uloˇzen´ y stav obnov´ı ve zvoleném model checkeru. Po obnoven´ı uloˇzeného stavu je z nˇej moˇzné provést bounded model checking. Nev´ yhodou této metody je nemoˇznost zaˇc´ıt bounded model checking z jiného neˇz z pouze uloˇzeného stavu. Nen´ı moˇzné jako u pˇredeˇslé metody zahájit bounded model checking z nˇejakého z pˇredcházej´ı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ém stavu je tˇreba provést pˇr´ısluˇsnou zmˇenu i v ukl´ adaném resp. obnoveném stavu. Napˇr. u Java program˚ u m˚ uˇze doj´ıt ke zmˇenˇe verze Java virtáln´ıho stroje (JVM) nebo zmˇena verze model checkeru m˚ uˇze zp˚ usobit také nutnost zmˇeny v ukládán´ı a obnoven´ı stavu. Nev´ yhoda moˇznosti verifikace pouze z uloˇzeného stavu se dá ˇcásteˇcnˇe odstranit opˇetovn´ ym ukládán´ım stav˚ u systému napˇr. po urˇcitém ˇcasovém intervalu. Nicménˇe stále tu z˚ ustává nutnost uloˇzen´ı veˇsker´ ych potˇrebn´ ych informac´ı pro obnoven´ı stavu systému v model checkeru. Tˇechto informac´ı je znaˇcná 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ádan´ ych informac´ı. Naopak v´ yhodou je fakt, ˇze nezp˚ usobuje trvalé zpomalen´ı bˇehu programu, ke zpomalen´ı docház´ı pouze v dobˇe ukl´ ad´ an´ı stavu. • Dalˇ s´ı Strategie. V´ yˇse uvedené strategie se daj´ı r˚ uznˇe kombinovat, napˇr. po urˇcitém ˇcasovém intervalu m˚ uˇze docházek k ukládán´ı stavu systému a zaznamenáván´ı cesty z tohoto stavu. Po urˇcité dobˇe dojde k pˇremazán´ı uloˇzené 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á se o metodu, pomoc´ı které se ne” ukl´ adaj´ı vˇsechny informace o bˇehu programu, ale pouze ty informace, které jsou relevantn´ı k pˇrehr´ an´ı bˇehu programu do poˇzadovaného stavu.

18

Kapitola 4

Java PathFinder Projekt SHADOWS se vˇenuje léˇcen´ı program˚ u napsan´ ych v jazyce Java, a proto bylo vyb´ıráno z model checker˚ u vhodn´ ych pro verifikaci Java program˚ u. Byly zkoumány 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é uˇzivatelské rozhran´ı, a také r˚ uzné algoritmy po model checking (pro redukci stavového prostoru, vyhled´ avac´ı heuristiky, abstraktn´ı definice atd.). Bogor lze pouˇz´ıt i jako plugin do Eclipse. (Eclipse je integrované v´ yvojové 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é ho vyuˇz´ıt pro v´ yuku z´ akladn´ıch algoritm˚ u model checkingu a jeho podstaty. Zároveˇ n lze Bogor vyuˇz´ıt pro klasick´ y model checking. • Bandera [8] je model checker pro programy napsané v Javˇe, které obsahuj´ı paralelismus. Bandera pˇrekl´ ad´ a zdrojov´ y kód v Jave do vstupn´ıho jazyka nˇejakého jiného existuj´ıc´ıho model checkeru jako napˇr´ıklad SPIN, SMV, SAL, atd. Tyto jiné model checkery zabezpeˇcuj´ı vlastn´ı verifikaci systému. Po zverifikován´ı systému Bandera umoˇzn ˇuje namapovat v´ ystup verifikace ze zvoleného model checkeru na p˚ uvodn´ı Java k´ od. • Java PathFinder(JPF) [9] je model checker, kter´ y provád´ı verifikaci nad Java byte-codem. JPF je implementován jako speciáln´ı Java virtuáln´ı stroj (JVM), kter´ y v sobˇe pˇrehr´ av´ a programy urˇcené k verifikaci. Bˇehem pˇrehráván´ı programu kontroluje poˇzadované vlastnosti nebo specifikace systému. JPF je implicitnˇe nastaven na detekci deadlocks, unhandled exception, violations of assertions. Zároveˇ n JPF m˚ uˇze detekovat i dalˇs´ı vlastnosti systému, které se daj´ı zadat pomoc´ı parametr˚ u. Nebo je moˇzné naimplementovat dalˇs´ı vlastn´ı speciáln´ı souˇcásti JPF pro verifikaci poˇzadovan´ ych vlastnost´ı systému. 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ého prostoru, r˚ uzné heuristiky pro prohled´ av´ an´ı stavového prostoru atd. Model checker Bogor je také moˇzné rozˇs´ıˇrit o vlastn´ı moduly, nicménˇe v´ yhodou JPF je jeho nasazen´ı jiˇz na reálné systémy. Hlavn´ı nev´ yhodu model checkeru Bandera je nutnost transformovat vstupn´ı zdrojov´ y kódu programu do jiného jazyka. T´ım je zp˚ usobena nemoˇznost selodáván´ı 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é v jazyce Java [9, 13, 17, 19, 22]. Verifikace se provád´ı na u ´rovni Java byte-codu. JPF pˇredstavuje speciáln´ı virtuáln´ı stroj, ve které se spouˇst´ı verifikovan´ y systém. Z d˚ uvodu bˇehu aplikace pˇr´ımo v JPF, nen´ı nutné spouˇstˇet program v´ıcekrát nebo ho nˇejak´ ym zp˚ usobem upravovat. JPF neprov´ ad´ı jednoduch´ y bˇeh programu, ale vykonává rovnou verifikaci za bˇehu (runtime). Prohled´ av´ an´ı stavového prostoru prob´ıhá pomoc´ı r˚ uzn´ ych prohledávac´ıch strategi´ı, které budou pops´ any d´ ale. Samotn´ y Java PathFinder je také napsán v jazyce Java, jeho architektura je rozdˇelena do modul˚ u, které umoˇzn ˇuj´ı dalˇs´ı rozˇsiˇritelnost. Je moˇzné rozˇsiˇrovat jiˇz existuj´ıc´ı moduly o dalˇs´ı funkce nebo implementovat nové moduly. Pokud JPF bˇehem verifikace nalezne chybu (error), standardnˇe vyp´ıˇse cestu (trace), která k chybˇe vedla, a také vyp´ıˇse relevantn´ı informace o bˇehu (aktuáln´ı vlákno, jednotlivé ˇrádky zdrojového kódu, apod), tyto informace mohou pomoci opravit nalezenou chybu. Základn´ı 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é moduly, které definuj´ı jak´ ym zp˚ usobem bude verifikace prob´ıhat. Pomoc´ı nastaven´ı JPF se urˇc´ı, jaká vyhledávac´ı strategie (search strategy) bude pouˇzita pro prohled´ av´ an´ı stavového prostoru, které listenery (search listener) budou s touto strategi´ı pouˇzity (pro z´ısk´ an´ı poˇzadovan´ ych informac´ı). Dále lze nastavit generován´ı moˇznost´ı (choice generator) nedeterminismu, jedná se o hodnoty vstupn´ıch dat, prokládán´ı vl´ aken atd. Dalˇs´ı nastaven´ı umoˇznuje pˇrilinkovat listener zaloˇzen´ y na sledován´ı jednotliv´ ych krok˚ u virtuáln´ıho stroje. JPF tedy systematicky, podle zvolené strategie, prohledává stavov´ y prostor vstupn´ıho programu, pokud dojde k detekci chyby. JPF uˇzivateli poskytne zprávu o verifikaci, kter´ a obsahuje cestu, která vedla k chybˇe, typ detekovaného problému a dalˇs´ı informace, které byly nastaveny uˇzivatelem.

20

JPF umoˇzn ˇuje verifikovat programy, které maj´ı v´ıce vláken, nicménˇe neumoˇzn ˇuje verifikaci soubˇeˇzného bˇehu vl´ aken (na dvou procesorech). JPF pouze simuluje soubˇeˇznost vláken. Zároveˇ n neumoˇzn ˇuje zverifikovat programy, které obsahuj´ı nativn´ı metody (metody psané v jiném jazyce neˇz Java). JPF neobsahuje podporu vˇsech knihoven Java, pokud program obsahuje urˇcité knihovny, nen´ı ho moˇzné verifikovat [9]. Nicménˇe umoˇzn ˇuje vytvoˇren´ı nativn´ıch metod, které jsou v rámci verifikace brány jako atomické ˇc´ asti k´ odu a neprov´ ad´ı se nad nimi verifikace. Metoda je vykonána bez proklád´ an´ı jin´ ymi instrukcemi k´ odu. D´ıky tomuto mechanizmu je moˇzné verifikovat programy obsahuj´ıc´ı knihovny nebo metody, které nechceme brát v u ´vahu do verifikace. Pro verifikaci vstupn´ıch dat obsahuje JPF specializované API, pomoc´ı kterého lze urˇcit, jak´ ych hodnot mohou tyto data nab´ yvat. Jinou moˇznost´ı je volba pro náhodn´ y v´ ybˇer hodnot vstupn´ıch dat. Nast´ınˇené vlastnosti JPF budou dále rozepsány. JPF m˚ uˇze simulovat nedeterminismus, pro generov´ an´ı nedeterminismu obsahuje JPF dva mechanismy: • Backtracking znamen´ a, ˇze se JPF m˚ uˇze vrátit k vykonanému stavu a nahradit zvolenou moˇznost (hodnotu promˇenné), z které vznikl nedeterminismus, jinou moˇznost´ı a t´ım vygenerovat nov´ y stav a následnˇe generovat cestu. Tento zp˚ usob se aplikuje na postupné rozgenerov´ an´ı vˇsech moˇzn´ ych plánovac´ıch sekvenc´ı (moˇzn´ ych hodnot). • State matching je zaloˇzen na mechanismu vyhnut´ı se generován´ı jednoho stavu systému 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ému stavu a zde se pokraˇcuje s verifikac´ı.

4.2

Specifikace

JPF umoˇzn ˇuje verifikovat r˚ uzné vlastnosti podle zadan´ ych poˇzadavk˚ u. V JPF existuj´ı tˇri základn´ı 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ého kódu programu a slouˇz´ı k z´ısk´ an´ı informac´ı z´ avisl´ ych pˇr´ımo na datech aplikace. Jedná se o u ´ˇcinné z´ıskán´ı informac´ı a chov´ an´ı systému. Nev´ yhodou této metody je nutnost zásahu do zdrojového kódu programu. Zároveˇ n m˚ uˇze doj´ıt k n´ ar˚ ustu stavového prostoru, pokud se maj´ı zverifikovat i pˇridané 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é tyto vlastnosti kontrolovat za bˇehu programu pˇri kaˇzdé zmˇenˇe pomoc´ı search objektu. Základn´ı specifikace, které jsou implicitnˇe v JPF pomoc´ı tohoto mechanizmu kontrolovány jsou následuj´ı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á se o dvˇe tˇr´ıdy, pomoc´ı kter´ ych jsou naimplementovány r˚ uzné listnery. Ty slouˇz´ı k z´ıskáván´ı r˚ uzn´ ych informac´ı o bˇehu programu. V JPF je jiˇz ˇrada tˇechto listener˚ u naimplementována. Jednotlivé listenery d´ avaj´ı napˇr´ıklad následuj´ıc´ı inforamce: SearchMonitor – v´ ypis statistick´ y informac´ı o bˇehu programu (poˇcet vygenerovan´ ych stav˚ u, velikost vyuˇzité pamˇeti, atd.),

21

HeapTracker – v´ ypis vyuˇzit´ı haldy (heap) na vˇsech cestách verifikace, StateSpaceDot – vytvoˇr´ı graf vygenerovaného stavového prostoru bˇehem verifikace, MethodTracker – v´ ypis vˇsech metod, které byly bˇehem verifikace volány, atd. Mechanizmus listener˚ u umoˇznuje z´ıskávát informace o programu na tˇrech u ´rovn´ıch. Obecné listenery poskytuj´ı informace o programu z´ıskané pomoc´ı rozhran´ı, nacházej´ı se mimo program. Jedn´ a se o SearchListnery a VMListenery. Druh´ ym typem listener˚ u jsou specializované vyhled´ avac´ı listenery, ty se opˇet nacház´ı mimo program a jsou k nˇemu pouze linkov´ any. Nicménˇe jsou navrˇzeny pro z´ıskán´ı specifick´ ych informac´ı o programu, nebo jsou navrˇzeny ke konkrétn´ımu u ´ˇcelu, napˇr. gov.nasa.jpf.search.heuristic.BFSHeuristic slouˇz´ı pro nastaven´ı prohled´ av´ an´ı stavového prostoru pomoc´ı BFS strategie. Tˇret´ım typem listener˚ u jsou vnitˇrn´ı listenery, které se nacház´ı v konkrétn´ım bal´ıku uvnitˇr implementace JPF a umoˇznuj´ı z´ısk´ avat inforamce z daného konkrétn´ıho bal´ıˇcku. Napˇr. bal´ık gov.nasa.jpf.jvm.bytecode obsahuje jednotlivé instrukce byte-codu a tedy listener v tomto bal´ıku umoˇznuje z´ıskat nebo mˇenit primárn´ı informace o jednotliv´ ych instrukc´ıch bytecodu, které jsou ostatn´ım listener˚ um skryty. Nejˇsirˇs´ı vyuˇzit´ı nab´ızej´ı obecné listenery, které umoˇznuj´ı z´ıskat nebo mˇenit informace v programu bezpeˇcn´ ym“ zp˚ usobem. ” SearchListenery lze pouˇz´ıt pro monitorován´ı prohledávac´ıho procesu stavov´ ym prostorem. Umoˇznuj´ı zaznamen´ avat napˇr´ıklad informace o jednotliv´ ych stavech systému nebo vytváˇret graf stavového prostoru, kter´ y obsahuje inforamce o postupu stavov´ ym prostorem i základn´ı informace o jednotliv´ ych stavech. VMListenery mohou zaznamenávat nebo mˇenit jednotlivé kroky provádˇen´ı programu na u ´rovni virtu´ aln´ıho stroje. VMListener zle napˇr´ıklad pouˇz´ıt pro monitorován´ı vykon´ an´ı byte-code instrukc´ı MONITORENTER a MONITOREXIT, které 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ést dvˇema zp˚ usoby. Prvn´ım zp˚ usobem je statické nastaven´ı vlastnost´ı JPF pˇred jeho spuˇstˇen´ım. Tento mechanizmus umoˇznuje zvolit jednotlivé listnery, které maj´ı b´ yt pˇrilinkovány a také nastavit parametry pˇridávan´ ych listener˚ u. Druhou moˇznost´ı je dynamické pˇridán´ı listener˚ u do bˇehu JPF, lisntener je pˇrid´ an pˇr´ımo do zdrojového k´ odu aplikace a vyvolán aˇz za bˇehu.

4.3

Prohled´ av´ an´ı stavov´ eho prostoru

JPF obsahuje r˚ uzné nastavitelné vyhledávac´ı strategie (Search strategies) pro prohledáv´ an´ı stavového prostoru verifikovaného systému. Naimplementovány jsou základn´ı vyhledávac´ı strategie jako DF S (Depth First Search – prohledáván´ı do hloubky), BF S (Breadth First Search – prohled´ av´ an´ı do ˇs´ırky), A∗ , Best-F irst or BeamSearch. Zároveˇ n je moˇzné nastavit r˚ uzné parametry u jednotliv´ ych strategi´ı jako hloubku prohledáván´ı, prioritu stav˚ u, apod. JPF obsahuje i strategie pro náhodn´ y bˇeh programem napˇr.RandomSearch nebo P athSearch. Vhodn´ ym v´ ybˇerem prohledávac´ı strategie a jej´ıho nastaven´ı lze ˇr´ıdit generován´ı stavového prostoru a t´ım doc´ılit zverifikován´ı zadané specifikace systému dˇr´ıve, nemus´ı doj´ıt k explozi stavového prostoru.

Redukce stavov´ eho prostoru. Java PathFinder obsahuje r˚ uzné mechanizmy, které maj´ı za c´ıl omezit explozi stavového prostoru. V kapitole 3, která pojednává o Model checkingu jsou vyps´ any r˚ uzné pˇr´ıstupy jak doc´ılit redukce stavového prostoru. Mechanizmy redukce v JPF jsou zaloˇzeny na uveden´ ych principech.

22

• Partial Order Reduction (POR) je metoda, která u ´ˇcinnˇe redukuje poˇcet generovan´ ych stav˚ u. Poˇcet pl´ anovan´ ych rozhodován´ı (vˇetven´ı) m˚ uˇze b´ yt znaˇcnˇe omezen, pokud seskup´ıme vˇsechny instrukce v konkrétn´ım vláknˇe, které nemohou zp˚ usobit zmˇenu mimo toto vl´ akno. Takové instrukce jsou seskupeny do jednoho pˇrechodu, pokud program obsahuje hodnˇe vláken, které mezi sebou nesd´ılej´ı data, m˚ uˇze b´ yt redukce stavového prostoru znaˇcná. Oproti tomu pokud program obsahuje mnoˇzstv´ı sd´ılen´ ych dat nebo prov´ azan´ ych operac´ı, redukce pomoc´ı POR je minimáln´ı. JPF prov´ ad´ı POR on-the-fly“, pˇri provádˇen´ı se nespoléhá na statickou anal´ yzu, ale vy” hodnocuje atomické sekce za bˇehu, resp. urˇcuje, které instrukce mus´ı b´ yt vyhodnoceny jako hraniˇcn´ı daného pˇrechodu do nového stavu. Pokud je POR pˇri spuˇstˇen´ı JPF povolena, vykon´ avaj´ı se vˇsechny instrukce v aktuáln´ım vláknˇe do okamˇziku neˇz dalˇs´ı instrukce zp˚ usob´ı zmˇenu v plánován´ı (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é zp˚ usobuj´ı zmˇenu v plánován´ı, na obr. 4.2 jsou tyto instrukce vyobrazeny s jejich z´ avislostmi.

Obr´ azek 4.2: Instrukce maj´ıc´ı vliv na plánován´ı [9] • Choice Generatory (CG) jsou dalˇs´ım d˚ uleˇzit´ ym mechanizmem pro práci 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ánován´ı. CG jsou jedn´ım z moˇzn´ ych ˇreˇsen´ı jak se vyrovnat s problémem vstupn´ıch dat. Pomoc´ı rozhran´ı gov.nasa.jpf.jvm.Verify lze zadat, jak´ ych hodnot maj´ı urˇcité promˇenné nab´ yvat a takto specifikovan´ ymi moˇznostmi hodnot promˇenn´ ych se provád´ı verifikace. Pokud jsou vstupn´ı data typu boolean nen´ı problém provést verifikaci nad vˇsemi moˇznostmi hodnot, u typu integer jiˇz nast´ av´ a problém s vygenerován´ım vˇsechn moˇznost´ı hodnot a u promˇenné typu float je to jiˇz velmi nevhodné.

23

K ˇreˇsen´ı tohoto problému 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á hodnot ze zvoleného intervalu a u typu float i po vymezen´ı intervalu z˚ ustává velké mnoˇzstv´ı moˇzn´ ych hodnot. Proto je zde dalˇs´ı mechanizmus jak urˇcit interval i krok mezi jednotliv´ ymi hodnotami. Pˇresné hodnoty promˇenné 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á 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é generovat vˇsechny moˇzné hodnoty promˇenné, pokud je relevantn´ı pouze vztah hodnoty k prahu).

Obr´ azek 4.3: Instrukce maj´ıc´ı vliv na plánován´ı [9]

• Explicitn´ı urˇ cen´ı Atomicity spoˇc´ıvá v proveden´ı urˇcitého kódu programu atomicky. Ta ˇc´ ast k´ odu, kter´ a má b´ yt provedena atomicky je explicitnˇe urˇcena uˇzivatelem pomoc´ıVerify.beginAtomic() a Verify.endAtomic(). Zároveˇ n mus´ı uˇzivatel zaruˇcit, ˇze d´ıky této atomicitˇe nedojde k nenalezen´ı chyby v systému.

4.4

Rozˇ siˇ ritelnost

Pro vyuˇzit´ı JPF v projektu SHADOWS je podstatná jeho vlastnost rozˇsiˇritelnosti. JPF je open source a je tedy moˇzné doimplementovat jiné vlastn´ı moduly nebo funkce. Pro z´ısk´ an´ı dalˇs´ıch vlastnost´ı z verifikovaného systému je moˇzné vytváˇret nové listenery, nové prohledávac´ı strategie. Ty mohou b´ yt modifikac´ı jiˇz naimplementovan´ ych a upraveny pro konkrétn´ı u ´ˇcel nebo je moˇzné vytv´ aˇret nové 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áce bylo navrhnout a posléze implementovat metodu pro ovˇeˇren´ı opravy v projektu SHADOWS. C´ılem opravy je automatické léˇcen´ı chyb v Java programech. Léˇcen´ı se specializuje na chyby vzniklé soubˇeˇznost´ı, kapitola 2. Pro kontrolu opravy byla zvolena formáln´ı metoda Model Checking, kapitola 3. Z d˚ uvodu problému stavové exploze nen´ı moˇzné provést cel´ y model checking nad reáln´ ym systémem. Proto pro vlastn´ı verifikaci byla zvolena modifikace – bounded model checking kapitola 3.5. Klasick´ y bounded model checking spoˇc´ıvá v omezen´ı hloubky stavového prostoru, kter´ y se má prohled´ avat. Pokud m´ a b´ yt bounded model checking pouˇzit pro ovˇeˇren´ı opravy, nen´ı c´ılem provést model checking od zaˇcátku bˇehu programu do pˇredem definované hloubky, ale zverifikovat konkrétn´ı ˇc´ ast programu, kde byla aplikována oprava. K tomuto u ´ˇcelu uzné strategie pro navigaci stavov´ ym prostorem do chybyly v kapitole 3.6 uvedeny i r˚ bového stavu. Potom je jiˇz moˇzné provést bounded model checking ne z poˇcáteˇcn´ıho stavu, ale z daného stavu (napˇr. chybového stavu) a zverifikovat poˇzadované vlastnosti. K navigaci stavov´ ym prostorem byla vybrána strategie Record&Replay trace. Tato strategie byla vybrána pro moˇznost provést bounded model checking ne pouze z podezˇrelého (chybového) stavu, ale i z nˇekterého z pˇredeˇsl´ ych stav˚ u. Tato vlastnost je velmi v´ yhodná z hlediska ovˇeˇren´ı opravy. Jako podezˇrel´ y stav je detekován chybov´ y stav, ale oprava m˚ uˇze provést zmˇeny v prov´ adˇen´ı programu nejenom po chybovém stavu, ale také pˇred n´ım (napˇr. pˇrid´ an´ı zámku). Proto je moˇznost zaˇc´ıt verifikaci z nˇekterého z pˇredeˇsl´ ych stav˚ u v´ yhodná. Tento fakt pˇreb´ıj´ı nev´ yhody této metody jako nároˇcnost na zaznamenané informace a zpomalen´ı bˇehu aplikace. Pro vlastn´ı implementaci byl zvolen model checker Java PathFinder, kter´ y sk´ ytá velké moˇznosti rozˇsiˇritelnost o dalˇs´ı funkce (Listenery a Search Strategie). Listenery lze vyuˇz´ıt k záznamu potˇrebn´ ych informac´ı, lze tedy listenery pouˇz´ıt k záznamu bˇehu programu. Dalˇs´ı ˇcást spoˇc´ıv´ a v pˇrehr´ an´ı zaznamenané cesty a navigaci do konkrétn´ıho stavu. K tomuto u ´ˇcelu lze vyuˇz´ıt vyhled´ avac´ı strategie, které je samozˇrejmˇe opˇet potˇreba upravit a doimplementovat pro pˇrehr´ an´ı zaznamenané cesty. Pokud se dostaneme do poˇzadovaného stavu stavového prostoru, je moˇzné provést bounded model checking, kter´ y se provád´ı také pomoc´ı modifikované prohled´ avac´ı strategie, která obsahuje vlastnosti bounded model checkingu. Kapitola je d´ ale rozdˇelena do d´ılˇc´ıch podkapitol, kde kaˇzdá podkapitola popisuje urˇcitou ˇcást implementace. V prvn´ı podkapitole je uvedena implementace zvolené metody pro navigaci skrz stavov´ y prostor. Jedná se o strategii Record&Replay Trace. V prvn´ı fázi byla tato metoda cel´ a implementov´ ana v Java PathFinderu, pro ovˇeˇren´ı a otestován´ı funkˇcnosti metody a ovˇeˇren´ı pouˇzitelnosti pomoc´ı zvoleného model checkeru. Dále je zde uveden jednoduch´ y pˇr´ıklad, kter´ y demonstruje funkˇcnost zvolené strategie. 25

Druh´ a podkapitola se vˇenuje bounded model checkingu, po pˇrehrán´ı cesty v JPF se z dosaˇzeného stavu provede bounded model checking. V této podkapitole je popsána nov´ a prohled´ avac´ı strategie, kter´ a slouˇz´ı k vykonán´ı bounded model checkingu, a kterou je moˇzné dále rozˇsiˇrovat o verifikaci dalˇs´ıch vlastnost´ı. I zde je uveden jednoduch´ y pˇr´ıklad pro lepˇs´ı názornost funkˇcnosti bounded model checkingu. Tˇret´ı podkapitola se vˇenuje modifikaci naimplementovan´ ych metod pro u ´ˇcel projektu SHADOWS. Aby bylo moˇzné v´ yˇse popsan´ y mechanizmus vyuˇz´ıt v projektu SHADOWS, je nutné prov´ adˇet nahr´ av´ an´ı bˇehu programu mimo JPF a v JPF provést aˇz samotnou verifikaci. Tato ˇc´ ast implementace nen´ı zcela dokonˇcená z d˚ uvod˚ u r˚ uzn´ ych peripeti´ı, s kter´ ymi bylo potˇreba se pˇri implementaci vypoˇrádat. Problémy a jejich návrh ˇreˇsen´ı jsou uvedeny v dané podkapitole. Z´ aroveˇ n je zde nast´ınˇeno, jak´ ym smˇerem se bude dále pokraˇcovat v dokonˇcen´ı zaˇclenˇen´ı naimplementovan´ ych metod do projektu SHADOWS. Posledn´ı podkapitola obsahuje nˇekteré testy a v´ ysledky, které jsou pouze d´ılˇc´ı. Celkové testován´ı naimplementovan´ ych metod bude moˇzné aˇz po integraci strategi´ı do projektu SHADOWS.

5.1

Record&Replay trace v JPF

Metoda Record&Replay trace je zaloˇzena na záznamu potˇrebn´ ych informac´ı pro opˇetovné pˇrehrán´ı stejného bˇehu programu. Aby bylo moˇzné tuto metodu aplikovat pro ovˇeˇren´ı opravy, bylo nutné nejprve otestován´ı, zda je tento mechanizmus – záznamu cesty a pˇrehrán´ı dané 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ád´ı rozgenerován´ı celého stavového prostoru a bylo tedy nutné nejprve pochopit jeho princip verifikace. Jak jiˇz bylo uvedeno JPF obsahuje ˇradu prohled´ avac´ıch strategi´ı. Pro pochopen´ı principu generován´ı stavového prostoru jsou d˚ uleˇzité n´ asleduj´ıc´ı z´ akladn´ı strategie DF S a BF S. • DF S strategie: 1) Sestrojen´ı zásobn´ıku (stack), kter´ y obsahuje vˇsechny uzly, které se maj´ı expandovat. Na zaˇcátku zásobn´ık obsahuje poˇcáteˇcn´ı stav. 2) Je-li zásobn´ık pr´ azdn´ y, prohled´ av´ an´ı konˇc´ı. Jinak se pokraˇcuje v prohledáván´ı. 3) Ze zásobn´ı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á o stav, kter´ y jiˇz v zásobn´ıku je nebo je jiˇz expandovan´ y, provede se návrat do bodu 2). Implementace DF S metody v JPF (gov.nasa.jpf.search.DFSearch) je navrˇzena takov´ ym zp˚ usobem, aby nedocházelo ke generován´ı vˇsech následn´ık˚ u, ale do zásobn´ıku jsou uloˇzeny pouze vˇsechny expandované stavy a informace o moˇzn´ ych následovn´ıc´ıch pomoc´ı CG (ne cel´ y stav). Dalˇs´ı bezprostˇredn´ı následovn´ıci stavu se generuj´ı aˇz pˇred vykon´ an´ım stavu. Pro oˇsetˇren´ı, aby se negeneroval jeden stav v´ıcekrát, 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é k vykon´ an´ı a druh´ y obsahuje jiˇz expandované stavy. Do prvn´ı fronty se na zaˇc´ atku vloˇz´ı poˇc´ ateˇcn´ı stav. 2) Pokud prvn´ı fronta neobsahuje ˇzádn´ y stav pro rozgenerov´ an´ı prohled´ aván´ı konˇc´ı. Jinak se pokraˇcuje v prohledáván´ı stavového prostoru. 3) Z prvn´ıho seznamu se vybere ˇceln´ı stav a uloˇz´ı se do druhého 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ány bud’ v prvn´ım nebo druhém seznamu). Implementace BF S metody v JPF (gov.nasa.jpf.search.heuristic.BFSearch) je naimplementov´ ana podobn´ ym zp˚ usobem. V metodˇe docház´ı k vygenerován´ı vˇsech bezprostˇredn´ıch n´ asledovn´ık˚ u po expandován´ı stavu (vˇsechny moˇznosti z CG), tyto stavy jsou vytvoˇreny a pˇred jejich vykonán´ım docház´ı pouze k jejich postupnému obnoven´ı. Ve strategii BF S je zaj´ımavou myˇslenkou rozgenerován´ı vˇsech moˇzn´ ych následovn´ık˚ u (t´ım je vidˇet, co kter´ y vykon´ av´ a). Nicménˇe ve strategii BF S se do fronty pro následované obnoven´ı a vykon´ an´ı stavu uloˇz´ı vˇsichni bezprostˇredn´ı následovn´ıci. C´ılem strategie Record&Replay trace je vykonat pouze konkrétn´ı moˇznost a ostatn´ı nerozgenerovávat, resp. vykonat pouze jeden konkrétn´ı bˇeh programu. Toho lze doc´ılit naplánován´ım a uloˇzen´ım do fronty pouze zvolené moˇznosti CG.

5.1.1

Record&Replay pomoc´ı ChoiceGener´ ator˚ u

Aby bylo moˇzné napl´ anovat pouze konkrétn´ı moˇznost CG, je zapotˇreb´ı pochopit ovlád´ 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ázka ˇcásti v´ ypisu z daného listeneru je na obr. 5.1, listener vypisuje moˇznosti CG, kde doˇslo k volbˇe a která moˇznost byla zvolena. V´ ypis je ze vzorového 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é náhodnˇe zvolené 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ého pˇr´ıkladu s listenerem CGMonitor

SaveCurChoice. SaveCurChoice je listener, který zaznamenává potˇrebné informace o zvolené moˇznosti CG do souboru. Pomoc´ı pˇreddefinovaného rozhran´ı VMListener˚ u je detekov´ an zaˇc´ atek nové moˇznosti ChoiceGenerátoru. Po vykonán´ı prvn´ı instrukce do zaˇcátku nové moˇznosti CG (zvolen´ a moˇznost se jiˇz vykonává), se uloˇz´ı informace o jak´ y typ CG se jedná (BooleanChoiceGenerator, ThreadChoiceGenerator, atd.), o kolikátou moˇznost z CG se jedn´ a a jaké je aktu´ aln´ı vl´ akno. Tyto informace jsou postaˇcuj´ıc´ı k opˇetovnému pˇrehr´ an´ı správné moˇznosti CG. Listener umoˇznuje následuj´ıc´ı nastaven´ı (properties): 27

save cur choice.trace – n´ azev v´ ystupn´ıho souboru se záznamem bˇehu, y bude zapsán do v´ ystupn´ıho souboru, save cur choice.comment – znˇen´ı komentáˇre, kter´ vut.logging – (true/false) pro v´ ypis vykonan´ ych moˇznost´ı CG na pˇr´ıkazovou ˇrádku (v´ ypis urˇcen´ y pro testov´ an´ı).

LoadCurChoice Jedná se o listener, který podle vstupn´ıho souboru, který obsahuje CG a jejich zvolené moˇznosti provede naˇcten´ı cesty a pokud je to moˇzné opˇetovné pˇrehr´ an´ı programu koresponuj´ıc´ı s uloˇzenou cestou (uloˇzená cesta CG koresponduje s CG, které jsou voleny ve spuˇstˇené aplikaci). Listener gov.nasa.jpf.tools.ChoiceSelector je základem uvedeného nového listeneru. Bˇehem registrace listeneru pˇri spuˇstˇen´ı JPF se naˇcte cesta ze souboru. Pokud se pˇri vykonáván´ı programu naraz´ı na vytváˇren´ı nového CG, provede se kontrola s naˇctenou cestou, pokud typ aktu´ aln´ıho CG z uloˇzené cesty koresponduje s typem CG z vykonávaného programu napl´ anuje se proveden´ı pouze uloˇzené moˇznosti. Listener umoˇznuje následuj´ı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áván´ı i pokud uloˇzená cesta jiˇz skonˇcila nebo uloˇzená cesta nekoresponduje s vykonávan´ ym programem, load cur choice.randomSeed – zadán´ı ˇrady pro Random, která se pouˇzije pro náhodn´ y v´ ybˇer moˇznosti CG, nekoresponduj´ıc´ıch s uloˇzenou cestou (urˇceno pro testován´ı).

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án´ı cesty vyuˇzity ChoiceGenerátory, 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á v moˇznosti pˇrehrán´ı bˇehu programu pomoc´ı informac´ı, které lze z´ıskat z libovolného“ bˇehu programu. ” C´ılem je pˇrehr´ at bˇeh programu napsaného v Javˇe, zdrojov´ y kód se nejprve pˇreloˇz´ı do spustitelného mezik´ odu – Java byte-code. Tento kód se posléze spust´ı pomoc´ı JVM (Java Virtual Machine). Jak jiˇz bylo uvedeno, JPF je speciáln´ı virtuáln´ı stroj, kter´ y také prov´ ad´ı bˇeh programu pomoc´ı byte-code instrukc´ı. Pro pˇrehr´ an´ı urˇcitého bˇehu programu je tedy potˇreba zaznamenat poˇrad´ı vykonáv´ an´ı jednotliv´ ych byte-code instrukc´ı a informace o tom, které vlákno dané instrukce vykonáv´ a. Záznam cesty je st´ ale prov´ adˇen pomoc´ı JPF, ale tentokrát se ukládaj´ı ty informace, které lze z´ıskat z programu i bez JPF. Mezi dalˇs´ı informace, které je potˇreba znát pro pˇresné pˇrehrán´ı cesty programu jsou vstupn´ı data, ˇcten´ı/zápis do souboru atd. Tyto informace nebyly prozat´ım br´ any v potaz a z´ aznam/pˇrehrán´ı cesty se provád´ı nad programy, u kter´ ych ˇ ı/zápis do souboru je sloˇzit´ tyto informace nejsou zapotˇreb´ı. Cten´ y problém, JPF nepodporuje knihovny pro ˇcten´ı/z´ apis do souboru. Dalˇs´ı d˚ uleˇzité 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ásah do zdrojového 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áln´ı byte-code instrukce. Mechanizmus pˇrehr´ an´ı programu v JPF spoˇc´ıvá 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é názvy, stejné funkce i stejné parametry.

28

D´ıky faktu prov´ adˇen´ı programu pˇr´ımo v JPF a dobrému rozhran´ı na listenery, je moˇzné pˇripojit listenery témˇ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é odchytávat d˚ uleˇzité informace – vˇsechny vykonané byte-code instrukce, bˇeˇz´ıc´ı vl´ akna atd. Jelikoˇz k záznamu potˇrebn´ ych informac´ı doch´ az´ı stále zat´ım v JPF, je moˇzné 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áznam cesty, která obsahuje vykonané byte-code instrukce je vytvoˇren nov´ y listener cz.vutbr.fit.tools.RecordTrace. Ten se podobá pˇredeˇslé implementaci listeneru (SaveCurChoice). Rozd´ıl je v implementovan´ ych metodách pomoc´ı rozhran´ı VMListener a v zaznamenan´ ych informac´ıch bˇehem bˇehu programu. I tento listener umoˇzn ˇuje nastaven´ı parametr˚ u, které ovlivˇ nuj´ı jeho funkci: vut record trace.CG – (true/false) pro zaznamenáván´ı informace o zvolené moˇznosti CG (urˇceno pro testov´ an´ı), vut record trace.Insn – (true/false) pro zaznamenáván´ı vykonané instrukce byte-codu, vut record trace.Thread – (true/false) pro zaznamenáván´ı informac´ı o aktuáln´ım vláknˇe (jméno, index), vut record trace.FileName – n´ azev v´ ystupn´ıho souboru se zaznamenanou cestou, vut record trace.Info – (true/false) zaznamenáván´ı dalˇs´ıch informac´ı (krok vpˇred, krok vzad, apod.). Z nastaven´ı listeneru plyne moˇznost zaznamenávat r˚ uzné informace podle poˇzadavk˚ u. Aby pˇr´ı naˇc´ıt´ an´ı inforamc´ı zaznamenané cesty bylo patrné, o jakou informaci se jedn´ a, obsahuje kaˇzd´ y typ informace sv˚ uj pˇredem definovan´ y prefix. Pˇr´ıklad ˇcásti souboru se zaznamenanou cestou, kter´ a obsahuje vˇsechny moˇzné 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ázek 5.2: Zaznamenan´ a cesta pomoc´ı listeneru cz.vutbr.fit.tools.RecordTrace Kaˇzd´ y v´ ypis obsahuje na zaˇcátku informace o aplikaci, ke které byl poˇr´ızen – n´ azev aplikace a vstupn´ı parametry, pokud nˇejaké byly. Dále obsahuje informace o CG (prefix [x], kde x je ˇc´ıslo CG), typ CG, jaká moˇznost byla zvolena a ˇc´ıslo vybrané moˇznosti. 29

Nejˇcastˇejˇs´ı poloˇzkou z´ aznamu jsou informace, podstatné pro pˇrehrán´ı cesty. Tyto informace jsou: jméno aktu´ aln´ıho vl´ akna, index aktuáln´ıho vlákna a popis byte-code instrukce (prefix #). Posledn´ım typem informace jsou informace o stavech a prohledáván´ı stavov´ ym prostorem (prefix %). Pomoc´ı listeneru RecordTrace lze tedy provést záznam cesty v JPF. Nicménˇe pokud by byla aplikace spuˇstˇena v JPF pouze s t´ımto listenerem, nedoˇslo by k záznamu jedné cesty, ale JPF automaticky prohled´ av´ a cel´ y stavov´ y prostor. Implicitn´ı prohledávac´ı strategi´ı je DFS. Pokud je tedy c´ılem zaznamenat pouze jeden bˇeh aplikace, je nutné spustit JPF s jinou vyhled´ avac´ı strategi´ı, kter´ a prov´ ad´ı resp. simuluje pouze jeden bˇeh programu. JPF obsahuje dvˇe jednoduché naimplementované strategie RandomSearch a PathSearch. Ty simuluj´ı náhodn´ 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ákladn´ım nastaven´ı a s listenerem SaveCurChoice. Pomoc´ı nˇeho se zaznamenaj´ı vˇsechny moˇzné cesty, jedna z nich se vybere a uloˇz´ı do souboru, kter´ y bude na vstupu druhého listeneru LoadCurChoice. Pˇri spuˇstˇen´ı JPF s listenerem LoadCurChoice se pˇrilinkuje i listener pro záznam relevantn´ıch informac´ı o cestˇe RecordTrace. D´ıky tomu se doc´ıl´ı zaznamen´ an´ı námi zvolené zaj´ımavé cesty a ne pouze náhodné cesty.

ReplayTrace. Pˇrehrán´ı cesty jiˇz nelze implementovat jako listener. Je tˇreba vybrat a provést stavy ve stavovém prostoru, které koresponduj´ı se zaznamenanou cestou. Pro tento mechanizmus je naimplementov´ ana nová prohledávac´ı strategie. Tato prohledávac´ı strategie, jako vˇsechny naimplementované prohledávac´ı strategie v JPF, je zaloˇzena na superclass Search. Nov´ a strategie ReplayTrace má základ v prohledávac´ıch strategi´ıch – DFSearch a BFSearch. Princip ReplayTrace spoˇc´ıv´ a v generován´ı vˇsech bezprostˇredn´ıch následovn´ık˚ u aktuáln´ı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ého stavu a t´ım se doc´ıl´ı rozgenerov´ an´ı pouze té ˇcásti stavového prostoru, která koresponduje s uloˇzenou cestou. Prohled´ av´ an´ı stavového prostoru pro urˇcen´ı koresponduj´ıc´ıch následovn´ık˚ u se provád´ı pomoc´ı prohled´ avac´ı strategie BFS. ReplaySearchHeuristic je tedy nová vyhledávac´ı strategie zaloˇzená na principu Search strategi´ı, a jej´ı z´ aklad je pˇrevzat z vyhledávac´ıch strategi´ı DFSearch a BFSHeuristic. Zásadn´ı rozd´ıl spoˇc´ıv´ a v rozgenerováván´ı jednotliv´ ych následovn´ık˚ u a jejich provádˇen´ı. Stejnˇe jako listenery i vyhled´ avac´ı strategie sk´ ytaj´ı moˇznost nastaven´ı parametr˚ u. U této strategie lze nastavit n´ asleduj´ıc´ı: u, které se ukládaj´ı ke genevut.replay search.QueueLimit – maximáln´ı délka fronty stav˚ rován´ı (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án´ı pr˚ ubˇeˇzn´ ych informac´ı bˇehem prohled´ av´ an´ı (urˇceno pro testován´ı), vut.replay search.HeurisiticName – volba prohledávac´ı strategie stavov´ ym prostorem (DFS, BFS). Pˇri zaregistrov´ an´ı vyhled´ avac´ı strategie po spuˇstˇen´ı JPF se nejprve naˇcte zaznamenaná cesta ze vstupn´ıho souboru. Pro naˇc´ıtán´ı cesty byla implementována nová tˇr´ıda cz.vutbr.fit.tools.LoadRecord. LoadRecord slouˇz´ı k naˇcten´ı cesty ze souboru a souˇcasnému rozdˇelen´ı jednotliv´ ych informac´ı. Ty jsou zapsány do struktury Trace ti insn,

30

která m´ a formu seznamu. Trace ti insn umoˇznuje uchovávat pˇr´ıznak o následnosti jednotliv´ ych informac´ı, a také 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á prov´ ad´ı samotné porovn´ an´ı zaznamenané cesty s bˇehem programu. Porovnán´ı bˇehu se prov´ ad´ı po jednotliv´ ych kroc´ıch. Po vygenerován´ı nového stavu se zavolá metoda CheckState(), která porovn´ a aktu´ aln´ı krok programu s aktuáln´ım krokem zaznamenané cesty. Aktuáln´ı krok záznamu, je prvn´ı krok z´ aznamu, kter´ y jeˇstˇe nebyl pˇrehrán provádˇen´ ym programem. Po spuˇstˇen´ı prohled´ av´ an´ı stavového prostoru pomoc´ı strategie ReplaySearchHeuristic se zaˇcne prohled´ avat stavov´ y prostor stejn´ ym zp˚ usobem jako u strategie BF S. Po vykonán´ı poˇc´ ateˇcn´ıho stavu dojde k rozgenerován´ı bezprostˇredn´ıch následovn´ık˚ u. Po vygenerován´ı n´ asledovn´ık˚ u dojde k jejich zaˇrazen´ı do fronty, kde ˇcekaj´ı na vykonán´ı, zároveˇ n dojde k nastaven´ı pˇr´ıznakugenerateChildren. Ten urˇcuje, zda má b´ yt stav vykonán a jeho n´ asledovn´ıci generov´ ani. Pomoc´ı pˇr´ıznaku docház´ı k vykonáván´ı pouze tˇech stav˚ u, které 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átku prohledáván´ı byla zaznamenan´ a cesta pˇred´ ana do tˇr´ıdy CheckStep. Po záznamu cesty je moˇzné se pohybovat po jednotliv´ ych kroc´ıch, aktu´ aln´ım krokem zaznamenané cesty je posledn´ı nevykonan´ y krok v programu. Parametrem metody CheckState() je aktuáln´ı krok provádˇeného programu, ten se porovn´ av´ a s aktu´ aln´ım krokem zaznamenané cesty. Urˇcen´ı koresponduj´ıc´ıch krok˚ u se provád´ı podle shody jednotliv´ ych byte-code instrukc´ı a vlákna, které je vykonává. Porovn´ an´ı byte-code instrukc´ı a identifikace vlákna je jednoduchá, maj´ı stejnou signaturu (záznam i pˇrehr´ an´ı se prov´ ad´ı pomoc´ı JPF). Problém pro porovnán´ı jednotliv´ ych krok˚ u nast´ av´ a u hranice pˇrechodu mezi jednotliv´ ymi stavy. Hranic´ı pˇrechodu b´ yvá typicky instrukce pro naˇcten´ı/uloˇzen´ı promˇenné nebo zmˇenu aktuáln´ıho vlákna. Pokud v m´ıstˇe naˇcten´ı/uloˇzen´ı promˇenné doch´ az´ı k vˇetven´ı (generován´ı nov´ ych stav˚ u). Je tˇreba dávat pozor, zda k vykonán´ı 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é i ve vˇsech rozgenerovan´ ych stavech, vykonán´ı instrukce se opakuje na zaˇcátku nového pˇrechodu. M˚ uˇze nastat i situace, kdy je vykonán´ı instrukce naplánované aˇz na zaˇc´ atku nov´ ych pˇrechod˚ u. V pˇr´ıpadˇe jednoho bˇehu JPF tento problém nevznik´ a, problém nast´ av´ a pˇri porovn´ av´ an´ı pˇrechod˚ u dvou bˇeh˚ u JPF. Je tedy nutné s t´ımto problémem 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é také poˇc´ıtat s faktem, kdy m˚ uˇze skonˇcit zaznamenan´ a cesta a prohledáván´ı stavového prostoru nen´ı ukonˇceno. V takovém pˇr´ıpadˇe lze provést bud’ ukonˇcen´ı prohledáván´ı s koncem zaznamenané cesty nebo d´ ale provádˇ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ád´ı prokládán´ı dvou vláken. Kaˇzdé z vláken v cyklu vypisuje na standardn´ı v´ ystup svoje jméno 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áznam 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áznamu cesty v JPF Pomoc´ı nastaven´ı listeneru bylo zvoleno uloˇzen´ı pouze nejnutnˇejˇs´ıch informac´ı pro pˇrehr´ an´ı cesty programu. Zaznamenané informace jsou jméno aktuáln´ıho vlákna, jeho index a vykonané byte-code instrukce. Uk´ azka ˇcásti záznamu 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é cesty v JPF demonstruje následuj´ıc´ı obr. 5.6. Na obrázku je patrné generov´ an´ı stavového prostoru. Z kaˇzdého stavu doˇslo k vygenerován´ı vˇsech bezprostˇredn´ıch n´ asledovn´ık˚ u. Nicménˇe vykonáván´ı vygenerovaného stavu a jeho následovn´ık˚ u pokraˇcuje pouze t´ım stavem (stavy), které koresponduj´ı se zaznamenan´ ymi kroky cesty. 32

V uvedeném pˇr´ıkladˇe se jedn´ a vˇzdy pouze o jeden koresponduj´ıc´ı následuj´ıc´ı stav. Generován´ı cesty konˇc´ı po dosaˇzen´ı posledn´ıho stavu uloˇzené cesty.

Obr´ azek 5.6: Graf vygenerovaného stavového 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é aplikovat na r˚ uzné prohledávac´ı strategie, napˇr. na ˇcasto jmenované BF S a DF S. Pomoc´ı parametr˚ u strategi´ı je moˇzné zadat poˇzadovanou nejvˇetˇs´ı hloubku prohled´ av´ an´ı k. Standardnˇe se bounded model checking provád´ı z poˇc´ ateˇcn´ıho stavu do zvolené hloubky k, zároveˇ n je moˇzné zadávat dalˇs´ı nastavitelné parametry prohled´ av´ an´ı, a také pˇrid´ an´ı dalˇs´ıch listener˚ u pro verifikaci dalˇs´ıch vlastnost´ı sledovaného systému. Pokud vezmeme form´ aln´ı z´ apis bounded model checkingu z kapitoly 3.5, kde je verifikovan´ y systém pops´ an pomoc´ı Kripkeho struktury, je moˇzné naj´ıt podobnou strukturu systému i v JPF. V JPF se nejprve nevytváˇr´ı model verifikovaného systému, ale verifikace se prov´ ad´ı pˇr´ımo nad re´ aln´ ym systémem. Nicménˇe i zde se dá naj´ıt podobnost v pr˚ uchodu stavov´ ym prostorem s v´ ypoˇcetn´ım stromem Kripkeho struktury. JPF pˇr´ı prohledáván´ı stavového prostoru vytv´ aˇr´ı stavy systému i pˇrechody. Pˇrechod mezi stavy je definován pomoc´ı vykonan´ ych byte-code instrukc´ı. Stav systému je charakterizován aktuáln´ım stavem celého systému (hodnoty promˇenn´ ych, aktuáln´ı vlákno, atd.). Vlastnosti, které se maj´ı u systému verifikovat jsou form´ alnˇe zapsané pomoc´ı temporáln´ıch formul´ı. Pˇri verifikace pomoc´ı JPF lze nadefinovat verifikované vlastnosti a ovˇeˇrit je pomoc´ı listener˚ u. Ty se daj´ı pˇripojit na ve33

rifikovan´ y systém do poˇzadovaného m´ısta a s generován´ım stavového prostoru kontroluj´ı poˇzadované vlastnosti. JPF umoˇzn ˇuje z´ıskat informaci, zda omezená cesta obsahuje smyˇcku (k-loop) pro verifikaci nekoneˇcn´ ych vlastnost´ı. V JPF nedocház´ı k opˇetovnému vytváˇren´ı shodného stavu. Pokud byl jednou stav vygenerov´ an, nedocház´ı k jeho opˇetovnému generován´ı v jiném m´ıstˇe stavového prostoru, ale pouze se vyuˇziji jiˇz existuj´ıc´ı stav. Proto je snadné zjistit, zda na generované cestˇe existuje zpˇetn´ a smyˇcka. JPF implicitnˇe umoˇzn ˇuje provádˇet bounded model checking z poˇcáteˇcn´ıho stavu. C´ılem práce je ovˇsem provést bounded model checking z pˇredem urˇceného stavu a ne pouze ze stavu poˇc´ ateˇcn´ıho. K tomu u ´ˇcelu byly vytvoˇreny pˇredcházej´ıc´ı listenery a prohledávac´ı strategie. Prvn´ı moˇznost´ı je vyuˇzit´ı prvn´ıch listener˚ u (LoadCurChoice a SaveCurChoice). Pomoc´ı listeneru SaveCurChoice se zaznamená cesta aˇz do podezˇrelého (chybového) stavu. Záznam cesty tedy konˇc´ı v m´ıstˇe, kde se posléze má zaˇc´ıt provádˇet bounded model checking nebo je moˇzné urˇcit, zda se pˇred zaˇc´ atkem bounded model checkingu má provést pár krok˚ u zpˇet (backtrack()) pro zverifikov´ an´ı celého okol´ı chyby. Druh´ ym krokem je pˇrehrán´ı záznamu cesty pomoc´ı LoadCurChoice, navigace stavov´ ym prostorem konˇc´ı po vygenerován´ı posledn´ıho stavu zaznamenané cesty. Druhou moˇznost´ı je vyuˇzit´ı listeneru pro záznam cesty RecordTrace, jehoˇz záznam cesty také konˇc´ı v podezˇrelém stavu. Potom se JPF spust´ı s novou prohledávac´ı strategi´ı ReplaySearchHeurisicBMC, která vykonává navigaci stavov´ ym prostorem pomoc´ı zaznamenané cesty. Jedn´ a se o modifikaci prohledávac´ı strategie ReplaySearchHeurisic. Rozd´ıl spoˇc´ıv´ a v doimplementov´ an´ı funkce, která 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áteˇcn´ıho stavu bounded model checkingu, k urˇcen´ı hloubky provádˇen´ı generován´ı stavového prostoru, atd. Proto, aby bounded model checking slouˇzil k u ´ˇcelu ovˇeˇren´ı opravy, je tˇreba verifikovat specifické vlastnosti chov´ an´ı systému v okol´ı chyby. K tomuto u ´ˇcelu jsou implementovány dalˇs´ı listenery, které sleduj´ı poˇzadované vlastnosti. Pˇrilinkované listenery k bˇehu programu v JPF sleduj´ı poˇzadovanou vlastnost od zaˇcátku bˇehu aˇz do jeho konce. Tento mechanizmus v pˇr´ıpadˇe bounded model checkingu nen´ı ˇzádouc´ı. Napˇr´ıklad pokud listener slouˇz´ı k sledován´ı pˇr´ıstup˚ u ke sd´ılené promˇenné, nen´ı c´ılem zaznamen´ avat veˇskeré pˇr´ıstupy ke sd´ılené promˇenné, ale pouze pˇr´ıstupy v okol´ı chyby. Je snahou sledovat pouze ty pˇr´ıstupy, které 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é nastavit pomoc´ı vyhled´ avac´ı strategie a jeho pˇr´ıznak pˇredán do pˇrilinkovan´ ych listener˚ u. Implementace tohoto mechanizmu si vyˇzaduje z´ asah do navrˇzeného rozhran´ı mezi vyhledávac´ımi strategiemi a listenery.

ReplayTraceAndBoundedModelChecking. Jak bylo zm´ınˇeno výˇse, modifikac´ı prohled´ avac´ı strategie ReplaySearchHeuristic je moˇzné provádˇet bounded model checking po pr˚ uchodu stavov´ ym prostorem do podezˇrelého stavu. Jedná se o strategii ReplaySearchHeuristicBMC, kter´ a obsahuje rozˇs´ıˇren´ı nastaven´ı parametr˚ u o parametry bounded model checking: u, o které se má strategie vrátit 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é se zaˇc´ıná provádˇet bounded model checking, explicitn´ı urˇcen´ı hloubky na cestˇe, kde se zaˇc´ıná provádˇet bounded model checking, (pokud je hodnota rovna −1, bounded model checking zaˇc´ıná na konci zaznamenané cesty), vut.replay search.bmcMaxDepth – maximáln´ı hloubka provádˇ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ány zm´ınˇené parametry, které ˇr´ıd´ı navigaci stavov´ ym prostorem a n´ asledné vykonán´ı bounded model checkingu. Zadané parametry urˇc´ı, kde skonˇc´ı navigace a zaˇcne verifikace, resp. zp˚ usob´ı generovován´ı a vykonáván´ı vˇsech následn´ık˚ u stav˚ u, které maj´ı b´ yt provedeny. Prohledávac´ı strategie se ˇr´ıd´ı pomoc´ı jiˇz popsan´ ych heuristik, ty jsou také souˇcást´ı nastaven´ı vstupn´ıch parametr˚ u. Prozat´ım jsou implementov´ any pouze dva prohledávac´ı 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á se o vzorov´ y pˇr´ıklad, kter´ y je implementován jako program s v´ıce vlákny. Pouˇz´ıvá se pro demonstraci soubˇeˇzného pˇr´ıstupu ke sd´ılené promˇenné pomoc´ı v´ıce vláken. 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ém m´ıstˇe dojde k chybˇe nebo zda se jedn´ a pouze o false alarm. Data race – je chyba, která vzniká u soubˇeˇzného pˇr´ıstupu dvou vl´ aken ke sd´ılené promˇenné, pˇriˇcemˇz jedno vlákno se snaˇz´ı o zápis do sd´ılené promˇenné. Problém 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á vytv´ aˇr´ı a spouˇst´ı dalˇs´ı vl´ akna. Tato vl´ akna reprezentuj´ı jednotlivé u ´ˇcty – tˇr´ıda Account. Kaˇzdé vlákno m˚ uˇze simulovat r˚ uzné operace nad u ´ˇcty. Kaˇzdá z operac´ı nad u ´ˇcty je ukonˇcena a volán´ım metody Service() z tˇr´ıdy Bank. Zdrojov´ y kód 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ód metody z tˇr´ıdy Bank Na prvn´ı pohled uveden´ y zdrojov´ y kód neobsahuje chybu. Ale problém nastává pˇri zmˇenˇe celkové ˇc´ astky v bance (Bank Total). Programátor se mylnˇe domn´ıvá, ˇze uveden´ a operace se prov´ ad´ı jako atomick´ a. Pˇri pˇrevodu do mezikódu, kter´ y se posléze vykonáv´ a, má tato jednoduch´ a operace (pˇriˇcten´ı) ˇctyˇri Java byte-code instrukce: (1) z´ıskán´ı hodnoty Bank Total, (2) z´ısk´ an´ı hodnoty sum, (3) seˇcten´ı hodnot a (4) uloˇzen´ı nové hodnoty Bank Total. Problém tedy nast´ av´ a pokud zadanou operaci provád´ı dvˇe vlákna najednou. Pokud si obˇe vl´ akna naˇctou hodnotu Bank Total, aktualizuj´ı jej´ı hodnotu a posléze zap´ıˇs´ı novou

35

hodnotu sekvenˇcnˇe. Druh´ y z´ apis do Bank Total pˇrep´ıˇse aktualizovanou hodnotu prvn´ım vláknem, 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ém m´ıstˇe programu m˚ uˇze opravdu doj´ıt k TrueRace“. Uvedené m´ısto programu je povaˇzováno za podezˇrelé. ” Nejprve se provede bˇeh programu s pˇrilinkován´ım listeneru pro záznam cesty. Jedn´ a se o testov´ y pˇr´ıklad, je moˇzné provést nejprve záznam celého bˇehu programu pomoc´ı SaveCurChoice. Ze z´ aznamu listeneru je vidˇet v jaké hloubce a v kterém bˇehu se nach´ az´ı podezˇrel´ y stav, kter´ y m˚ uˇze zp˚ usobit problém. Tato hloubka a cesta je poznamenaná do souboru. D´ ale jsou aplikov´ any listenery LoadCurChoice a RecordTrace, které jsou vyuˇzity pro zaznamen´ an´ı cesty do poˇzadované hloubky. Druh´ ym krokem je proveden´ı pˇrehrán´ı uloˇzené cesty, která vede do podezˇrelého stavu. K proveden´ı je pouˇzita prohled´ avac´ı strategie ReplayTraceHeuristicBMC a dále je pˇrilinkován nov´ y listener Races, kter´ y je navrˇzen pro záznam jednotliv´ ych pˇr´ıstup˚ u k podezˇrelé promˇenné. Promˇenn´ a je identifikována podle svého um´ıstˇen´ı (bal´ıˇcek + tˇr´ıda) a identifikátoru promˇenné. 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é promˇenné v okamˇziku spuˇstˇen´ı bounded model checkingu. Po kaˇzdé provedené instrukci se kontroluje, zda neˇslo o instrukci pˇr´ıstupu ke sledované promˇenné. Pokud doˇslo k pˇr´ıstupu k promˇenné, zaznamenaj´ı se n´ asleduj´ıc´ı informace: hloubka – aktuáln´ı vlákno – aktuáln´ı metoda – stav systému – ˇ 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ázornˇen na obr. 5.9. Obr´ azek zn´ azorˇ nuje pouze ˇcást celého grafu, kter´ y reprezentuje generovan´ y stavov´ y prostor. Nejprve doˇslo k navigaci stavov´ ym prostorem do podezˇrelého stavu. Z podezˇrelého stavu se rozgenerov´ av´ a stavov´ y prostor a zároveˇ n se pomoc´ı listeneru ukládaj´ı informace o pˇr´ıstupu ke sd´ılené promˇenné. Nakonec byly ruˇcnˇe vyhodnoceny zaznamenane informace pomoc´ı listeneru. Na grafu je ˇcervenˇe uveden podezˇrel´ y stav, ze kterého byl ˇ zahájen 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ást celého grafu, kter´ y reprezentuje generovan´ y stavov´ y prostor. Nejprve doˇslo k navigaci stavov´ ym prostorem do podezˇrelého 36

stavu. Z podezˇrelého stavu se rozgenerovává stavov´ y prostor a zároveˇ n se pomoc´ı listeneru ukládaj´ı informace o pˇr´ıstupu ke sd´ılené promˇenné. Nakonec byly ruˇcnˇe vyhodnoceny zaznamenané informace pomoc´ı listeneru. V grafu je oznaˇcen podezˇrel´ y stav, ze kterého byl ˇ zahájen 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á u ´pravou strategie Record&Replay trace pro vyuˇzit´ı v projektu SHADOWS. Nahr´ av´ an´ı cesty programu se jiˇz neprovád´ı pomoc´ı JPF, ale mimo model checker. Pro z´ aznam cesty se vyuˇz´ıvá nástroj ConTest, kter´ y byl jiˇz zm´ınˇen na zaˇc´ ata se o nástroj, pomoc´ı kterého se detekuj´ı a posléze léˇc´ı nalezené ku práce v kapitole 2. Jedn´ chyby v programu. IBM ConTest je testovac´ı nástroj, kter´ y provád´ı instrumentaci Java byte-codu programu. ConTest obsahuje také listenerovou architekturu a umoˇzn ˇuje zanesen´ı ˇsumu do programu pro lepˇs´ı odhalov´ an´ı chyb vznikl´ ych soubˇeˇznost´ı. Instrumentace kódu spoˇc´ıv´ a ve vkládán´ı byte-code instrukc´ı do byte-codu monitorovaného programu. Pomoc´ı tˇechto vloˇzen´ ych instrukc´ı je moˇzné pˇrilinkovávat listenery do bˇehu programu, zanáˇset do programu ˇsum a dalˇs´ı. Na architektuˇre listener˚ u je zaloˇzen i mechanizmus pro detekci a následnou opravu chyb v programu. Pomoc´ı tˇechto listener˚ u je moˇzné z´ıskat r˚ uzné informace o vykonáván´ı programu pˇr´ımo za bˇehu. Instrumentovan´ y k´ od programu se spouˇst´ı v bˇeˇzném Java virtuáln´ım stroji. Pomoc´ı instrumentace a parametr˚ u se za bˇehu programu pˇrilinkovávaj´ı poˇzadované listenery ConTestu, které vykon´ avaj´ı zadané události. ConTest tedy m˚ uˇze stejn´ ym zp˚ usobem jako JPF pomoc´ı listener˚ u sledovat urˇcité vlastnosti nebo ˇcásteˇcnˇe modifikovat provádˇen´ı programu za bˇehu.

37

Zámˇerem je zaznamen´ avat cestu programu pˇri jeho provádˇen´ı s pˇrilinkovan´ ym ConTestem. Po aplikaci opravy ConTestem provést v okol´ı opravy bounded model checking v JPF a ovˇeˇrit korektnost opravy. C´ılem tedy je pˇrehrát zaznamenanou cestu ConTestem v JPF. ast zaznamenané cesty z ConTestu. Záznam cesty se provád´ı poNa obr. 5.10 je uvedena ˇc´ moc´ı speci´ aln´ıho listeneru, kter´ y byl pro tento u ´ˇcel navrˇzen. Listener zaznamenává vˇsechny moˇzné informace, které lze z ConTestu o bˇehu programu z´ıskat. Záznam cesty a implementace zm´ınˇeného listeneru nen´ı souˇcásti diplomové práce, 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áznam cesty obsahuje informace o aktuáln´ım vláknˇe (jméno, tˇr´ıda, index), dalˇs´ı informac´ı je ud´ alost ConTestu (bude dále rozepsané), informace o zdrojovém kódu (um´ıstˇen´ı a jméno zdrojového souboru, aktu´ aln´ı metoda), posledn´ı informac´ı je rozsah události ConTest a poˇrad´ı byte-code instrukce na ˇrádku, kterou daná událost ConTestu zaˇc´ıná. Z hlediska pˇrehr´ an´ı cesty je pro nás d˚ uleˇzité zaznamenávat m´ısta nedeterminismu, kter´ a urˇcuj´ı smˇer dalˇs´ıho prov´ adˇen´ı programu. Nástroj ConTest program rozdˇeluje na tzv. BasicBlocky. BasicBlock tvoˇr´ı ˇc´ ast programu, ve které nedocház´ı k nedeterminismu. Na uveˇ ısla na konci deném z´ aznamu cesty programu je vidˇet nˇekolik BasicBlock˚ u s r˚ uznou délkou. C´ kaˇzdého ˇr´ adku z´ aznamu odpov´ıdaj´ı ˇc´ısl˚ um ˇrádk˚ u ve zdrojovém kódu programu odkud – kam sah´ a BasicBlock. Posledn´ım ˇc´ıslem záznamu cesty je poˇradové ˇc´ıslo prvn´ı instrukce BasicBlock na zdrojovém ˇr´ adku kódu. Dalˇs´ı zaznamenanou ud´ alost´ı ConTestu je zaˇcátek vlákna Thread Begin nebo ukonˇcen´ı vlákna Thread End. Tyto ud´ alosti jsou také vznikem nedeterminismu a jsou tedy potˇrebné v záznamu cesty. V z´ aznamu cesty je patrn´ y rozd´ıl mezi informacemi z´ıskan´ ymi z JPF a informacemi, které 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é stavy a pˇrechody v systému, ty jsou ovˇsem odliˇsné 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át 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ávaznosti mezi uloˇzen´ ymi informacemi a informacemi za bˇehu programu je moˇzné aplikovat strategii pro navigaci stavov´ ym prostorem a následn´ 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é informace se zaznamenanou cestou ConTestem. Tyto informace slouˇz´ı k navigaci stavov´ ym prostorem. Druhou moˇznost´ı je pˇrehr´ an´ı instrumentovaného kódu v JPF. Instrumentace ConTestem sice pˇrid´ av´ a do byte-codu programu dalˇs´ı instrukce, ale bˇeh programu se provád´ı pomoc´ı 38

standardn´ıho virtu´ aln´ıho stroje. JPF je speciáln´ım virtuáln´ım strojem a je tedy teoreticky moˇzné pˇrehr´ an´ı instrumentovaného kód.

5.3.1

Replay trace pomoc´ı p˚ uvodn´ım k´ odu

Pˇri prozkoum´ av´ an´ı prvn´ı moˇznosti byl postup následuj´ıc´ı. Postupnˇe se specifikovaly informace z´ıskané 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é se mˇen´ı parametry a informace, které 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é byte-code instrukce identifikuj´ı pomoc´ı ˇc´ısla ˇrádku ve zdrojovém k´ odu (tato informace je v JPF obsaˇzena) a pomoc´ı poˇrad´ı instrukce na ˇrádku, tuto informaci se nepodaˇrilo z´ıskat. Z d˚ uvod˚ u pˇrepsán´ı p˚ uvodn´ıch byte-code instrukc´ı na odpov´ıdaj´ıc´ı JPF instrukce se ztrác´ı nˇekteré informace obsaˇzené v p˚ uvodn´ım mezikódu. Pro z´ısk´ an´ı poˇrad´ı instrukce na ˇrádku v p˚ uvodn´ım kódu by byl nutn´ y hlubˇs´ı zásah do fungov´ an´ı JPF. Poˇzadovaná informace by se musela z´ıskat v pr˚ ubˇehu tranformace p˚ uvodn´ıch instrukc´ı na instrukce JPF. Transformace p˚ uvodn´ıho kódu na instrukce JPF má nˇekolik f´ az´ı. Nejprve dojde k rozdˇelen´ı kódu na d´ılˇc´ı ˇcásti jako jsou metody, v dalˇs´ı fázi se postupnˇe proch´ az´ı jednotlivé 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é kaˇzdá byte-code instrukce potˇrebuje pro spr´ avnou funkci. V této fázi docház´ı k zásadn´ı zmˇenˇe. Nelze jiˇz zpˇetnˇe z´ıskat p˚ uvodn´ı informace instrukce. Pro uchov´ an´ı informace, kolikátou insturkc´ı na ˇrádku daná instrukce je, by bylo tˇreba zasáhnout do superclass vˇsech JPF instrukc´ı a pˇridat nov´ y parametr. Nastaven´ı tohoto parametru by bylo tˇreba pˇridat do správn´ ych“ konstruktor˚ u JPF instrukc´ı. Dále by bylo ” nutné zas´ ahnout do jendnotliv´ ych ˇcást´ı tranformace p˚ uvodn´ıho kódu na instrukce JPF a na vˇsechna potˇrebn´ a m´ısta zadat nejprve z´ıskán´ı poˇzadovaného parametru a pak jeho pˇredán´ı do nové instrukce JPF. Tento mechanizmus je nároˇcn´ y a zp˚ usobil by rozsáhlé zmˇeny v JPF. Vzhledem k tomu ,ˇze byte-code instrukce jsou jednou z hlavn´ıch informac´ı, která je potˇrebn´ a pro opˇetovné pˇrehr´ an´ı bˇehu programu, byla snaha tento mechanizmus naimplementovat tak, aby byly z´ısk´ any potˇrebné informace bez velkého zásahu do JPF. Nicménˇe po delˇs´ı dobˇe testov´ an´ı bylo od této moˇznosti upuˇstˇeno a nebyla naimplementována.

5.3.2

Replay trace pomoc´ı instrumentovan´ eho k´ odu

Druhou moˇznost´ı je pˇrehr´ an´ı instrumentovaného kódu pˇr´ımo v JPF. C´ılem je pˇrehr´ at p˚ uvodn´ı Java byte-code bez instrumentace. Je nutné se nˇejak´ ym zp˚ usobem s pˇridan´ ymi instrukcemi ConTestu vypoˇr´ adat. Ponechán´ı instrukc´ı kódu pˇri verifikaci nen´ı moˇzné. Pomoc´ı pˇridan´ ych instrukc´ı ConTestu se volaj´ı r˚ uzné moduly ConTestu, které nen´ı moˇzné pomoc´ı JPF zverifikovat. Vyˇrazen´ı tˇechto modul˚ u z verifikace pomoc´ı standardn´ıho mechanizmu JPF si vyˇzaduje z´ asah do zdrojového kódu a zmˇenu metod tˇechto modul˚ u na nativn´ı metody. Nativn´ı metody jiˇz nepodléhaj´ı verifikaci. Nástroj ConTest ovˇsem nen´ı moˇzné 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ánované instrukce je podobn´ y jako u listeneru LoadCurChoice, kde se z naplánovan´ ych moˇznost´ı CG provedla pouze jedna moˇznost a ostatn´ı se pˇreskoˇcily. 39

Principem nového listeneru je pˇreskakován´ı vˇsech instrukc´ı ConTestu, které byly do bytecodu pˇrid´ any a z´ aroveˇ n pˇreskakován´ı vˇsech souvisej´ıc´ıch instrukc´ı (parametr˚ u, návratov´ ych hodnot, atd.). Instrumentace ConTestem pˇridává do kódu instrukce pro volán´ı statick´ ych metod ConTestu. Statické metody jsou vol´ any pomoc´ı instrukce invokestatic. Vˇsechny metody ConTestu jsou tedy vol´ any pomoc´ı instrukce invokestatic, nicménˇe kaˇzdá metoda má jin´ y poˇcet parametr˚ u a jiné typy parametr˚ u a návratové hodnoty. Je tedy nutné oˇsetˇrit jakékoliv volán´ı metody ConTestu a pˇreskoˇcit správn´ 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á metoda ConTestu se vol´ a a odkud. D´ıky tomu lze pˇresnˇe urˇcit, které instrukce byly pˇridány ConTestem. Z´ aroveˇ n tato instrukce obsahuje informaci pˇred kterou p˚ uvodn´ı instrukci byla pˇridána a také informaci o p˚ uvodn´ı instrukci (na jakém ˇrádku kódu se nacház´ı a kolikátou instrukc´ı ˇrádku je). C´ılem je dané instrukce bˇehem provádˇen´ı programu v JPF pouze pˇreskakovat a ne je zcela vymazat. Nov´ y listener SkipConTestInstruction je zaloˇzen na prohledáván´ı naplánovan´ 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áván´ı naplánovan´ ych instrukc´ı. ConTest vˇzdy pˇrid´ av´ a instrukci pro volán´ı statické metody, nicménˇe kaˇzdá metoda m˚ uˇze m´ıt jin´ y poˇcet parametr˚ u, a proto je potˇreba urˇcit, jaká metoda má b´ yt volána. V listeneru SkipConTestInstruction docház´ı pouze k detekci, zda se jedná o instrukci pˇridanou ConTestem. Urˇcen´ı poˇctu parametr˚ u volané metody a tedy poˇctu pˇreskakovan´ ych instrukc´ı doch´ az´ı ve tˇr´ıdˇe Skipping. Jednotlivé typy metod, které 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ásleduj´ıc´ı problém. Bˇehem instrumentace zdrojového kódu programu nedocház´ı pouze k pˇridán´ı dalˇs´ıch instrukc´ı ConTestu, ale také ke zmˇenˇe urˇcit´ ych byte-code instrukc´ı. Zmˇena se t´ yká instrukc´ı pro vlákna (start, stop, yield, join, atd.). ConTest p˚ uvodn´ı instrukce, které pracuj´ı s vlákny, nahradil vol´ an´ım vlastn´ıch metod, které maj´ı dané vlákno jako parametr. K proveden´ı p˚ uvodn´ı instrukce dojde bˇehem vykonán´ı metody ConTestu. Pokud jsou tyto metody v JPF pˇreskakov´ any, p˚ uvodn´ı instrukce se neprovedou a nastává problém. Je tedy tˇreba implementovat mechanizmus, pomoc´ı kterého se doc´ıl´ı proveden´ı, resp. obnoven´ı p˚ uvodn´ıch instrukc´ı, které byly bˇehem instrumentace kódu odstranˇeny a správnˇe je zpˇet zaˇclenit do k´ odu. Z principu fungován´ı JPF se nab´ızej´ı dvˇe moˇznosti, jak vytvoˇrit poˇzadovanou instrukci: • Byte-code instrukce JPF. Princip spoˇc´ıvá v pˇretransformován´ı instrukce ConTestu na p˚ uvodn´ı instrukci zdrojového kódu nebo vytvoˇren´ı nové 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áˇren´ı vlastn´ıch instrukc´ı z p˚ uvodn´ıch instrukc´ı. Pro transformaci instrukce ConTestu na jinou instrukci JPF je potˇreba znát informace, které 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ám 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ásah do JPF. Z toho d˚ uvodu nen´ı tato moˇznost pro ˇreˇsen´ı problému vyuˇzita. • Standardn´ı byte-code instrukce. Druhou moˇznost´ı je vytvoˇren´ı nové 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éze 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é informace pro vytvoˇren´ı nové byte-code instrukce. Druh´ a z uveden´ ych moˇznost´ı byla hloubˇeji prostudována. Pro vytvoˇren´ı nové funguj´ıc´ı instrukce je tˇreba pˇredat spr´ avné odkazy do ConstantPool tabulky, zadat správnˇe parametry a v neposledn´ı ˇradˇe spr´ avnˇe zaˇclenit mezi ostatn´ı instrukce. Tato ˇc´ ast implementace – vytvoˇren´ı nové instrukce, nen´ı zcela funkˇcn´ı. Metoda pro vytváˇren´ı nové instrukce je v rozpracované fázi. Listener SkipConTestInstruction se také nacház´ı v rozpracované fázi. Listener je v tuto chv´ıli schopn´ y pˇreskoˇcit vykonáván´ı vˇsech instrukc´ı ConTestu i s jeho parametry, které jsou do k´ odu pˇrid´ any nav´ıc. Avˇsak stále neumoˇzn ˇuje nahrazen´ı instrukc´ı ConTestu pro pr´ aci s vl´ akny za p˚ uvodn´ı instrukce. Je tedy moˇzné v JPF pˇrehrát 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ávác´ıch strategi´ı byla testována bˇehem jejich n´ avrhu a po jejich dokonˇcen´ı. Kaˇzdá z v´ yˇse uveden´ ych ˇcást´ı implementace si vyˇzadovala jin´ y v´ ybˇer testov´ ych program˚ u. Testové programy byly vyb´ırány podle poˇzadavk˚ u, které maj´ı jednotliv´ı listenery a strategie splˇ novat. Nˇekteré z testov´ ych pˇr´ıklad˚ u jsou souˇc´ ast´ı pˇriloˇzeného DVD media. Pro zhodnocen´ı dosaˇzen´ ych v´ ysledk˚ u byly vytvoˇreny r˚ uzné bˇehy vybran´ ych program˚ u. Jednotlivé bˇehy se vykon´ av´ aly v uveden´ ych nástroj´ıch: bˇeˇzn´ y Java virtuáln´ı stroj (JVM), Java PathFinder (JPF) a ConTest. Z´ıskané informace z jednotliv´ ych bˇeh˚ u program˚ u jsou posléze porovn´ any. Vyhodnocen´ı bˇeh˚ u program˚ u slouˇz´ı k urˇcen´ı ˇcasové nároˇcnosti ovˇeˇren´ı opravy chyby v programu. V kaˇzdém z uveden´ ych nástroj˚ u trvá bˇeh programu r˚ uznou dobu a z hlediska verifikace, která je typicky nároˇcná na ˇcás, je porovnán´ı tˇechto bˇeh˚ u zaj´ımavé. Jednotlivé testy, které zde budou uvedeny je moˇzné opˇetovnˇe spustit, jsou souˇcást´ı pˇriloˇzeného DVD. Pouze n´ astroj ConTest nen´ı volnˇe ˇs´ıˇriteln´ y a pˇriloˇzené DVD tedy obsahuje pouze v´ ysledky tˇechto test˚ u. Informace o ConTestu je moˇzné 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é souˇca´sti pˇriloˇzeného DVD. Pˇr´ıklad je zaloˇzen na vzájemném proklád´ an´ı jednotliv´ ych vl´ aken, které simuluj´ı jednotlivé u ´ˇcty v bance (Account). D´ıky vzájemnému prokl´ ad´ an´ı a pˇr´ıstupu do sd´ılené promˇenné je moˇzné pomoc´ı tohoto pˇr´ıkladu pozorovat vliv nedeterminismu na rychlost provádˇen´ı programu. Aplikace je vhodn´ ym pˇr´ıkladem programu s nutnost´ı pl´ anován´ı prokládán´ı jednotliv´ ych instrukc´ı r˚ uzn´ ych vláken. Pro testové u ´ˇcely bylo v programu vytvoˇreno deset vláken simuluj´ıc´ıch jednotlivé u ´ˇcty. D´ıky nez´ avislosti vykon´ av´ an´ı jednotliv´ ych vláken na sobˇe vzniká velké mnoˇzstv´ı moˇzn´ ych proklád´ an´ı instrukc´ı jednotliv´ ych vláken. Druh´ ym pˇr´ıkladem je velice jednoduch´ y program SkipInstruction. Jedná se o u ´mˇele vytvoˇren´ y program pro testovn´ an´ı funkˇcnosti listeneru a pro pˇreskakován´ı 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é mohou b´ yt ConTestem do programu pˇridány. ConTest vkl´ ad´ a instrukce pˇri vytváˇren´ı/zmˇenˇe promˇenn´ ych v programu, pˇri vol´ an´ı metod v programu a samozˇrejmˇe u volán´ı metod vláken (start(),stop(),join(), atd.). Program tedy obsahuje r˚ uzné typy promˇenn´ ych jako integer, double, tyto promˇenné mohou b´ yt statické nebo nestatické (instance promˇenn´ ych). Stejnˇe taky i volán´ı metod m˚ uˇze nab´ yvat r˚ uzn´ ych typ˚ u (statické, ...) a jednotlivé metody mohou m´ıt r˚ uzné typy parametr˚ u. umˇerné V´ ysledky test˚ u, které jsou uvedené v tabulkách 5.1 a 5.2 byly z´ıskány jako pr˚ hodnoty ˇcas˚ u bˇehu program˚ u. Kaˇzd´ y typ bˇehu byl spuˇstˇen tis´ıckrát 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ém Java virtuáln´ım stroji (JVM). Pr˚ umˇern´ a délka bˇehu v JVM je brána jako refernˇcn´ı. Následnˇe byly programy spuˇstˇeny v model checkeru Java PathFinder (JPF), kter´ y byl nastaven pro vykonán´ı jednoho n´ ahodného bˇehu programu. Pak byla vytvoˇrena instrumentace kódu programu pomoc´ı nástroje ConTest a program opˇet spuˇstˇen v JVM s instrumentac´ı. Posledn´ım testem bˇehu bylo pˇrehr´ an´ı instrumentovaného kódu v JPF. Tento test byl spuˇstˇen pouze pro pˇr´ıklad SkipInstruction, kter´ y obsahuje pouze ty instrumentované instrukce, které je moˇzné v této fázi implementace pˇreskakovat. Pr˚ umˇerné 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ástroj´ı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ástroj´ıch je vidˇet, ˇze JPF nen´ı navrˇzen´ y pro jednoduch´ y bˇeh programu. Pˇri simulován´ı bˇehu programu v JPF docház´ı ke znaˇcnému zpomalen´ı celé aplikace. Oproti tomu bˇeh programu, kter´ y byl instrumentován pomoc´ı ConTestu nen´ı tolik zpomalen. Je ovˇsem nutné brát v potaz fakt, ˇze pˇri testovém bˇehu nebylo instrumentace vyuˇzito (ConTest nepˇridal k bˇehu programu ˇzádny listener ani nezasahoval do bˇehu aplikace). Posledn´ım z uveden´ ych ˇcas˚ u je pˇrehrán´ı instrumentovaného kódu v JPF. Z dosaˇzen´ ych ˇcas˚ u je vidˇet, ˇze pˇri pˇrehráván´ı programu v JPF s instrumentac´ı jiˇz k velkému zpoˇzdˇen´ı nedoch´ az´ı. To je v´ yhodn´ ym faktem pro dalˇs´ı v´ yvoj. Je moˇzné verifikovat p˚ uvodn´ı zdrojov´ y k´ od programu nebo instrumentovan´ y kód za stejnou cenu. Z uvedené tabulky také vypl´ yvá závˇer, ˇze doba provádˇen´ı bˇehu programu v JPF znaˇcnˇe záleˇz´ı na struktuˇre programu a na typu nedeterminismu. Pokud program obsahuje velké mnoˇzstv´ı nedeterminismu a prokládán´ı instrukc´ı, které je potˇreba ˇreˇsit, docház´ı ke znaˇcnému

42

zpomalen´ı bˇehu programu. U prvn´ıho pˇr´ıkladu Bank Account, kter´ y obsahuje velké mnoˇzstv´ı moˇzného prokl´ ad´ an´ı, doch´ az´ı k menˇs´ımu zpomalen´ı aplikace, z d˚ uvodu velkého poˇctu nezávisl´ ych instrukc´ı.

5.4.2

Rychlost metody Record&Replay trace

Dalˇs´ı testov´ an´ı bylo zamˇeˇreno na zjiˇstˇen´ı rychlosti zaznamenáván´ı a pˇrehrán´ı cesty programu v JPF nebo ConTestu. Testy byly opˇet prov´ adˇeny nad stejn´ ymi programy jako pˇredchoz´ı. Referenˇcn´ı rychlost provádˇen´ı z˚ ust´ av´ a stejn´ a – jednoduch´ y bˇeh programu v JVM. Pro testován´ı strategie Record&Replay trace byly pouˇzity naipmlementované 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ádˇen´ı programu zaznamenává volby ChoiceGenerátor˚ u. Druhé testy (Record v JPF I) byly spuˇstˇeny v JPF s listenerem LoadCurChoice a RecordTrace. Pomoc´ı tˇechto test˚ u tedy docházelo zároveˇ n k pˇrehráván´ı bˇehu aplikace pomoc´ı ChoiceGener´ ator˚ u a z´ aroveˇ n k záznamu cesty s byte-code instrukcemi. Tˇret´ı testy (Record v JPF II) byly spuˇstˇeny v JPF pouze s listenerm RecordTrace, nedocházelo tedy k navigaci stavov´ ym prostorem pomoc´ı cesty, ale k náhodnému bˇehu pomoc´ı implementované strategie RandomSearch. Ve ˇctvrt´ ych testech (Record v ConTestu) byla cesta nahrávána 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án´ım chybového bˇehu programu. U druhého programu SkipInstruction nedoch´ az´ı k chybovému bˇehu programu, a proto nebylo druhé testov´ an´ı pˇrehráv´ an´ı cesty zapotˇreb´ı. Namˇeˇrené ˇ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é pomˇery ˇcas˚ u zvolen´ ych program˚ u. Rozd´ıl v ˇcase pro simulován´ı pˇrehr´ av´ an´ı programu v JPF z˚ ustává i u implementované strategie Record&Replay trace. Z tabulky je patrné dalˇs´ı zpomalen´ı, které nastává v d˚ usledku nahráván´ı bˇehu programu. Velikost zpomalen´ı nahr´ aván´ı v JPF je zhruba dvojnásobné oproti náhodnému bˇehu v JPF. Oproti tomu pomˇer pˇrehr´ aván´ı cesty oproti zaznamenáván´ı cesty je u r˚ uzn´ ych program˚ u odliˇsn´ y. Tento fakt vypl´ yvá z principu strategie pˇrehráván´ı cesty. Pˇri pˇrehráv´ an´ı cesty je tˇreba zkontrolovat, které kroky programu koresponduj´ı s uloˇzenou cestou. Pokud program obsahuje velké mnoˇzstv´ı nedeterminismu a velké 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ává vˇsechny vykonané instrukce byte-codu, ale pouze m´ısta vˇetven´ı, je rychlejˇs´ı. Je také c´ılem zaznamenat bˇeh programu mimo JPF a v JPF provést pouze pˇrehrán´ı cesty.

44

Kapitola 6

Z´ avˇ er C´ılem diplomové pr´ ace bylo navrhnout a posléze implementovat metodu pro ovˇeˇren´ı opravy v projektu SHADOWS. Oprava chyb v uvedné ˇcásti projektu SHADOWS se specializuje na chyby v Java programech. Konkrétnˇe se jedná o chyby, které vznikaj´ı v d˚ usledku parelelismu. Pro kontrolu opravy chyby byla zvolena modifikace formáln´ı metody model checkingu. Nejprve bylo nutné nastudovat model checking, jaké má vlastnosti a principy. Po prostudov´ an´ı model checkingu bylo moˇzné navrhnout metodu zaloˇzenou na modifikaci model checkingu takov´ ym zp˚ usobem, aby splˇ novala zadané poˇzadavky pro ovˇeˇren´ı opravy. Navrˇzen´ a metoda pro ovˇeˇren´ı opravy je zaloˇzena na vykonáván´ı bounded model checkingu v okol´ı opravy. Bounded model checking vznikl omezen´ım provádˇen´ı verifikace pomoc´ı model checkingu do zadané hloubky stavového prostoru. Tato modifikace model checkingu lze pro ovˇeˇrov´ an´ı opravy chyby vyuˇz´ıt. Oprava se vˇenuje chybám vznikl´ ym soubˇeˇznost´ı, které jsou zaloˇzeny na zp˚ usobu prokládán´ı jednotliv´ ych instrukc´ı. T´ım tedy dojde ˇcasem k vykon´ an´ı vˇsech relevantn´ıch instrukc´ı, které mohou m´ıt vliv na opravu. K vykonán´ı tˇechto relevatn´ıch instrukc´ı vˇetˇsinou docház´ı v pˇrijatelném ˇcase a je tedy moˇzné pouˇz´ıt bounded model checking. Nicménˇe z´ asadn´ım problémem pro vyuˇzit´ı bounded model checkingu v okol´ı chyby je navigace stavov´ ym prostorem do poˇzadovaného stavu systému. Pro navigaci stavov´ ym systémem existuj´ı r˚ uzné strategie, které byly studovány 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ásledné pˇrehr´ an´ı tohoto bˇehu ve zvoleném model checkeru. Uloˇzená cesta tedy slouˇz´ı k navigaci stavov´ ym prostorem do poˇzadovaného stavu, ze kterého je vykonán bounded model checking pro zverifikov´ an´ı poˇzadovan´ ych vlastnost´ı. Diplomov´ a pr´ ace obsahuje jednotlivé ˇcásti 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ásti, na implementaci mechanizmu pro z´ aznam cesty a na strategii pro pˇrehrán´ı zaznamenané cesty. Pro implementaci mechanizmu pro z´ aznam cesty bylo hlavn´ım bodem urˇcen´ı jaké informace je tˇreba zaznamen´ av´ at, aby bylo moˇzné zaznamenanou cestu pozdˇeji pˇrehrát. Potom byly postupnˇe navrˇzeny a implementovány listenery model checkeru, které slouˇz´ı pro záznam cesty, kter´ a obsahuje informace podle pouˇzitého listeneru. Po naimplementován´ı mechanizmu pro z´ aznam cesty bylo moˇzné pˇristoupit k implementaci strategie pro pˇrehrán´ı cesty. Pˇrehrán´ı cesty bylo u ´spˇeˇsné u cesty zaznamenané pomoc´ı listener˚ u Java PathFinderu. Zat´ım nen´ı hotové pˇrehr´ av´ an´ı cesty, která byla zaznamenána pomoc´ı nástroje ConTest. Ten v pro-

45

jektu SHADOWS slouˇz´ı pro opravu chyby. Tato ˇcást implementace pro vytvoˇren´ı strategie pˇrehrávaj´ıc´ı cestu zaznamenanou pomoc´ı ConTestu je v rozpracované fázi. Dalˇs´ı pr´ ace bude vˇenov´ ana dokonˇcen´ı této strategie. Po dokonˇcen´ı implementace strategie pro pˇrehr´ an´ı cesty bude moˇzné celou metodu otestovat na reáln´ ych datech. A provést bounded model checking pro ovˇeˇren´ı opravy. Pro vlastn´ı verifikaci byl zvolen model checker Java PathFinder, kter´ y umoˇznuje r˚ uzné rozˇs´ıˇren´ı. Umoˇznuje tedy nejen verifikaci vlastnost´ı pro které Java PathFinder jiˇz obsahuje moduly, ale také doimplementován´ı dalˇs´ıch modul˚ u pro verifikaci konkrétn´ıch speciáln´ıch vlastnost´ı systému. Implementace tˇechto modul˚ u do Java PathFinderu jiˇz nen´ı obt´ıˇzná. 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

BOUNDED MODEL CHECKING V NÁSTROJI JAVA PATHFINDER

Recommend Documents