´ UCEN ˇ ´I TECHNICKE ´ V BRNE ˇ VYSOKE Fakulta informaˇcn´ıch technologi´ı ´ Ustav inteligentn´ıch syst´em˚ u
Ing. Bohuslav Kˇ rena
´ ˇ METODY ANALYZY OBJEKTOVE ´ ORIENTOVANYCH PETRIHO S´IT´I ANALYSIS METHODS OF OBJECT ORIENTED PETRI NETS ´cena ´ verze Ph.D. Thesis Zkra
Obor:
Informaˇcn´ı technologie
ˇ Skolitel:
ˇ ska, CSc. Prof. RNDr. Milan Ceˇ
Oponenti:
ˇ Prof. Ing. Stefan Hud´ak, DrSc. Doc. Ing. Jaroslav Sklen´aˇr, CSc.
Datum obhajoby: 20. ˇr´ıjen 2004
Kl´ıˇ cov´ a slova objektovˇe orientovan´e Petriho s´ıtˇe, PNtalk, form´aln´ı metody, stavov´e prostory, probl´em stavov´e exploze, paralelizace, architektury se sd´ılenou pamˇet´ı, Java, JOMP
Key Words Object-Oriented Petri Nets, PNtalk, Formal Methods, State Spaces, State Space Explosion Problem, Parallel Approach, Shared Memory Architecture, Java, JOMP
M´ısto uloˇ zen´ı Vˇedeck´e oddˇelen´ı, FIT VUT v Brnˇe, Boˇzetˇechova 2, 612 66 Brno
c Bohuslav Kˇrena 2004.
ISBN 80-214-2797-3 ISSN 1213-4198
Obsah 1 Souˇ casn´ y stav ˇ reˇ sen´ e problematiky 1.1 Moˇznosti odhalov´an´ı chyb v syst´emech . . . . . . . . . . . . . . 1.2 Souvisej´ıc´ı v´yzkum na FIT . . . . . . . . . . . . . . . . . . . . . 1.3 Objektovˇe orientovan´e Petriho s´ıtˇe . . . . . . . . . . . . . . . .
5 5 6 6
2 C´ıl pr´ ace
8
3 Zvolen´ e metody zpracov´ an´ı
8
4 Hlavn´ı v´ ysledky pr´ ace 4.1 Automatick´a typov´a anal´yza OOPNs . . . . . . . . 4.1.1 Symbolick´a simulace . . . . . . . . . . . . . 4.1.2 Statick´a typov´a anal´yza . . . . . . . . . . . 4.1.3 Dynamick´a typov´a anal´yza . . . . . . . . . . 4.2 Paralelizace gener´atoru stavov´ych prostor˚ u OOPNs 4.2.1 Rozdˇelen´ı vyhled´avac´ı tabulky . . . . . . . 4.2.2 Pˇr´ıstup k nezpracovan´ym stav˚ um . . . . . . 4.2.3 Odd´ıl pro znaˇcen´ı m´ıst . . . . . . . . . . . . 4.2.4 Shrnut´ı dosaˇzen´ych v´ysledk˚ u. . . . . . . . .
. . . . . . . . .
9 9 9 10 11 13 14 14 16 16
5 Z´ avˇ er 5.1 Dosaˇzen´e v´ysledky . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Moˇznosti dalˇs´ıho v´yzkumu . . . . . . . . . . . . . . . . . . . . 5.3 Souvisej´ıc´ı publikace . . . . . . . . . . . . . . . . . . . . . . . .
17 17 17 18
Literatura
18
Curriculum Vitae
21
Abstract
22
. . . . . . . . .
. . . . . . . . .
. . . . . . . . .
. . . . . . . . .
. . . . . . . . .
. . . . . . . . .
3
1
Souˇ casn´ y stav ˇ reˇ sen´ e problematiky
Syst´emy zaloˇzen´e na poˇc´ıtaˇc´ıch jsou nyn´ı pouˇz´ıv´any t´emˇeˇr ve vˇsech oblastech lidsk´e ˇcinnosti. Nespr´avn´a funkce tˇechto syst´em˚ u m˚ uˇze m´ıt za n´asledek velk´e finanˇcn´ı ztr´aty a pˇri pouˇzit´ı v kritick´ych aplikac´ıch m˚ uˇze doj´ıt k poˇskozen´ı zdrav´ı, ke ztr´at´am lidsk´ych ˇzivot˚ u nebo k v´aˇzn´emu poˇskozen´ı ˇzivotn´ıho prostˇred´ı. Pˇri v´yvoji poˇc´ıtaˇcov´ych syst´em˚ u je tedy v´ıce neˇz ˇz´adouc´ı, aby tyto syst´emy obsahovaly minimum chyb. Z´asadn´ı pˇrek´aˇzkou pro tvorbu dokonal´ych poˇc´ıtaˇcov´ych syst´em˚ u je jejich sloˇzitost. V praxi se vyuˇz´ıv´a ˇrada metod pro zlepˇsen´ı kvality vyv´ıjen´ych poˇc´ıtaˇcov´ych syst´em˚ u, pˇriˇcemˇz jednotliv´e metody se pouˇz´ıvaj´ı s r˚ uznou u ´spˇeˇsnost´ı v r˚ uzn´ych f´az´ıch v´yvoje syst´em˚ u. Nˇekter´e metody se snaˇz´ı zlepˇsit anal´yzu a n´avrh syst´em˚ u, ˇrada technik se pouˇz´ıv´a pro minimalizaci vzniku chyb pˇri implementaci software a existuje t´eˇz nepˇrebern´e mnoˇzstv´ı metod a technik pro testov´an´ı v´ysledn´eho produktu. Kromˇe toho existuj´ı i metody, kter´e ovlivˇ nuj´ı vˇsechny f´aze v´yvoje syst´emu — jedn´a se napˇr´ıklad o metody pro ˇr´ızen´ı v´yvoje syst´em˚ u, pouˇz´ıv´an´ı CASE n´astroj˚ u ˇci vyuˇzit´ı form´aln´ıch technik. A pr´avˇe form´aln´ım technik´am je tato pr´ace vˇenov´ana.
1.1
Moˇ znosti odhalov´ an´ı chyb v syst´ emech
Zˇrejmˇe nejstarˇs´ı a nejrozˇs´ıˇrenˇejˇs´ı metodou pro odhalov´an´ı chyb v syst´emech je testov´ an´ı, kter´e spoˇc´ıv´a v experimentov´an´ı se samotn´ym syst´emem nebo jeho ˇc´ast´ı. Nev´yhodou testov´an´ı je, ˇze u re´aln´ych syst´em˚ u nelze vyzkouˇset reakce syst´emu na vˇsechny moˇzn´e situace, protoˇze jich je pˇr´ıliˇs mnoho. Dalˇs´ı ˇcasto pouˇz´ıvanou metodou je simulace, kter´a spoˇc´ıv´a v experimentov´an´ı se simulaˇcn´ım modelem syst´emu. Posledn´ı v´yznamnou skupinou metod pro odhalov´an´ı chyb v syst´emech je form´ aln´ı anal´yza a verifikace. Tyto metody maj´ı na rozd´ıl od testov´an´ı a simulace potenci´al pro dokazov´an´ı spr´avnosti syst´em˚ u. Vstupem form´aln´ı anal´yzy a verifikace je model syst´emu, kter´y m˚ uˇze b´yt popsan´y napˇr. pomoc´ı automat˚ u, Petriho s´ıt´ı, procesn´ıch algeber nebo univerz´aln´ıch programovac´ıch jazyk˚ u. Dalˇs´ım vstupem form´aln´ı verifikace je specifikace vlastnosti, kter´a m´a b´yt pro dan´y syst´em ovˇeˇrena. Vlastnosti jsou nejˇcastˇeji vyj´adˇreny pomoc´ı nˇekter´e tempor´aln´ı logiky, pˇriˇcemˇz mezi nejpouˇz´ıvanˇejˇs´ı patˇr´ı Linear-time Temporal Logic (LTL), Computation Tree Logic (CTL) a CTL*, kter´a spojuje vyjadˇrovac´ı moˇznosti LTL a CTL[6]. Podle zp˚ usobu zjiˇst’ov´an´ı, zda model danou vlastnost splˇ nuje, m˚ uˇzeme metody form´aln´ı anal´yzy a verifikace rozdˇelit do tˇr´ı tˇr´ıd — struktur´aln´ı metody, deduktivn´ı metody (theorem proving) a metody zaloˇzen´e na proch´azen´ı stavov´ych prostor˚ u (model checking). Hlavn´ım probl´emem prakticky vˇsech metod form´aln´ı anal´yzy a verifikace je 5
sloˇzitost. U metod zaloˇzen´ych na generov´an´ı a proch´azen´ı stavov´eho prostoru model˚ u, kter´e jsou pˇredmˇetem naˇseho z´ajmu, se sloˇzitost projevuje probl´emem stavov´e exploze — velikost stavov´eho prostoru roste exponenci´alnˇe s velikost´ı modelu [20]. Pro omezen´ı tohoto probl´emu se pouˇz´ıvaj´ı dvˇe z´akladn´ı skupiny technik. Do prvn´ı skupiny ˇrad´ıme metody, kter´e vyuˇz´ıvaj´ı u ´spornˇejˇs´ı reprezentaci stavov´ych prostor˚ u nebo kter´e ˇc´asti stavov´eho prostoru v˚ ubec negeneruj´ı. Metody z druh´e skupiny pro generov´an´ı a proch´azen´ı stavov´ych prostor˚ u zase vyuˇz´ıvaj´ı v´ykonnˇejˇs´ı poˇc´ıtaˇce (s distribuovanou nebo sd´ılenou pamˇet´ı). Metody z obou skupin lze s v´yhodou kombinovat.
1.2
Souvisej´ıc´ı v´ yzkum na FIT
Na Fakultˇe informaˇcn´ıch technologi´ı (FIT) VUT v Brnˇe je v´yzkumu metod pro v´yvoj poˇc´ıtaˇcov´ych syst´em˚ u vˇenov´ana dlouhodob´a pozornost. Z´akladn´ı metody modelov´an´ı a simulace diskr´etn´ıch i spojit´ych syst´em˚ u jsou rozˇsiˇrov´any za u ´ˇcelem modelov´an´ı a simulace sloˇzit´ych, heterogenn´ıch, paraleln´ıch i objektovˇe orientovan´ych syst´em˚ u [18, 7]. Pro modelov´an´ı, simulaci, form´aln´ı anal´yzu a verifikaci paraleln´ıch syst´em˚ u jsou hojnˇe pouˇz´ıv´any Petriho s´ıtˇe [19], kter´e poskytuj´ı grafickou reprezentaci a pˇresn´y matematick´y popis syst´em˚ u. Petriho s´ıt´ım se na FIT vˇenuje v´yzkumn´a skupina Petriho s´ıt´ı, jej´ıˇz dˇr´ıvˇejˇs´ı u ´spˇeˇsn´ y v´yzkum ˇcernob´ıl´ych Petriho s´ıt´ı vyvrcholil n´avrhem a implementac´ı n´astroje PESIM [5]. V posledn´ı dek´adˇe byl v´yzkum zamˇeˇren na vysoko´ urovˇ nov´e Petriho s´ıtˇe, zejm´ena pak na rozˇs´ıˇren´ı Petriho s´ıt´ı o koncepty objektov´e orientace. V´ysledkem v´yzkumu byl n´avrh formalizmu objektovˇe orientovan´ych Petriho s´ıt´ı1 a s n´ım spojen´eho jazyka a n´astroje PNtalk [8, 21, 4]. Na modelov´an´ı a simulaci OOPN model˚ u logicky navazuje jejich form´aln´ı anal´yza a verifikace [17, 22, 3], v jej´ımˇz r´amci jsou zkoum´any metody form´aln´ı anal´yzy a verifikace zejm´ena softwarov´ych syst´em˚ u zaloˇzen´e na generov´an´ı a proch´azen´ı koneˇcn´ych stavov´ych prostor˚ u a novˇe i na speci´aln´ı metody pro verifikaci parametrick´ych a nekoneˇcnˇe stavov´ych syst´em˚ u [2].
1.3
Objektovˇ e orientovan´ e Petriho s´ıtˇ e
Objektovˇe orientovan´e Petriho s´ıtˇe (OOPNs) jsou formalizmem, kter´y je vhodn´y pro modelov´an´ı, prototypov´an´ı a form´aln´ı anal´yzu a verifikaci paraleln´ıch a distribuovan´ych syst´em˚ u. OOPNs spojuj´ı koncepty Petriho s´ıt´ı (modelov´an´ı kauzality, nedeterminizmu a paralelizmu v diskr´etn´ıch syst´emech) 1
Objektovˇe orientovan´e Petriho s´ıtˇe budeme v dalˇs´ım textu oznaˇcovat zaˇzitou zkratkou OOPNs (ObjectOriented Petri Nets), kterou budeme pouˇz´ıvat vˇzdy, kdyˇz budeme o objektovˇe orientovan´ ych Petriho s´ıt´ıch hovoˇrit jako o jazyku, o formalizmu nebo o syst´emu. Kdyˇz vˇsak budeme cht´ıt oznaˇcit urˇcit´ y model popsan´ y pomoc´ı OOPNs, budeme pouˇz´ıvat zkratku OOPN (Object-Oriented Petri Net).
6
s objektovou orientac´ı (zapouzdˇren´ı, dˇediˇcnost, polymorfizmus). Zaveden´ı tˇr´ıd a objekt˚ u do Petriho s´ıt´ı umoˇzn ˇuje snadn´e a pˇrirozen´e vytv´aˇren´ı rozs´ahl´ych a pˇresto pˇrehledn´ych model˚ u. Form´aln´ı anal´yza a verifikace OOPN model˚ u je moˇzn´a, protoˇze OOPNs jsou form´alnˇe definov´any, ale je pomˇernˇe sloˇzit´a, protoˇze OOPNs jsou bohat´ym modelovac´ım formalizmem. Z´akladn´ı principy OOPNs nyn´ı uk´aˇzeme na jednoduch´em pˇr´ıkladu OOPN modelu (obr. 1), kter´y se skl´ad´a ze dvou tˇr´ıd — tˇr´ıda Stack pˇredstavuje model z´asobn´ıku, zat´ımco tˇr´ıda Application ukazuje jeho pouˇzit´ı. jm´eno tˇr´ıdy tˇr´ıda
objektov´a s´ıt’
pˇredch˚ udce
Stack is_a PN hasDepth: n
parametrov´e m´ısto
x
n
top
push: x t
0
t>0
NT
selektor metody
err t=0
str´ aˇz pˇrechodu
NT:=t-1
(t,x)
(NT,x)
#ok
pop
t
NT
NT:=t+1
pop
t
x push
synchronn´ı port
(#ok,x)
#err
s´ıt’ metody
v´ ystupn´ı m´ısto
stack
return
return
Application is_a PN
m´ısto s poˇca´teˇcn´ım znaˇcen´ım
vstupn´ı hrana
akce pˇrechodu
s1:=Stack new t1
p1
p3
s1
v´ ystupn´ı hrana
1, 2, 3, 4
p2
x
s1
s1
t2 s1 push: x
testovac´ı hrana
y:=s1 pop
t3
y x
(#ok,x)
p5
p4 t4
Obr´azek 1: Jednoduch´y pˇr´ıklad OOPN modelu Principy objektov´e orientace jsou v OOPNs vyuˇzity pro strukturov´an´ı — tˇr´ıdy jsou uspoˇr´ad´any relac´ı dˇediˇcnosti, pro asynchronn´ı komunikaci slouˇz´ı metody a pro synchronn´ı komunikaci zase synchronn´ı porty. Prvky vysokou ´rovˇ nov´ych Petriho s´ıt´ı slouˇz´ı pro popis chov´an´ı objekt˚ u a metod. Pˇrechody jsou s m´ısty spojeny hranami, na nichˇz se nach´azej´ı inskripˇcn´ı v´yrazy. Pˇrechody mohou obsahovat str´aˇze, jejichˇz prostˇrednictv´ım lze volat synchronn´ı porty, a akce, z nichˇz lze zase volat metody. Dynamick´e chov´an´ı OOPNs je zaloˇzeno na konceptu ud´alost´ı. 7
2
C´ıl pr´ ace
C´ılem t´eto pr´ace je zlepˇsit moˇznosti form´aln´ı anal´ yzy a verifikace softwarov´ych syst´em˚ u popsan´ych pomoc´ı OOPNs. Tato oblast je ale pomˇernˇe rozs´ahl´a, proto se zamˇeˇr´ıme pouze na vybran´e metody a techniky. Prvn´ı oblast´ı, kter´e se budeme vˇenovat, je typov´a anal´yza OOPNs. OOPNs nejsou silnˇe typovan´e, ale urˇcit´e informace o typech znaˇcek, kter´e se mohou dostat do jednotliv´ych m´ıst modelu, mohou b´yt uˇziteˇcn´e. Prvn´ım c´ılem t´eto pr´ace je proto navrhnout metody pro automatick´e zjiˇst’ov´an´ı mnoˇzin typ˚ u znaˇcek, kter´e se pˇri evoluci mohou dostat do jednotliv´ych m´ıst OOPN model˚ u. Druh´y pˇr´ıstup k anal´yze OOPNs, kter´ym se v t´eto pr´aci budeme zab´yvat, je zaloˇzen na generov´an´ı a prohled´av´an´ı stavov´ych prostor˚ u. Hlavn´ım probl´emem tˇechto metod je probl´em stavov´e exploze. Druh´ym c´ılem t´eto pr´ace je proto paralelizace gener´atoru stavov´ych prostor˚ u OOPNs na architektur´ach se sd´ılenou pamˇet´ı, kter´a by mˇela omezit vliv probl´emu stavov´e exploze na praktickou pouˇzitelnost tˇechto metod.
3
Zvolen´ e metody zpracov´ an´ı
Pˇri n´avrhu metod pro automatickou typovou anal´yzu OOPNs budeme vych´azet z jejich dynamick´eho chov´an´ı, pˇriˇcemˇz se jeho vhodnou aproximac´ı pokus´ıme tyto metody urychlit. Zavedeme proto tzv. symbolickou simulaci, pˇri kter´e budou bˇeˇzn´e znaˇcky nahrazeny sv´ymi typy a bˇeˇzn´e ud´alosti budou nahrazeny symbolick´ymi ud´alostmi, kter´e budou pracovat se symbolick´ymi znaˇckami (tedy s typy). Dynamick´y charakter OOPNs, kter´y zvyˇsuje jejich vyjadˇrovac´ı schopnosti, komplikuje jejich form´aln´ı anal´yzu a verifikaci. Navrhneme zde dvˇe metody, kter´e se s dynamick´ym vytv´aˇren´ım objekt˚ u a metod pˇri typov´e anal´yze OOPNs vypoˇr´adaj´ı, kaˇzd´a vˇsak jin´ym zp˚ usobem. Z´akladn´ı principy typov´e anal´yzy ovˇeˇr´ıme implementac´ı prototypu typov´eho analyz´atoru OOPNs v Javˇe. Pˇri implementaci gener´atoru stavov´ych prostor˚ u OOPNs budeme pro u ´sporu pr´ace vych´azet z typov´eho analyz´atoru OOPNs. Jako implementaˇcn´ı jazyk proto pouˇzijeme tak´e Javu, kter´a se v oblasti vysoce n´aroˇcn´ych v´ypoˇct˚ u teprve prosazuje. Pro vlastn´ı paralelizaci gener´atoru stavov´ych prostor˚ u OOPNs pak pouˇzijeme n´astroj JOMP, kter´y zpˇr´ıstupˇ nuje pro Javu standard OpenMP pouˇz´ıvan´y pro jazyky C a Fortran. Vlastn´ı paralelizace na architektur´ach se sd´ılenou pamˇet´ı b´yv´a relativnˇe jednoduch´a. N´aroˇcnˇejˇs´ı je pak nalezen´ı optim´aln´ıho rozdˇelen´ı dat na sd´ılen´a a lok´aln´ı a synchronizace pˇr´ıstupu ke sd´ılen´ym dat˚ um pro dosaˇzen´ı co nejvyˇsˇs´ıho paraleln´ıho zrychlen´ı. Pop´ıˇseme zde v´ysledn´y paraleln´ı algoritmus a zhodnot´ıme dosaˇzen´e experiment´aln´ı v´ysledky. 8
4 4.1
Hlavn´ı v´ ysledky pr´ ace Automatick´ a typov´ a anal´ yza OOPNs
OOPNs nejsou silnˇe typovan´e, tzn. OOPN modely neobsahuj´ı explicitn´ı definice typ˚ u znaˇcek, kter´e jsou pˇr´ıpustn´e v m´ıstech ˇci v hranov´ych v´yrazech. Tato vlastnost OOPNs, kter´a byla pˇri n´avrhu OOPNs pˇrevzata z jazyka Smalltalk, je v´yhodn´a pro rychl´y n´avrh a prototypov´an´ı, protoˇze pˇri zmˇen´ach modelu nen´ı nutn´e udrˇzovat konzistenci typov´ych deklarac´ı. V nˇekter´ych pˇr´ıpadech vˇsak mohou b´yt informace o typech uˇziteˇcn´e. C´ılem typov´e anal´yzy je proto urˇcit typy znaˇcek, kter´e se mohou pˇri evoluci OOPN modelu vyskytnout v jeho jednotliv´ych m´ıstech. V´ysledky typov´e anal´yzy mohou b´yt vyuˇzity v nˇekolika oblastech. Typovou anal´yzu m˚ uˇzeme ch´apat jako speci´aln´ı prostˇredek pro ladˇen´ı OOPN model˚ u— pˇri modelov´an´ı m´ame obvykle urˇcitou pˇredstavu o tom, kter´e typy znaˇcek se mohou dostat do jednotliv´ych m´ıst modelu. Pokud se v´ysledky typov´e anal´yzy pro dan´y model liˇs´ı od naˇsich pˇredstav, m˚ uˇze to signalizovat chybu v modelu. Informace z´ıskan´e typovou anal´yzou mohou b´yt tak´e pouˇzity jako automaticky generovan´a souˇc´ast dokumentace modelu. V pˇr´ıpadˇe, ˇze bychom chtˇeli OOPN modely pˇrekl´adat do jin´ych formalizm˚ u, kter´e umoˇzn ˇuj´ı form´aln´ı anal´yzu a verifikaci a kter´e jsou obvykle silnˇe typovan´e, bylo by moˇzn´e v´ysledky typov´e anal´yzy vyuˇz´ıt pro zjiˇstˇen´ı v syntaxi OOPNs chybˇej´ıc´ı informace o typech. Znalost typ˚ u tak´e m˚ uˇze umoˇznit dalˇs´ı optimalizace simul´atoru OOPNs a gener´atoru stavov´ych prostor˚ u OOPNs. 4.1.1
Symbolick´ a simulace
Automatick´a typov´a anal´yza OOPNs je zaloˇzena na vhodn´e aproximaci chov´an´ı OOPNs s c´ılem sn´ıˇzit jej´ı ˇcasovou i prostorovou sloˇzitost na pˇrijatelnou u ´roveˇ n. Touto aproximac´ı se vˇsak zav´ad´ı urˇcit´a nepˇresnost, takˇze mnoˇziny typ˚ u, kter´e dostaneme jako v´ysledek typov´e anal´yzy, mohou b´yt vˇetˇs´ı, neˇz bychom dostali pˇresn´ym odvozen´ım z u ´pln´eho stavov´eho prostoru. Jsme-li si vˇedomi t´eto nepˇresnosti ve v´ysledc´ıch, jsou takto z´ıskan´e v´ysledky st´ale uˇziteˇcn´e. J´adrem pouˇzit´e aproximace je symbolick´a reprezentace, kdy jednotliv´e znaˇcky jsou nahrazeny sv´ym typem (napˇr. 7 7→ int). M´ısto bˇeˇzn´ych ud´alost´ı jsou pak prov´adˇeny symbolick´e ud´alosti, pˇri kter´ych nejsou ze vstupn´ıch m´ıst odeb´ır´any znaˇcky a str´aˇze pˇrechod˚ u nejsou vyhodnocov´any bˇeˇzn´ym zp˚ usobem (napˇr. pˇresn´e vyhodnocen´ı v´yrazu int ≥ int ned´av´a smysl), je pouze kontrolov´ano, zda ve vstupn´ıch a testovac´ıch m´ıstech jsou pˇr´ısluˇsn´e symbolick´e znaˇcky. Je tak´e nutn´e pˇredefinovat primitivn´ı funkce, kter´e se vyskytuj´ı v akc´ıch pˇrechod˚ u, aby pracovaly s typy (napˇr. int + int = int). Protoˇze pˇri symbolick´em prov´adˇen´ı 9
nem´a poˇcet znaˇcek vliv na proveditelnost pˇrechodu, nen´ı nutn´e uchov´avat informaci o poˇctu symbolick´ych znaˇcek v m´ıstˇe, takˇze m´ısto multimnoˇzin, kter´e se vyskytuj´ı ve znaˇcen´ı m´ıst a na hranov´ych v´yrazech, m˚ uˇzeme pracovat pouze s mnoˇzinami. Symbolickou simulaci ukonˇc´ıme v okamˇziku, kdy se proveden´ım ˇz´adn´e symbolick´e ud´alosti nezmˇen´ı symbolick´e znaˇcen´ı modelu. Z praktick´ych d˚ uvod˚ u poˇzadujeme, aby typov´a anal´yza skonˇcila. Mnoˇzina z´akladn´ıch typ˚ u OOPN modelu je samozˇrejmˇe koneˇcn´a. Nekoneˇcnost prostoru typ˚ u vˇsak mohou zp˚ usobit symbolick´e seznamy2, kter´e mohou b´yt sloˇzeny ze z´akladn´ıch typ˚ u a ze symbolick´ych seznam˚ u. Abychom omezili tento potenci´alnˇe nekoneˇcn´y prostor typ˚ u na koneˇcn´y a t´ım zaruˇcili koneˇcnost symbolick´e simulace, zavedeme limit na maxim´aln´ı hloubku zanoˇren´ı a na maxim´aln´ı d´elku symbolick´ych seznam˚ u, kter´e budou zpracov´any pˇresnˇe. Kdyˇz by pak nˇekter´y symbolick´y seznam mˇel pˇrekroˇcit stanoven´e meze, bude nahrazen pˇribliˇznou symbolickou hodnotou, kter´a nebude obsahovat informaci o hloubce zanoˇren´ı ani o pozic´ıch jednotliv´ych z´akladn´ıch v nˇem obsaˇzen´ych.
4.1.2
Statick´ a typov´ a anal´ yza
Statick´a i dynamick´a typov´a anal´yza je zaloˇzena na symbolick´e simulaci. Obˇe metody se ale liˇs´ı v pˇr´ıstupu k dynamick´emu charakteru OOPNs tedy k vytv´aˇren´ı objekt˚ u a k vol´an´ı metod. Pˇri statick´e typov´e anal´yze je na poˇc´atku pro kaˇzdou tˇr´ıdu vytvoˇrena jedna objektov´a s´ıt’ a pro kaˇzdou metodu jedna instance jej´ı s´ıtˇe. Poˇcet s´ıt´ı se pak v pr˚ ubˇehu symbolick´e simulace nemˇen´ı. Dynamick´e chov´an´ı OOPNs je zaloˇzeno na konceptu ud´alost´ı, coˇz se pochopitelnˇe odr´aˇz´ı i pˇri symbolick´e simulaci, kde vˇsak m´ısto o bˇeˇzn´ych ud´alostech hovoˇr´ıme o ud´alostech symbolick´ych. Proveditelnost symbolick´ych ud´alost´ı z´avis´ı na symbolick´em znaˇcen´ı vstupn´ıch a testovac´ıch m´ıst a na typov´e konzistenci nav´az´an´ı promˇenn´ych na hran´ach, ve str´aˇzi a v akci pˇrechodu. Efekt jednotliv´ych typ˚ u symbolick´ych ud´alost´ı je vˇsak odliˇsn´y od bˇeˇzn´ych ud´alost´ı. Proveden´ı symbolick´e ud´alosti N nem´a pˇri statick´e typov´e anal´yze za n´asledek vznik nov´eho objektu dan´e tˇr´ıdy, ale pouze pˇriˇrazen´ı identifik´atoru t´eto tˇr´ıdy do pˇr´ısluˇsn´e promˇenn´e. Pˇri proveden´ı symbolick´e ud´alosti F se pouze pˇridaj´ı pˇr´ısluˇsn´e symbolick´e znaˇcky do parametrov´ych m´ıst v s´ıti volan´e metody. Symbolick´a ud´alost J pak neruˇs´ı s´ıt’ metody, ale v souladu s v´ystupn´ımi hranami pˇrechodu pˇrid´a do pˇr´ısluˇsn´ych m´ıst symbolickou znaˇcku z v´ystupn´ıho m´ısta t´eto metody. Pˇri prov´adˇen´ı v´ypoˇct˚ u pˇri symbolick´e ud´alosti A m´ısto klasick´ych v´ypoˇct˚ u prob´ıhaj´ı pouze odpov´ıdaj´ıc´ı symbolick´e v´ypoˇcty nad typy (napˇr. int + int = int). 2
10
Seznamy zde ch´ apeme jako jeden z moˇzn´ ych pohled˚ u na n-tice.
4.1.3
Dynamick´ a typov´ a anal´ yza
Pˇri n´avrhu statick´e typov´e anal´yzy jsme kladli d˚ uraz na jej´ı rychlost, ale pˇri v´yskytu obecn´ych datov´ych struktur v modelu m˚ uˇzeme z´ıskat ponˇekud nepˇresn´e v´ysledky. Pro z´ısk´an´ı pˇresnˇejˇs´ıch v´ysledk˚ u typov´e anal´yzy pˇri zachov´an´ı pˇrijateln´e rychlosti v´ypoˇctu lze pouˇz´ıt tzv. dynamickou typovou anal´yzu, jej´ıˇz principy zde nyn´ı struˇcnˇe pop´ıˇseme. Z´akladn´ım rozd´ılem mezi dynamickou a statickou variantou typov´e anal´yzy je zp˚ usob, jak´ym jsou zpracov´any objekty a metody. Zat´ımco pˇri statick´e typov´e anal´yze existovala pr´avˇe jedna instance kaˇzd´e s´ıtˇe, pˇri dynamick´e typov´e anal´yze jsou jednotliv´e instance s´ıt´ı rozliˇsov´any. Ke kaˇzd´emu objektu je pˇri jeho vzniku pˇripojena instance objektov´e s´ıtˇe, kter´a je oznaˇcena poˇc´ateˇcn´ım symbolick´ym znaˇcen´ım. Pokud se v jednom m´ıstˇe objev´ı dva objekty stejn´e tˇr´ıdy a symbolick´e znaˇcen´ı objektov´e s´ıtˇe jednoho z nich pokr´yv´a symbolick´e znaˇcen´ı objektov´e s´ıtˇe druh´eho, m˚ uˇzeme tento druh´y objekt odstranit. Pokr´yvaj´ıc´ı objekt totiˇz poskytuje z hlediska symbolick´e simulace minim´alnˇe stejn´e chov´an´ı jako objekt pokryt´y. Pˇri ruˇsen´ı pokryt´eho objektu je vˇsak nutn´e pˇresunout vˇsechny jeho rozpracovan´e metody k objektu pokr´yvaj´ıc´ımu a tak´e nahradit vˇsechny reference na ruˇsen´y objekt, kter´e se vyskytuj´ı v aktu´aln´ım symbolick´em znaˇcen´ı, referencemi na pokr´yvaj´ıc´ı objekt. T´ım jsme vylouˇcili v´yskyt dvou objekt˚ u se stejn´ym symbolick´ym znaˇcen´ım v jednom m´ıstˇe. Pro zajiˇstˇen´ı koneˇcnosti dynamick´e typov´e anal´yzy n´am tedy zb´yv´a vyˇreˇsit posledn´ı probl´em souvisej´ıc´ı se zaveden´ım objekt˚ u. Jiˇz ukonˇcen´ı statick´e typov´e anal´yzy br´anily neomezen´e seznamy, coˇz jsme vyˇreˇsili zaveden´ım maxim´aln´ı hloubky zanoˇren´ı a d´elky seznam˚ u, kter´e byly zpracov´any pˇresnˇe. Pˇri dynamick´e typov´e anal´yze se mohou vyskytnout neomezen´e seznamy dynamicky vytv´aˇren´ych symbolick´ych objekt˚ u. Zavedeme proto limit na maxim´aln´ı vzd´alenost (mˇeˇreno poˇctem referenc´ı) od poˇc´ateˇcn´ıho objektu tak, ˇze symbolick´e ud´alosti, po jejichˇz proveden´ı by se ve znaˇcen´ı objevil pˇr´ıliˇs vzd´alen´y objekt, nebudou provediteln´e. Domn´ıv´ame se, ˇze kdyˇz zvol´ıme tento limit dostateˇcnˇe velk´y, nemuselo by m´ıt zaveden´ı tohoto limitu vliv na pˇresnost z´ıskan´ym v´ysledk˚ u. T´ımto jsme se tedy vypoˇr´adali s objekty v r´amci dynamick´e typov´e anal´yzy a zb´yv´a n´am vyˇreˇsit zpracov´an´ı metod. Pˇri vyvol´an´ı symbolick´e metody ze symbolicky prov´adˇen´eho pˇrechodu je vytvoˇrena nov´a instance s´ıtˇe t´eto metody, kter´a je oznaˇcena poˇc´ateˇcn´ım symbolick´ym znaˇcen´ım a do jej´ıch m´ıst pro parametry jsou um´ıstˇeny symbolick´e argumenty. Reference na tuto metodu je uchov´ana v nav´az´an´ı pr´avˇe prov´adˇen´eho pˇrechodu v promˇenn´e mid. Protoˇze pˇri symbolick´e simulaci neodeb´ır´ame z m´ıst symbolick´e znaˇcky, kter´e se do nich dostaly, lze se domn´ıvat, ˇze v´ysledek typov´e anal´yzy nez´aleˇz´ı na poˇrad´ı v´yskytu jednotliv´ych symbolick´ych ud´alost´ı, nebot’ v´yskyt jedn´e symbolick´e ud´alosti nem˚ uˇze zabr´anit budouc´ımu proveden´ı ostatn´ıch provediteln´ych 11
symbolick´ych ud´alost´ı. M˚ uˇzeme proto pˇri symbolick´e simulaci poˇzadovat, aby typov´a anal´yza vyvolan´e metody byla dokonˇcena co nejdˇr´ıve. Symbolick´a simulace se proto soustˇred´ı pr´avˇe na tuto novou metodu, pˇr´ıpadnˇe na dalˇs´ı metody z n´ı vyvolan´e. Po dokonˇcen´ı typov´e anal´yzy dan´e metody bude tato metoda ukonˇcena n´asleduj´ıc´ım zp˚ usobem. Aktu´aln´ı symbolick´e znaˇcen´ı m´ıst jej´ı s´ıtˇe bude pˇrid´ano ke st´avaj´ıc´ım mnoˇzin´am typ˚ u znaˇcek, kter´e se mohou dostat do jednotliv´ych m´ıst dan´e metody, a pro vˇsechny symbolick´e znaˇcky ve v´ ystupn´ım m´ıstˇe se dokonˇc´ı symbolick´e proveden´ı pˇrechodu, kter´y metodu vyvolal. S´ıt’ metody je pak zruˇsena a spolu s n´ı i vˇsechny symbolick´e objekty, na kter´e t´ımto krokem pˇrestal existovat odkaz. Abychom zaruˇcili koneˇcnost dynamick´e typov´e anal´yzy, omez´ıme potenci´aln´ı cykly vol´an´ı metod n´asleduj´ıc´ım pravidlem. Pokud je metoda (i nepˇr´ımo) vyvol´ana sama sebou, nejsou v n´ı provediteln´e ty ud´alosti, kter´e jsou aktu´alnˇe rozpracov´any v nadˇrazen´ych instanc´ıch t´eto metody. Protoˇze mnoˇzina symbolick´ych ud´alost´ı, kter´e se mohou vyskytnout v dan´e s´ıti, je koneˇcn´a, mus´ı b´yt koneˇcn´a i posloupnost vol´an´ı metod. Uk´azka v´ysledk˚ u dynamick´e typov´e anal´yzy je na obr´azku 2. Stack is_a PN x
top
push: x t
0
x push
t
NT
NT:=t+1
pop
err
t>0
NT
(NT,x)
#ok
pop
t
#err
(#ok,x)
stack
return
Application2 is_a PN p1
s1:=Stack new
t1
p6
s2:=Stack new
s1 p3
p2
x
s1
t2 s1 push: x
p8
s1
’a’, ’b’, ’c’ x
y:=s1 pop
t3
s2
t6 s2 push: x
x p4
t4
{int}
stack
{(int,int), (int,char)}
push: x
{int, char}
push: return
{symbol}
pop: return
{symbol, (symbol,int), (symbol,char)}
p1 p2 p3
{symbol} {Stack} {int}
p4
{symbol, (symbol,int), (symbol,char)}
s2
p5 p6 p7 p8
{int} {symbol} {Stack} {char}
y:=s2 pop
t7
p9
{symbol, (symbol,int), (symbol,char)}
p10
{char}
y
(#ok,x)
p5
top
p7
y x
t5
s2
1, 2, 3, 4
V´ysledn´e typy
t=0
NT:=t-1
(t,x)
return
M´ısto
(#ok,x)
p10
p9 t8
a) OOPN model se dvˇema z´asobn´ıky
b) V´ysledky anal´yzy
Obr´azek 2: Pˇr´ıklad v´ysledk˚ u dynamick´e typov´e anal´ yzy OOPNs 12
4.2
Paralelizace gener´ atoru stavov´ ych prostor˚ u OOPNs
Z´akladn´ım probl´emem metod form´aln´ı anal´yzy a verifikace zaloˇzen´ych na generov´an´ı a proch´azen´ı stavov´ych prostor˚ u je probl´em stavov´e exploze, kter´y br´an´ı jejich u ´spˇeˇsn´emu nasazen´ı i pro rozs´ahlejˇs´ı modely. Pro omezen´ı praktick´ych dopad˚ u probl´emu stavov´e exploze lze vyuˇz´ıt ˇradu optimalizac´ı zaloˇzen´ych na redukc´ıch stavov´eho prostoru nebo paraleln´ı pˇr´ıstup. Pr´avˇe vyuˇzit´ım paraleln´ıho pˇr´ıstupu pˇri generov´an´ı a proch´azen´ı stavov´ych prostor˚ u se zab´yv´ame v t´eto pr´aci. Jako modelovac´ı formalizmus byly pouˇzity OOPNs, ale d´ale popsan´y paraleln´ı algoritmus lze pouˇz´ıt i pro dalˇs´ı modelovac´ı formalizmy. Neˇz se budeme vˇenovat paralelizaci gener´atoru stavov´ych prostor˚ u OOPNs, pop´ıˇseme zde jeho z´akladn´ı principy. Stavov´y prostor je d´an mnoˇzinou stav˚ u, mnoˇzinou struktur´aln´ıch pˇrechod˚ u, mnoˇzinou s´emantick´ych pˇrechod˚ u a poˇc´ateˇcn´ım stavem. Stav OOPN modelu je relativnˇe sloˇzit´y a odpov´ıd´a syst´emu vz´ajemnˇe propojen´ych objekt˚ u, pˇriˇcemˇz kaˇzd´y objekt se skl´ad´a z pr´avˇe jedn´e instance objektov´e s´ıtˇe a z nˇekolika instanc´ı s´ıt´ı pr´avˇe rozpracovan´ych metod. Stav kaˇzd´e s´ıtˇe je d´an znaˇcen´ım vˇsech m´ıst s´ıtˇe a pˇr´ıpadn´ym odkazem na rozpracovanou metodu u pˇrechod˚ u s´ıtˇe. Mnoˇzina struktur´aln´ıch pˇrechod˚ u odpov´ıd´a mnoˇzinˇe pˇrechod˚ u a mnoˇzina s´emantick´ych pˇrechod˚ u ud´alostem. Poˇc´ateˇcn´ı stav OOPN modelu odpov´ıd´a jednomu objektu hlavn´ı tˇr´ıdy, kter´y obsahuje pouze objektovou s´ıt’ oznaˇcenou poˇc´ateˇcn´ım znaˇcen´ım a bez odkaz˚ u na rozpracovan´e metody u pˇrechod˚ u. Pˇri generov´an´ı stavov´eho prostoru je obvykle omezuj´ıc´ım faktorem dostupn´a operaˇcn´ı pamˇet’, proto se t´emˇeˇr vˇzdy do stavov´eho prostoru ukl´adaj´ı pouze unik´atn´ı stavy. Pokud je z nˇekter´eho uzlu vygenerov´an n´asledn´ık, kter´y jiˇz ve stavov´em prostoru existuje, je tento existuj´ıc´ı stav povaˇzov´an za n´asledn´ıka a novˇe vygenerovan´y duplicitn´ı stav nen´ı nutn´e znovu ukl´adat. Pˇri vygenerov´an´ı kaˇzd´eho stavu je vˇsak nutn´e proj´ıt dosud vygenerovan´y stavov´y prostor a zjistit, zda novˇe vygenerovan´y stav je unik´atn´ı nebo duplicitn´ı. To je ˇcasovˇe n´aroˇcn´e zvl´aˇstˇe pro vˇetˇs´ı stavov´e prostory. Hled´an´ı stav˚ u ve stavov´em prostoru i operace porovn´an´ı dvou stav˚ u mus´ı b´yt proto co nejrychlejˇs´ı. Rychl´e vyhled´av´an´ı ve stavov´em prostoru je zajiˇstˇeno vyhled´avac´ı tabulkou (angl. hash table), v n´ıˇz se k jednotliv´ym stav˚ um pˇristupuje pomoc´ı vyhled´avac´ıho kl´ıˇce. Hlavn´ımi u ´koly pˇri paralelizaci libovoln´eho algoritmu je rozdˇelen´ı pr´ace mezi jednotliv´e procesory a zajiˇstˇen´ı synchronizovan´eho pˇr´ıstupu ke sd´ılen´ym dat˚ um. V naˇsem pˇr´ıpadˇe se proto budeme d´ale zab´yvat stavov´ym prostorem, kter´y je realizov´an vyhled´avac´ı tabulkou, seznamem dosud neprozkouman´ych stav˚ u a odd´ılem pro ukl´ad´an´ı znaˇcen´ı. 13
4.2.1
Rozdˇ elen´ı vyhled´ avac´ı tabulky
Vyhled´avac´ı tabulku, kter´a slouˇz´ı pro rychl´y pˇr´ıstup ke stav˚ um, rozdˇel´ıme na v´ıce ˇc´ast´ı (vzhledem ke struktuˇre vyhled´avac´ı tabulky to nen´ı obt´ıˇzn´e). Ke kaˇzd´e takov´e tabulce pak pˇriˇrad´ıme seznam dosud nezpracovan´ych stav˚ u, kter´e by mˇely b´yt uloˇzeny pr´avˇe do t´eto vyhled´avac´ı tabulky. Pˇrirozen´y zp˚ usob, kter´ym jsme zaˇcali, je rozdˇelen´ı vyhled´avac´ı tabulky na tolik ˇc´ast´ı, kolik m´ame k dispozici procesor˚ u (vl´aken t´ymu). Pˇri tomto pˇr´ıstupu vˇsak velice ˇcasto doch´azelo k nerovnomˇern´emu rozdˇelen´ı pr´ace mezi jednotliv´e procesory. Rozdˇelili jsme proto vyhled´avac´ı tabulku na v´ıce ˇc´ast´ı, neˇz je vl´aken. Jednotliv´a vl´akna se pak u jednotliv´ych tabulek stˇr´ıdaj´ı, jak ukazuje obr´azek 3, na kter´em je poˇc´ateˇcn´ı pˇriˇrazen´ı vl´aken k datov´ym uzl˚ um (vnitˇrn´ı struktura uzl˚ u a vl´aken je na obr´azku 4).
U0
U1
Vl´akno 0 U5
U2 Vl´akno 1
U4
U3
Obr´azek 3: Dˇelen´ı pr´ace mezi dvˇe vl´akna Pokud vl´akno zpracuje vˇsechny nezpracovan´e stavy pˇr´ısluˇsej´ıc´ı k dan´emu uzlu, tento uzel opust´ı a hled´a dalˇs´ı uzel, kter´y obsahuje nˇejak´e nezpracovan´e stavy. Pokud naraz´ı na uzel pˇriˇrazen´y jin´emu vl´aknu, pˇreskoˇc´ı ho. Experiment´alnˇe jsme urˇcili, ˇze poˇcet datov´ych uzl˚ u je vhodn´e zvolit jako trojn´asobek poˇctu vl´aken, kter´e se u jednotliv´ych vyhled´avac´ıch tabulek stˇr´ıdaj´ı. 4.2.2
Pˇ r´ıstup k nezpracovan´ ym stav˚ um
Na poˇc´atku je v seznamu nezpracovan´ych stav˚ u pouze poˇc´ateˇcn´ı stav modelu. Generov´an´ı stavov´eho prostoru pak spoˇc´ıv´a v postupn´em zpracov´an´ı dosud nezpracovan´ych stav˚ u, pˇriˇcemˇz zpracov´an´ım se rozum´ı zkontrolov´an´ı, zda se jiˇz stav ve stavov´em prostoru nenach´az´ı, a pokud ne, vygeneruj´ı se vˇsichni 14
jeho n´asledn´ıci, kteˇr´ı jsou pak pˇrid´ani na konec seznamu dosud nezpracovan´ych stav˚ u. Kdyby byl seznam dosud nezpracovan´ych stav˚ u sd´ılen´y vˇsemi vl´akny, bylo by sice nejlepˇs´ı rozdˇelen´ı pr´ace mezi vˇsechna vl´akna, ale doch´azelo by k ˇcast´ym koliz´ım. Rozdˇelili jsme proto tento seznam na nˇekolik ˇc´ast´ı, kter´e pochopitelnˇe koresponduj´ı s rozdˇelen´ım vyhled´avac´ı tabulky (viz obr´azek 4). uzel vl´akno vyhled´avac´ı tabulka
odd´ıl pro znaˇcen´ı
lok´aln´ı seznam stav˚ u seznam stav˚ u
Obr´azek 4: Vnitˇrn´ı datov´a struktura uzl˚ u a vl´aken K takov´emu ˇc´asteˇcn´emu seznamu nezpracovan´ych stav˚ u pak pˇristupuj´ı vˇsechna vl´akna t´ymu, protoˇze do nˇej vkl´adaj´ı vygenerovan´e stavy, kter´e patˇr´ı do pˇr´ısluˇsn´e vyhled´avac´ı tabulky. Nejˇcastˇeji vˇsak k nˇemu pˇristupuje vl´akno, kter´e zpracov´av´a dan´y uzel, protoˇze z nˇej jednotliv´e stavy vyj´ım´a a zpracov´av´a. Abychom omezili konflikty mezi vl´akny na minimum, m´a kaˇzd´e vl´akno sv˚ uj lok´aln´ı seznam nezpracovan´ych stav˚ u, kter´y zpracov´av´a, dokud nen´ı pr´azdn´y. Pak ho prostˇe vymˇen´ı za seznam stav˚ u, do kter´eho zat´ım mohla ostatn´ı vl´akna pˇridat dalˇs´ı stavy ke zpracov´an´ı. Pokud ani v tomto seznamu stav˚ u nen´ı nic ke zpracov´an´ı, vl´akno uzel opust´ı. Zkoumali jsme tak´e dva moˇzn´e zp˚ usoby ˇrazen´ı dosud nezpracovan´ych stav˚ u. Doˇsli jsme k na prvn´ı pohled pˇrekvapiv´emu z´avˇeru, ˇze nezpracovan´e stavy je lepˇs´ı ukl´adat do z´asobn´ıku (LIFO) neˇz do fronty (FIFO). Pˇri generov´an´ı rozs´ahl´ych stavov´ych prostor˚ u je stav na zaˇc´atku fronty ve vyrovn´avac´ı pamˇeti s menˇs´ı pravdˇepodobnost´ı, neˇz je tomu u stavu na vrcholu z´asobn´ıku. Pouˇzit´ım z´asobn´ıku se tedy zv´yˇs´ı u ´spˇeˇsnost hled´an´ı ve vyrovn´avac´ı pamˇeti (angl. cache hit rate) a t´ım se urychl´ı bˇeh programu. Druhou moˇznou pˇr´ıˇcinou je prom´ıch´an´ı stav˚ u generovan´ych v r˚ uzn´ych f´az´ıch generov´an´ı v z´asobn´ıku, kter´e m˚ uˇze m´ıt za n´asledek lepˇs´ı rozdˇelen´ı nezpracovan´ych stav˚ u mezi procesory a t´ım ke sn´ıˇzen´ı poˇctu koliz´ı. 15
4.2.3
Odd´ıl pro znaˇ cen´ı m´ıst
Posledn´ı datovou strukturou (z obr´azku 4), kterou jsme se dosud nezab´yvali, je odd´ıl pro ukl´ad´an´ı znaˇcen´ı m´ıst. Pˇred t´ım, neˇz se t´ımto probl´emem budeme zab´yvat, mus´ıme si uvˇedomit, ˇze ˇcten´ı z tohoto odd´ılu bude velice ˇcast´e, zat´ımco zaps´an´ı nov´e hodnoty do nˇej bude – kromˇe poˇc´ateˇcn´ı f´aze – sp´ıˇse v´yjimeˇcn´e. Odd´ıl pro ukl´ad´an´ı znaˇcen´ı by mohl b´yt spoleˇcn´y pro vˇsechna vl´akna, coˇz by mohlo zv´yˇsit poˇcet koliz´ı. Druhou moˇznost´ı je pˇriˇradit kaˇzd´emu vl´aknu lok´aln´ı odd´ıl pro ukl´ad´an´ı znaˇcen´ı. Do tohoto odd´ılu se vkl´adaj´ı znaˇcen´ı pˇri generov´an´ı stav˚ u. Protoˇze vˇsak vl´akna pracuj´ı i se stavy, kter´e byly vygenerov´any jin´ymi vl´akny, je nutn´e, aby vˇsechny lok´aln´ı odd´ıly obsahovaly stejn´e hodnoty. Proto je nutn´e, aby novˇe nalezen´e znaˇcen´ı bylo zaps´ano do odd´ıl˚ u vˇsech vl´aken. Tento postup vˇsak zvyˇsuje pamˇet’ov´e n´aroky. Experiment´alnˇe jsme ovˇeˇrili, ˇze velikost odd´ılu pro znaˇcen´ı je v porovn´an´ı s velikost´ı stavov´eho prostoru zanedbateln´a, takˇze jej lze udrˇzovat na nˇekolika m´ıstech. M˚ uˇze se vˇsak pro nˇekter´e typy stavov´ych prostor˚ u uk´azat, ˇze jako v´yhodnˇejˇs´ı bude varianta se spoleˇcn´ym odd´ılem pro znaˇcen´ı.
4.2.4
Shrnut´ı dosaˇ zen´ ych v´ ysledk˚ u
Pouˇzit´ım vˇsech v´yˇse uveden´ych optimalizac´ı paraleln´ı verze gener´atoru jsme oproti optimalizovan´e sekvenˇcn´ı verzi dos´ahli paraleln´ıho zrychlen´ı 3,3 pˇri pouˇzit´ı ˇsestn´acti procesor˚ u na syst´emu Sun Fire 15k a zrychlen´ı aˇz 2,3 pˇri pouˇzit´ı ˇctyˇr procesor˚ u na syst´emu Sun Enterprise 450. I pˇres relativnˇe n´ızkou efektivitu lze tyto v´ysledky povaˇzovat za uspokojiv´e. Kromˇe dosaˇzen´ı urˇcit´eho zrychlen´ı se n´am podaˇrilo na obou architektur´ach dos´ahnout velice vyv´aˇzen´eho rozdˇelen´ı pr´ace mezi jednotliv´a vl´akna, coˇz je nezbytn´a podm´ınka pro dosaˇzen´ı vysok´e efektivity paraleln´ıch v´ypoˇct˚ u. Hlavn´ım probl´em, kter´y br´an´ı vyˇsˇs´ımu paraleln´ımu zrychlen´ı gener´atoru, je pˇr´ıliˇs vysok´a reˇzie spojen´a se spr´avou pamˇeti – garbage collecting. Moˇznou cestou k odstranˇen´ı tohoto probl´emu je implementovat uˇzivatelsk´e pˇridˇelov´an´ı pamˇeti, kter´e bylo s u ´spˇechem pouˇzito v podobn´e situaci v [1]. Dalˇs´ım ˇreˇsen´ım je v´yraznˇe zredukovat poˇcet vytv´aˇren´ych objekt˚ u, nicm´enˇe vzhledem k objektovˇe orientovan´ym rys˚ um OOPNs je tˇeˇzk´e implementovat stavov´y gener´ator bez Java objekt˚ u a bez garbage collectingu. Pokud bychom vˇsak chtˇeli zkoumat stavov´y prostor model˚ u popsan´ych formalizmem s niˇzˇs´ı dynamikou, lze pˇredpokl´adat, ˇze v´yˇse navrˇzen´y algoritmus bude velice dobr´y. 16
5
Z´ avˇ er
V t´eto pr´aci byly navrˇzeny nov´e metody a techniky pro form´aln´ı anal´yzu OOPN model˚ u. V´yznam t´eto pr´ace proto spoˇc´ıv´a pˇredevˇs´ım v rozvinut´ı v´ysledk˚ u dˇr´ıve dosaˇzen´ych dr. Janouˇskem [8] a dr. Vojnarem [22] v oblasti OOPNs. Urˇcit´y dopad na oblasti mimo OOPNs a d´ıky pouˇzit´ı Javy a n´astroje JOMP dokonce i na oblasti mimo form´aln´ı anal´yzu a verifikaci m˚ uˇze m´ıt ˇc´ast pr´ace vˇenovan´a paraleln´ımu zpracov´an´ı stavov´ych prostor˚ u OOPNs.
5.1
Dosaˇ zen´ e v´ ysledky
Dosaˇzen´e v´ysledky lze rozdˇelit do dvou oblast´ı. Nejdˇr´ıve byly pops´any z´akladn´ı principy automatick´e typov´e anal´yzy a jako hlavn´ı pˇr´ınos v t´eto oblasti byly navrˇzeny dva algoritmy pro typovou anal´yzu — tzv. statick´a a dynamick´a typov´a anal´yza. Obˇe metody se snaˇz´ı vyˇreˇsit probl´emy spojen´e zejm´ena s dynamikou OOPNs, kaˇzd´a vˇsak jin´ym zp˚ usobem. Statick´a typov´a anal´yza probl´emy ˇreˇs´ı zjednoduˇsen´ım situace, ˇc´ımˇz se sice v´ypoˇcet urychl´ı ale za cenu zanesen´ı dalˇs´ıch nepˇresnost´ı do v´ysledk˚ u. Dynamick´a typov´a anal´yza se naopak snaˇz´ı OOPN objekty a metody zpracovat pˇresnˇe za cenu sloˇzitˇejˇs´ıho a pomalejˇs´ıho algoritmu. Druhou oblast´ı, ve kter´e byly v r´amci t´eto pr´ace dosaˇzeny zaj´ımav´e v´ysledky, je oblast paraleln´ıho zpracov´an´ı stavov´ych prostor˚ u OOPNs na architektur´ach se sd´ılenou pamˇet´ı. Byl navrˇzen a implementov´an algoritmus pro paraleln´ı generov´an´ı stavov´ych prostor˚ u zahrnuj´ıc´ı detekci uv´aznut´ı. Tento algoritmus obsahuje unik´atn´ı mechanizmus pro synchronizaci pˇr´ıstupu k vyhled´avac´ı tabulce i velice u ´ˇcinn´y mechanizmus pro rozdˇelov´an´ı pr´ace mezi jednotliv´e procesory. Zde navrˇzen´e principy a techniky proto mohou b´yt uˇziteˇcn´e i pro paralelizaci dalˇs´ıch podobn´ych probl´em˚ u.
5.2
Moˇ znosti dalˇs´ıho v´ yzkumu
OOPNs jsou bohat´y formalizmus, a proto je implementace n´astroj˚ u pro pr´aci s nimi znaˇcnˇe ˇcasovˇe n´aroˇcn´a. V r´amci bakal´aˇrsk´ych a diplomov´ych prac´ı lze oˇcek´avat u ´pln´e dokonˇcen´ı automatick´eho typov´eho analyz´atoru OOPNs. D´ale se pl´anuje propojen´ı vytvoˇren´eho prototypu gener´atoru stavov´ych prostor˚ u OOPNs, kter´y zat´ım nepodporuje vˇsechny vlastnosti OOPNs, s novˇe vytv´aˇren´ym otevˇren´ym procesorem a simul´atorem OOPNs [9]. V paralelizaci gener´atoru stavov´ych prostor˚ u byly dosaˇzeny dobr´e v´ysledky, nicm´enˇe hlavn´ım probl´emem, kter´y br´an´ı dosaˇzen´ı vyˇsˇs´ıho paraleln´ıho zrychlen´ı, st´ale z˚ ust´av´a garbage collecting. Lze se pokusit jeˇstˇe v´ıce zredukovat pamˇet’ov´e operace nutn´e pro generov´an´ı a ukl´ad´an´ı stav˚ u OOPNs, nicm´enˇe 17
vzhledem k dynamick´emu charakteru OOPNs nebude moˇzn´e garbage collecting zcela eliminovat. Zaj´ımav´ym smˇerem v´yzkumu by tak´e mohla b´yt aplikace navrˇzen´eho paraleln´ıho algoritmu pro formalizmy s menˇs´ı dynamikou chov´an´ı a s jednoduˇsˇs´ımi stavy (napˇr. P/T Petriho s´ıtˇe). Aktu´aln´ı verze gener´atoru stavov´ych prostor˚ u OOPNs umoˇzn ˇuje pouze detekci uv´aznut´ı. Dalˇs´ım logicky navazuj´ıc´ım krokem je tedy rozˇs´ıˇren´ı gener´atoru o paraleln´ı dotazov´an´ı nad stavov´ymi prostory OOPN, kter´e je vˇsak pomˇernˇe n´aroˇcn´e vzhledem k dynamice OOPNs plynouc´ı z jejich objektov´e orientace.
5.3
Souvisej´ıc´ı publikace
V´yˇcet autorov´ych publikac´ı vˇenuj´ıc´ıch se d´ılˇc´ım v´ysledk˚ um t´eto pr´ace zde uv´ad´ıme v chronologick´em poˇrad´ı. V pr´aci byly vyuˇzity v´ysledky dosaˇzen´e jiˇz v r´amci inˇzen´yrsk´eho studia [10, 11]. Probl´emu efektivn´ıho vyhodnocov´an´ı izomorfizmu graf˚ u, kter´e je d˚ uleˇzit´e pˇri ukl´ad´an´ı vygenerovan´ych stav˚ u do stavov´eho prostoru, se vˇenuje [13]. Motivaci pro typovou anal´yzu a z´akladn´ı metody pro jej´ı implementaci lze nal´ezt v [16]. Zmapov´an´ı metod zaloˇzen´ych na generov´an´ı a proch´azen´ı stavov´ych prostor˚ u a metod pro omezen´ı probl´emu stavov´e exploze se zhodnocen´ım jejich pouˇzitelnosti v kontextu OOPNs je v [12]. OOPN model protokolu ABP [14] lze vyuˇz´ıt jako pˇr´ıpadovou studii pro ovˇeˇrov´an´ı vytv´aˇren´ych n´astroj˚ u form´aln´ı anal´yzy a verifikace. Integrace n´astroj˚ u pro typovou anal´yzu a pro generov´an´ı a proch´azen´ı stavov´ych prostor˚ u OOPNs usnadˇ nuj´ıc´ı implementaci identifikac´ı ˇc´ast´ı spoleˇcn´ych obˇema n´astroj˚ um byla pops´ana v [17]. Zkuˇsenosti z´ıskan´e z implementace typov´eho analyz´atoru OOPNs jsou shrnuty v [15].
Literatura [1] Allmaier, S. C., Horton, G. Parallel Shared-Memory State-Space Exploration in Stochastic Modeling. In Bilardi, G., et al., editoˇri, Solving Irregularly Structured Problems in Parallel, 4th International Symposium, IRREGULAR’97, volume 1253 of Lecture Notes in Computer Science, Paderborn, Germany, 1997. Springer. s. 207–218. ISBN 3-540-63138-0. [2] Bouajjani, A., Habermehl, P., Vojnar, T. Abstract Regular Model Checking. In Computer Aided Verification - CAV’2004, volume 3114 of Lecture Notes in Computer Science, Berlin, Germany, 2004. Springer Verlag. s. 372–386. ˇ ska, M., Haˇsa, L., Vojnar, T. Partial-Order Reduction in Model Chec[3] Ceˇ king of Object-Oriented Petri Nets. In Computer Aided Systems Theory 18
– EUROCAST 2003, volume 2809 of Lecture Notes in Computer Science, Berlin, Germany, 2003. Springer-Verlag. s. 265–278. ISBN 3-540-20221-8. ˇ ska, M., Janouˇsek, V., Vojnar, T. PNtalk – A Computerized Tool for [4] Ceˇ Object-Oriented Petri Nets Modelling. In Pichler, F., Moreno-D´ıaz, R., editoˇri, Computer Aided Systems Theory – EUROCAST’97, volume 1333 of Lecture Notes in Computer Science, Las Palmas de Gran Canaria, Canary Islands, Spain, 1997. Springer-Verlag. s. 591–610. ISBN 3-540-638113. ˇ ska, M., Sk´acel, M. Petri Net Tool PESIM. In 5th International [5] Ceˇ Workshop on Petri Nets and Performance Models, Toulouse, France, 1993. [6] Clarke, E. M., Grumberg, O., Peled, D. A. Model Checking. The MIT Press, Cambridge, Massachusetts, United States of America, 1999. 314 s. ISBN 0-262-03270-8. [7] Hrub´y, M., R´abov´a, Z. Modelling of Real-world Objects using the HELEF Language. ASU Newsletter: a publication of the Association of SIMULA Users., 38(1):47–57, 2002. ISSN 1102-593X. ´ [8] Janouˇsek, V. Modelov´ an´ı objekt˚ u Petriho s´ıtˇemi. Disertaˇcn´ı pr´ace, Ustav informatiky a v´ypoˇcetn´ı techniky, Fakulta elektrotechniky a informatiky, ˇ a republika, 1998. 137 s. Vysok´e uˇcen´ı technick´e v Brnˇe, Brno, Cesk´ [9] Koˇc´ı, R. The Open Architecture of the PNtalk System. In Proceedings of the International Conference and Competition – Student EEICT’2003, ˇ a republika, 2003. s. 358–362. ISBN 80-214-2401-X. Brno, Cesk´ [10] Kˇrena, B. Podpora pro anal´yzu stavov´ych prostor˚ u objektovˇe orientovan´ych Petriho s´ıt´ı. In Baˇstinec, J., Dibl´ık, J., editoˇri, Sborn´ık prac´ı ˇ a republika, kvˇeten 2000. Akademick´e studen˚ u a doktorand˚ u, Brno, Cesk´ nakladatelsv´ı CERM, s.r.o. s. 192–194. ISBN 80-7204-155-X. [11] Kˇrena, B. Podpora pro anal´yzu stavov´ych prostor˚ u objektovˇe oriento´ van´ych Petriho s´ıt´ı. Diplomov´a pr´ace, Ustav informatiky a v´ypoˇcetn´ı techniky, Fakulta elektrotechniky a informatiky, Vysok´e uˇcen´ı technick´e ˇ a republika, ˇcerven 2000. 59 s. v Brnˇe, Brno, Cesk´ [12] Kˇrena, B. First Approach to Model Checking in Object-Oriented Petri ˇ Nets. In Stefan, J., editor, Proceedings of XIIIrd International Autumn Colloquium on Advanced Simulation of Systems, ASIS’2001, Velk´e Losiny, ˇ a Republika, z´aˇr´ı 2001. MARQ Ostrava. s. 105–110. ISBN 80-85988Cesk´ 61-5. 19
[13] Kˇrena, B. The Graph Isomorphism Problem. In Arnoˇst, V., editor, Proˇ a receedings of 7th Conference Student FEI 2001, volume 2, Brno, Cesk´ publika, duben 2001. Vysok´e uˇcen´ı technick´e v Brnˇe. s. 343–347. ISBN 80-214-1860-5. [14] Kˇrena, B. A Case Study: Modelling Alternating Bit Protocol by PNˇ talk. In Stefan, J., editor, Proceedings of 36th International Conference on Modelling and Simulation of Systems, MOSIS’02, volume I, Roˇznov ˇ a republika, duben 2002. MARQ Ostrava. s. 65–72. pod Radhoˇstˇem, Cesk´ ISBN 80-85988-71-2. [15] Kˇrena, B. Object-Oriented Petri Nets and their Application and Type Analysis. Information Technologies and Control, 1(1):27–31, 2003. [16] Kˇrena, B., Vojnar, T. Type Analysis in Object-Oriented Petri Nets. In Zendulka, J., editor, Proceedings of 4th International Conference on Inforˇ a Repubmation System Modelling, ISM’01, Hradec nad Moravic´ı, Cesk´ lika, kvˇeten 2001. MARQ Ostrava. s. 173–180. ISBN 80-85988-51-8. ˇ ska, M. Integrated Type Analyzer and State [17] Kˇrena, B., Vojnar, T., Ceˇ Space Generator of Object-Oriented Petri Nets. In Brazilian Petri Net Meeting, Natal, Brazil, z´aˇr´ı 2002. 6 s. [18] Peringer, P. Hierarchick´e modelov´ an´ı na b´ azi komunikuj´ıc´ı objekt˚ u. Di´ sertaˇcn´ı pr´ace, Ustav informatiky a v´ypoˇcetn´ı techniky, Fakulta elektroˇ a retechniky a informatiky, Vysok´e uˇcen´ı technick´e v Brnˇe, Brno, Cesk´ publika, 1996. 82 s. [19] Petri, C. A. Kommunikation mit Automaten. Disertaˇcn´ı pr´ace, Institut f¨ ur Instrumentelle Mathematik, University Bonn, Germany, 1962. Available as Schriften des IIM Nr. 2. (In German). [20] Valmari, A. The State Explosion Problem. In Reisig, W., Rozenberg, G., editoˇri, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, volume 1491 of Lecture Notes in Computer Science, s. 429–528. SpringerVerlag, 1998. ´ [21] Vojnar, T. Syst´em PNtalk. Technick´a zpr´ava, Ustav informatiky a v´ypoˇcetn´ı techniky, Fakulta elektrotechniky a informatiky, Vysok´e uˇcen´ı ˇ a republika, 1997. technick´e v Brnˇe, Brno, Cesk´ [22] Vojnar, T. Towards Formal Analysis and Verification over State Spa´ ces of Object-Oriented Petri Nets. Disertaˇcn´ı pr´ace, Ustav informatiky a v´ypoˇcetn´ı techniky, Fakulta elektrotechniky a informatiky, Vysok´e uˇcen´ı ˇ a republika, 2001. 148 s. technick´e v Brnˇe, Brno, Cesk´ 20
Curriculum Vitae Z´ akladn´ı u ´ daje Jm´eno a pˇr´ıjmen´ı: Bohuslav Kˇrena Narozen: 25. 6. 1977, Brno Vzdˇel´an´ı: Ing., 2000, FEI VUT v Brnˇe
Zahraniˇ cn´ı st´ aˇ ze • 16. 10. 2002 - 19. 12. 2002, Central Laboratory for Parallel Processing, Bulharsk´a akademie vˇed, Sofie, Bulharsko, projekt BIS-21. • 21. 5. 2003 - 9. 7. 2003, Edinburgh Parallel Computing Centre, The University of Edinburgh, Edinburgh, Skotsko, program TRACS. • 31. 5. 2004 - 31. 7. 2004, Sofware Testing and Analysis Laboratory, Universit`a degli Studi di Milano - Bicocca, Milano, It´alie, projekt SegraVis.
Vybran´ e projekty • Modelov´ an´ı, verifikace a prototypov´ an´ı distribuovan´ych aplikac´ı s vyuˇ ˇzit´ım Petriho s´ıt´ı, GACR, k´od GA102/00/1017, 2000-2002. ˇ • Prostˇred´ı pro v´yvoj, modelov´ an´ı a aplikaci heterogenn´ıch syst´em˚ u, GACR, k´od GA102/01/1485, 2001-2004. • Metody form´ aln´ı anal´yzy a verifikace v objektovˇe orientovan´ych Petriho ˇ ˇ s´ıt´ıch, FRVS MSMT, k´od FR1948/2002/G1, 2002. • Bulgarian Information Society Center of Excellence for Education, Science and Technology in 21 Century, BIS-21, EU, k´od ICA1-2000-70016, 2002. • Access to Research Infrastructure Action of the Improving Human Potential Programme, TRACS, EU, k´od HPRI-CT-1999-00026, 2003. • Automatizovan´e metody a n´ astroje pro v´yvoj spolehliv´ych paraleln´ıch ˇ k´od GA102/04/0780, 2004-2006. a distribuovan´ych syst´em˚ u, GACR, • SegraVis – Syntactic and Semantic Integration of Visual Modelling Techniques, EU, k´od HPRN-CT-2002-00275, 2004-2005.
21
Abstract Object-oriented Petri nets (OOPNs) have been developed (in [8, 22]) to support modelling, investigating, and prototyping concurrent object-oriented software systems. OOPNs join together Petri net concepts (causality, nondeterminism, and concurrency) with object orientation concepts (encapsulation, inheritance, and polymorphism). Objects and classes allow OOPNs to be used for creating large and well-arranged models which is a significant benefit for their practical usage. Formal analysis and verification of OOPN models is possible due their exact mathematical definition. It is, however, quite complex because OOPNs are a rich formalism. In this work, we concentrate on two analysis methods in the context of OOPNs.
Type Analysis The first investigated method is type analysis. OOPNs — unlike many of the common dialects of high-level Petri nets — are not (syntactically) strongly typed which means that modellers do not have to explicitly declare the types of OOPN places, the types of the variables used in OOPN inscriptions, and so on. The goal of the type analysis is to automatically compute the types of tokens that can get to the particular places of an OOPN model. Weak typing of PNtalk is useful in the area of prototyping, however, as mentioned below, there are situations in which it may be useful to know at least something about the types associated with the particular OOPN places. Type analysis can be understood as a special means of debugging OOPN models: modellers usually have some intuition about what types of tokens should get into particular OOPN places and if the results of a type analysis are different, there may be a fault in the model. The information derived from type analysis can also be used as a part of the documentation of a model. Moreover, the results obtained from type analysis can further be useful when translating OOPNs into models described by some other — usually strongly typed — modelling languages. Finally, the results which may be obtained from type analysis may be used to optimize the internal representation of OOPNs and thus to increase the efficiency of running OOPN models and generating their state spaces. In order to decrease time and space requirements of type analysis and to ensure its termination, we suitably approximate the behaviour of OOPNs. The price which we pay for this is the fact that the sets of the types of tokens about which we are informed that they can get into the particular places can be bigger than in reality. However, it is a safe approximation and the obtained results can still be quite useful. 22
We have proposed two approaches to type analysis in OOPNs — the socalled static and dynamic type analysis. Both methods work with symbolically represented markings and events which do not contain concrete data values but the corresponding types only. Accordingly, we do not perform classical trivial computations in guards of transitions and ports or in actions of transitions. Instead, we only derive the types of the involved variables. Next, the multiplicities of elements in initial markings and arc expressions are ignored. Moreover, we do not remove types symbolically representing some tokens once they get into a place. The main difference between static and dynamic type analysis consists in working with object and net instances: the dynamic one distinguishes (in a restricted way) different object and net instances while the static one does not. Thus, the dynamic type analysis is more exact but more complicated and slower than the static one.
Parallel State Space Generator The second approach to analysis of OOPNs we deal with is based on state space generation and exploration. The main problem of such methods is the so-called state space explosion problem — the number of states grows exponentially with the size of the model. Thus, it is difficult or practically impossible to apply these methods directly to large systems. We can identify two main approaches for dealing with the problem. The first class of these methods consists in sophisticated generating and exploring state spaces while the second one exploits more powerful computers. In this thesis, we have decided to adapt the parallel reasoning for OOPNs. We have developed a parallel state space generator on architectures with shared memory using the Java programming language and the JOMP tool. Let us note that the methods we have proposed here are usable even outside the domain of OOPNs. In the parallel algorithm, we exploit specific optimization techniques in order to achieve good work sharing among threads with as few synchronization as possible. They include synchronized access to a divided hash table, virtual threading, indirect storage of markings, etc. Using all these optimizations, we have reached parallel speedups up to 3.3 using 16 processors on the Sun Fire 15k server and speedups up to 2.3 using 4 processors on the Sun Enterprise 450 server. Moreover, the work distribution among particular threads is fine. The main problem that prevents us to achieve an even better parallel speedup is memory management system (especially garbage collecting) due to the memory operations being performed sequentially. A possible approach to this problem is to implement an user-specific memory management system like in [1], to reduce the number of dynamically created objects, or to use the proposed algorithm for less dynamic formalisms. 23
