bandera daisy

Information about bandera daisy

Published on January 3, 2008

Author: worm

Source: authorstream.com

Content

Model Checking Daisy Using The Bandera Tool-set :  Model Checking Daisy Using The Bandera Tool-set SAnToS Laboratory, Kansas State University, USA http://bandera.projects.cis.ksu.edu US Army Research Office (ARO) US National Science Foundation (NSF) US Department of Defense Advanced Research Projects Agency (DARPA) Boeing Honeywell Technology Center IBM Intel Lockheed Martin NASA Langley Rockwell-Collins ATC Sun Microsystems Support Todd Wallentine Edwin Rodríguez Robby Venkatesh Prasad Ranganath http://indus.projects.cis.ksu.edu http://bogor.projects.cis.ksu.edu http://spex.projects.cis.ksu.edu Research Context ¡ Bandera:  Research Context ¡ Bandera Aiming for robust tools open source, (ambitiously) commercial quality (or close to it) Trying to build on lessons learned experiences from the previous Bandera version, etc. Integration into development process ease of use and scalability most of the time, focus is on bug-finding rather than true verification SAnToS Laboratory, Kansas State University http://www.cis.ksu.edu/santos Bandera ¡ A tool-set to support Model Checking Java progs.:  Bandera ¡ A tool-set to support Model Checking Java progs. javac SUN jmlc IASTATE Soot MCGILL Slicer Abs J2B Bogor .bir aspectj … … Tool Development Framework Counter example Research Context ¡ Bogor:  Research Context ¡ Bogor Supporting model-checking of OO programs (Java, in particular) and designs of avionics system Open platform for research/experimentation take your favorite new idea, implement it in Bogor to try it out Teaching tool foundation of a tool/application-oriented course on model-checking some material already available; much more on the way Bogor – Software Model Checking Framework:  Bogor – Software Model Checking Framework Bogor – Direct support for OO software:  Bogor – Direct support for OO software unbounded dynamic creation of threads and objects automatic memory management (garbage collection) virtual methods, … …, exceptions, etc. supports virtually all of the Java language features thread & heap symmetry compact state representation partial order reduction techniques driven by object escape analysis locking information Extensive support for checking concurrent OO software Direct support for… Software targeted algorithms… Bogor – Eclipse-based Tool Components:  Tool Development Framework Bogor – Eclipse-based Tool Components Bogor – Domain Specific Model-Checking:  Bogor – Domain Specific Model-Checking Modeling language and Algorithms easily customized to different domains Model Checking Daisy:  Model Checking Daisy Experiences with Bandera Modeling Java library Bogor customization Slicing Properties ¡ Results Challenges The Bandera Tool-set ¡ Status:  The Bandera Tool-set ¡ Status javac jmlc Soot Slicer Abs J2B Bogor .bir … … Tool Development Framework Counter example javac SUN jmlc IASTATE Soot MCGILL aspectj The Bandera Tool-set ¡ Status:  The Bandera Tool-set ¡ Status javac jmlc Soot Slicer Abs J2B Bogor .bir aspectj … … Counter example Modeling Java Library:  Modeling Java Library Bandera does not currently model full Java standard library some of Java library classes were taken from the GNU Classpath library still needs to model native calls Daisy uses RandomAccessFile involving native calls temporary solution: modeled Petal by using a byte array Bogor Customizations:  Bogor Customizations Daisy uses the Mutex class to implement fine-grained locking the lock status is implemented by using the locked boolean field Bogor has PORs based on: escape analysis Locking Discipline/Eraser [Stoller00], etc. class Mutex { boolean locked; int id; public Mutex(int id) { this.id = id; this.locked = false; } synchronized void acq() { while (locked) { try { this.wait(); } catch (Exception e) { … } } locked = true; } synchronized void rel() { locked = false; this.notify(); } } Bogor Customizations:  Bogor Customizations Customized LD so it query locked field when collecting the set of locks held by the current executing thread (~ 10 LOC) class Mutex { boolean locked; int id; public Mutex(int id) { this.id = id; this.locked = false; } synchronized void acq() { while (locked) { try { this.wait(); } catch (Exception e) { … } } locked = true; } synchronized void rel() { locked = false; this.notify(); } } Slicing Daisy:  Slicing Daisy used Bandera Slicer (http://indus.projects.cis.ksu.edu) when checking for Deadlock reduced the number of states by 5% will be even greater if the actual Java runtime library is used Properties:  Properties Property 1: locking protocol Property 2: deadlock Property 3: race condition Property 4: pre-/post-conditions and performs ghost variable not translated -- JML relation Property 5: invariants invariant checked by adding assert in pre-/post- methods that modified them Property 6: not checked Property 1: Locking Protocol:  Property 1: Locking Protocol SLAM’s SLIC style added an owner field for thread identifier check locking protocol using owner class Mutex { … TID owner = \none; synchronized void acq() { assert locked => owner != \tid; while (locked) { try { this.wait(); } catch (Exception e) { … } } locked = true; owner = tid; } synchronized void rel() { assert locked && owner == \tid; locked = false; owner = \none; this.notify(); } } Property 3: Race Condition:  Property 3: Race Condition LD complains whenever a variable access is not property locked (open browser) LD found an access to the disk is not properly locked (can cause a race condition) Property 3: Race Condition:  Property 3: Race Condition *** LD violated by object of type: int wrap (-128, 127)[]*** Previous lock-set: [[email protected]] Current lock-set: [[email protected]] FSM MAIN at line 93, column 5 loc loc1: live {} when !(BogorJava.isInitialized(isi, "(|DaisyTest|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|DaisyTest|)")) goto loc1; when BogorJava.isInitialized(isi, "(|DaisyTest|)") invoke {|DaisyTest.main(java.lang.String[])|}() return; FSM {|DaisyTest.main(java.lang.String[])|} at line 0, column 0 loc loc14: live { [|r3|], [|r4|], [|r3|], [|r4|] } when !(BogorJava.isInitialized(isi, "(|daisy.Daisy|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|daisy.Daisy|)")) goto loc14; when BogorJava.isInitialized(isi, "(|daisy.Daisy|)") invoke {|daisy.Daisy.dumpDisk()|}() goto loc15; FSM {|daisy.Daisy.dumpDisk()|} at line 0, column 0 loc loc3: live { [|l0|], [|r0|] } [|r0|] := invoke {|daisy.Daisy.iget(long)|}([|l0|]) goto loc4; FSM {|daisy.Daisy.iget(long)|} at line 0, column 0 loc loc5: live { [|r1|], [|r1|], [|l0|] } when !(BogorJava.isInitialized(isi, "(|daisy.DaisyDisk|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|daisy.DaisyDisk|)")) goto loc5; when BogorJava.isInitialized(isi, "(|daisy.DaisyDisk|)") invoke {|daisy.DaisyDisk.readi(long,daisy.Inode)|}([|l0|], [|r1|]) goto loc6; FSM {|daisy.DaisyDisk.readi(long,daisy.Inode)|} at line 0, column 0 loc loc4: live { [|r0|], [|l0|], [|$l3|], [|r0|], [|l0|], [|$l2|] } when !(BogorJava.isInitialized(isi, "(|daisy.Petal|)")) invisible invoke runStaticInitializers(BogorJava.getStaticInitializers(isi, "(|daisy.Petal|)")) goto loc4; when BogorJava.isInitialized(isi, "(|daisy.Petal|)") [|$l3|] := invoke {|daisy.Petal.readLong(long)|}([|$l2|]) goto loc5; FSM {|daisy.Petal.readLong(long)|} at line 0, column 0 loc loc6: live { [|l1|], [|i2|], [|b3|], [|l0|] } [|b3|] := invoke {|daisy.Petal.read(long)|}([|$l5|]) goto loc7; FSM {|daisy.Petal.read(long)|} at line 0, column 0 loc loc8: live { [|$b3|] } do { [|$b3|] := [|$r1|][[|i1|]]; } goto loc9; Properties 4 - 5:  Properties 4 - 5 javac jmlc Soot Slicer … J2B Bogor .bir … … … Manual JML Found the following perform specification of DaisyDir.openDirectory violated: (\forall int i; 0 <= i && i < d.entries.length ==> d.entries[i] != null) Conclusion ¡ Challenges in Model Checking:  Conclusion ¡ Challenges in Model Checking Environments needs the right environment to uncover bugs Abstractions, etc. what kinds of abstractions can be used to reduce the search space? Modeling Java library (e.g., native calls)

