NASA has just released Java PathFinder, a Java Virtual Machine that uses states to check all the possible ways a Java program can be executed, finding possible errors (NPEs or deadlocks, for example) in your code.
It then reports the entire execution path that leads to a defect. It's especially suited to find hard-to-test concurrency defects in multithreaded programs.
Currently, the software is limited to check for thread locks and uncaught exceptions, but it can be extended to check for other things, like race conditions. However, there is no support currently for java.awt, java.net and some of java.io.
The license is a custom license from NASA, NASA Open Source Agreement 1.3, but if the project was approved on Sourceforge it should follow the OSI conventions.
Do you see yourself using projects like this on your code, or is concurrency not an issue for J2EE applications?
-
NASA releases Java verification program as Opensource (15 messages)
- Posted by: Guillermo Castro
- Posted on: April 27 2005 13:25 EDT
Threaded Messages (15)
- NASA releases Java verification program as Opensource by Nils Kilden-Pedersen on April 27 2005 13:46 EDT
- NASA releases Java verification program as Opensource by Geert Bevin on April 27 2005 14:57 EDT
-
NASA releases Java verification program as Opensource by Cameron Purdy on April 27 2005 08:28 EDT
- NASA releases Java verification program as Opensource by han theman on April 28 2005 04:29 EDT
-
NASA releases Java verification program as Opensource by Cetin Karakus on April 28 2005 06:51 EDT
- Double checked locking by Ranjan Baisak on April 29 2005 04:50 EDT
- NASA releases Java verification program as Opensource by stu pot on April 28 2005 08:31 EDT
-
NASA releases Java verification program as Opensource by Cameron Purdy on April 27 2005 08:28 EDT
- Limit on number of lines of code that can be checked by Roy Tock on April 28 2005 08:37 EDT
- Limitations? Enhance it yourself... by Yoav Shapira on April 28 2005 10:52 EDT
- Hammurapii is quite good by Ruslan Zenin on April 29 2005 07:41 EDT
- NASA releases Java verification program as Opensource by Geert Bevin on April 27 2005 14:57 EDT
- FindBugs by Mark Garrison on April 28 2005 09:17 EDT
- rom The makers Of Apollo 13 And The Columbia Space Shuttle by M J on April 29 2005 12:12 EDT
- Still a cool job by Pete Haidinyak on May 02 2005 10:48 EDT
- No cut in pay necessary by Pete Kusnick on May 04 2005 08:16 EDT
- rom The makers Of Apollo 13 And The Columbia Space Shuttle by Cameron Purdy on May 02 2005 11:53 EDT
- Still a cool job by Pete Haidinyak on May 02 2005 10:48 EDT
-
NASA releases Java verification program as Opensource[ Go to top ]
- Posted by: Nils Kilden-Pedersen
- Posted on: April 27 2005 13:46 EDT
- in response to Guillermo Castro
Or do you think that concurrency issues are easy enough to detect and solve as things stand today?
You're kidding, right? -
NASA releases Java verification program as Opensource[ Go to top ]
- Posted by: Geert Bevin
- Posted on: April 27 2005 14:57 EDT
- in response to Nils Kilden-Pedersen
Sounded promising, so I tried it, but I got:
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames Research CenterJPF exception, terminating: class java.lang.NullPointerException: null
Hmm .. maybe I should use Java Pathfinder to find that NPE ;-) -
NASA releases Java verification program as Opensource[ Go to top ]
- Posted by: Cameron Purdy
- Posted on: April 27 2005 20:28 EDT
- in response to Geert Bevin
Sounded promising, so I tried it, but I got:
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames Research CenterJPF exception, terminating: class java.lang.NullPointerException: null
Hmm .. maybe I should use Java Pathfinder to find that NPE ;-)
That exception means that you passed the parameters in metric terms; try passing them using the imperial system (feet instead of meters).
Peace,
Cameron Purdy
Tangosol, Inc.
Coherence: Cluster your POJOs! -
NASA releases Java verification program as Opensource[ Go to top ]
- Posted by: han theman
- Posted on: April 28 2005 04:29 EDT
- in response to Cameron Purdy
That exception means that you passed the parameters in metric terms; try passing them using the imperial system (feet instead of meters).!
Bwhahahahahahahahahahaha. -
NASA releases Java verification program as Opensource[ Go to top ]
- Posted by: Cetin Karakus
- Posted on: April 28 2005 06:51 EDT
- in response to Cameron Purdy
that is really funny.
i wonder where these guys have their physics education?
Imperial College ? -
Double checked locking[ Go to top ]
- Posted by: Ranjan Baisak
- Posted on: April 29 2005 04:50 EDT
- in response to Cetin Karakus
[quote]Currently, the software is limited to check for thread locks and uncaught exceptions, but it can be extended to check for other things, like race conditions
[/quote]
Hmm...
I am not sure how it would impact singleton synchronize problem. Also re-ordering of variables during compile time.
Very much I am interested to implement singleton pattern using Partfinder.
However coming to NPE, it would be nice and appropriate to provide dynamic recovery during runtime. But during memory stack it would be rather more helpfull one.
regards,
Ranjan
ranjan_baisak@mentor.com -
NASA releases Java verification program as Opensource[ Go to top ]
- Posted by: stu pot
- Posted on: April 28 2005 08:31 EDT
- in response to Geert Bevin
wonder why spaceshuttle keeps crashing. DOH! -
Limit on number of lines of code that can be checked[ Go to top ]
- Posted by: Roy Tock
- Posted on: April 28 2005 08:37 EDT
- in response to Nils Kilden-Pedersen
From the Java PathFinder site, on the "What Can Be Checked by JPF" page:Another restriction is given by JPF's state storage requirements, which effectively limits the size of checkable applications to ~10kloc (depending on their internal structure) if no application and property specific abstractions are used.
The size restriction is pretty restrictive, and will prevent me from using this JVM very much. Too bad; the tool sounds useful otherwise. -
Limitations? Enhance it yourself...[ Go to top ]
- Posted by: Yoav Shapira
- Posted on: April 28 2005 10:52 EDT
- in response to Roy Tock
I'm sure the program size and other factors are limiting for various people, but now that NASA's open-sourced it, you can address those limitations yourself. Join the SourceForge project and start participating in discussions, sending in enhancements.
This could turn out to be a great product / project, if we give it traction as NASA probably intended by open-sourcing it. -
Hammurapii is quite good[ Go to top ]
- Posted by: Ruslan Zenin
- Posted on: April 29 2005 07:41 EDT
- in response to Nils Kilden-Pedersen
I think I still stick with Hammurapi core review tool (http://www.hammurapi.org).
It gives pretty good code review reports and it is extendable.
See some examples of the review results:
http://www.hammurapi.org/review/report.html -
FindBugs[ Go to top ]
- Posted by: Mark Garrison
- Posted on: April 28 2005 09:17 EDT
- in response to Guillermo Castro
I think I'll stick with FindBugs for now, it finds all sorts of things. -
rom The makers Of Apollo 13 And The Columbia Space Shuttle[ Go to top ]
- Posted by: M J
- Posted on: April 29 2005 12:12 EDT
- in response to Guillermo Castro
Is anyone here old enough to remember when being an Astronaut seemed like a cool job. -
Still a cool job[ Go to top ]
- Posted by: Pete Haidinyak
- Posted on: May 02 2005 10:48 EDT
- in response to M J
I would have take a large cut in pay and move to Houston to work for NASA. It's still a kewl job. -
No cut in pay necessary[ Go to top ]
- Posted by: Pete Kusnick
- Posted on: May 04 2005 08:16 EDT
- in response to Pete Haidinyak
Between missions to the bank you can buy a engineering start up and co-pilot with N-Sync. I see no problem with being a programmer and an astronaut. Of course, you would have to be in better shape than it takes to jockey from a reclining chair while smoking a stogie. -
rom The makers Of Apollo 13 And The Columbia Space Shuttle[ Go to top ]
- Posted by: Cameron Purdy
- Posted on: May 02 2005 11:53 EDT
- in response to M J
Is anyone here old enough to remember when being an Astronaut seemed like a cool job.
It is a cool job ;-)
Peace,
Cameron Purdy
Tangosol, Inc.
Coherence: Cluster your POJOs!