Mercurial > hg > Members > kono > jpf-core
view README @ 23:db918c531e6d
streamlined class init, which was a mixed case of registerClass()/initializeClass() and pushRequiredClinits(). Now it is a single initializeClass(ti) method which combines the previous initializeClass(), pushRequiredClinits() and pushClinit() methods. The reason for combining these is the forthcoming replacement of separately locked clinits from different DirectCallStackFrames with a single synthetic frame that calls clinits from nested synchronized blocks. This is required to model hotspot, which does cause deadlocks with concurrent init of classes that cause subclass init during their clinit executions.
| author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
|---|---|
| date | Wed, 15 Apr 2015 22:40:21 -0700 |
| parents | 61d41facf527 |
| children |
line wrap: on
line source
Java PathFinder README ====================== ========General Information about JPF =================== All the latest developments, changes, documentation can be found at: http://babelfish.arc.nasa.gov/trac/jpf/wiki ========Building and Installing ========================= If you are having problems installing and running JPF please look at the documentation on the wiki at: http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start A lot of the commonly problems during the install and build process have been documented on the wiki. Please make sure that the the issue you are running into is not addressed there; if is not then feel free to contact us at java-pathfinder@googlegroups.com ======Documentation====================================== There is a constant effort to update and add JPF documentation on the wiki. If you would like to contribute in that, please contact us at java-pathfinder@googlegroups.com Happy Verification -- the Java PathFinder team