Related presentations


Other presentations created by worm

EGYPT
26. 03. 2008
0 views

EGYPT

TNS GIPP
27. 09. 2007
0 views

TNS GIPP

icfascic dec01 J
09. 10. 2007
0 views

icfascic dec01 J

OgilvyOne
10. 10. 2007
0 views

OgilvyOne

06apr05
28. 11. 2007
0 views

06apr05

Sari
23. 11. 2007
0 views

Sari

Alternate Medicine
17. 12. 2007
0 views

Alternate Medicine

gwc2004 sin1
03. 12. 2007
0 views

gwc2004 sin1

suspensionbridges
30. 12. 2007
0 views

suspensionbridges

cablestaypresentation
01. 01. 2008
0 views

cablestaypresentation

Mioduszewski
15. 11. 2007
0 views

Mioduszewski

LNL 11nov06
14. 11. 2007
0 views

LNL 11nov06

MIR ISS
21. 11. 2007
0 views

MIR ISS

AnneRueth PP2
24. 02. 2008
0 views

AnneRueth PP2

SymChaffAAAI05
26. 02. 2008
0 views

SymChaffAAAI05

7 a
28. 02. 2008
0 views

7 a

classreunion
10. 03. 2008
0 views

classreunion

isc wt au i
14. 03. 2008
0 views

isc wt au i

Lew
18. 03. 2008
0 views

Lew

Mori
27. 03. 2008
0 views

Mori

Forum J
07. 04. 2008
0 views

Forum J

Presentation 02080482251
13. 04. 2008
0 views

Presentation 02080482251

IVI HF
21. 11. 2007
0 views

IVI HF

Withey presentation
31. 12. 2007
0 views

Withey presentation

mnesdecl
20. 11. 2007
0 views

mnesdecl

shortened version
01. 10. 2007
0 views

shortened version

esn 2004107832574530
01. 11. 2007
0 views

esn 2004107832574530

www2004 ohmukai
29. 12. 2007
0 views

www2004 ohmukai

EASD presentation 2004
28. 11. 2007
0 views

EASD presentation 2004

Pictorialtour
02. 10. 2007
0 views

Pictorialtour