bandera daisy

43 %
57 %
Information about bandera daisy
Entertainment

Published on January 3, 2008

Author: worm

Source: authorstream.com

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 <= 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)

Add a comment

Related presentations

Related pages

Daisy Bandera - YouTube

An active duty Marine surprises his sister on her wedding day. So thankful for the sacrifices military men and women make for our freedom everyday.
Read more

Daisy Bandera - Google+

Daisy Bandera. 24,113 views. About Posts Photos YouTube. Stream. Daisy Bandera commented on a video on YouTube. Shared publicly - 2014-07-18 . Awww ...
Read more

Daisy Bandera - Google Profile

Daisy Bandera hasn't shared anything on this page with you.
Read more

Relasyong Willie-Danita Paner tanggap na ni Daisy ...

I HAD a nice talk with our dear Mama Daisy Romualdez over the phone yesterday dahil tinawagan ko siya right after mabasa ko sa isang tabloid (not in this ...
Read more

Daisy “Marie” Pickett - The Bandera Bulletin: Obituaries

Daisy “Marie” Pickett passed peacefully into the arms of the Lord on February 27, 2014 at the age of 77. She was born on Nov. 18, 1936 in San Angelo to ...
Read more

daisy Banderas - Google+

daisy Banderas hasn't shared anything on this page with you.
Read more

Dixie Dude Ranch - Bandera Lodging, Vacations and ...

Dixie Dude Ranch in Bandera, Texas: 830-796-7771 or 1-800-375-9255. Home; Amenities. Amenities; Dining; Accommodations; Lodging Gallery; Swimming Pool ...
Read more

DAISY CALIL COM ANTONIO BANDERAS E DALI - YouTube

EM MADRID MARÇO DE 2010 ... This feature is not available right now. Please try again later.
Read more

Search :: LINE Webtoon

Slice of life. The Woes and Ah's of College Students. Daisy Bandera. grade 6.75. Slice of life. The Woe's and Ah's of College Students. Bandera Daisy ...
Read more