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: [record@177] Current lock-set: [record@762] 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 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)