[Javapathfinder-svn] SF.net SVN: javapathfinder:[1169] trunk

[<pcm...@us...>]

Revision: 1169
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1169&view=rev
Author:   pcmehlitz
Date:     2009-02-12 04:04:24 +0000 (Thu, 12 Feb 2009)

Log Message:
-----------
* rework of the FieldLockInfo mechanism - this came up because of some examples where JPF didn't find races in very simple programs. It turned out that the simplicity was the problem: if JPF comes up with a 'protected' StatisticFieldLockInfo assumption, but the related object gets recycled along this path before we ever hit a path that violates the assumption, we don't notice. Ideally, StatisticFieldLockInfos should be search-global, but since neither ElementInfo nor their reference values are guaranteed to be invariant, we hardly can enforce this over a GC.

* there now is a 'pindown' option to avoid GCing objects that have 'protected' StatisticFieldLockInfo assumptions, so that we can at least get subsequent warnings

* we now have a factory for FieldLockInfo instantiation

* consequently, the whole StatisticFieldLockInfo stuff is now in StatisticFieldLockInfoFactory
 
* since we have a real factory now, we can instantiate after the first lock protection, saving both checks *and* FieldLockInfo instances
 
* field attributes (previously used for filtering) have been moved over to the (almost abandoned) DefaultAttributor, since it's much more effective to check at class load time 

* the filtering has changed: we can specify field names that are never supposed to be scheduling relevant (library classes), and we can specify field names that should always break transitions if the object is shared (even if vm.por.sync_detection is on and there are locks)

* slight change in Area.remove() - we first ask the object via ElementInfo.recycle() if it is willing to leave this world. This is an implicit pindown, so be careful. There is a symmetric ElementInfo.resurrect() which can be used to restore volatile info that is not part of the state storage

The refactored system is more sound, but can still miss races if not configured properly. The configuration is now more conservative and orthogonal, but still confusing:

  +vm.por.fli_factory.class - the factory class name for FieldLockInfo creation

  +vm.por.field_boundaries.never - never break on these field name patterns (e.g. java.*)
  +vm.por.field_boundaries.break - always break on these patterns if the object is shared (e.g. for app class fields that caused assumption warnings)

  +vm.por.sync_detection.pindown - don't GC an object that has a 'protected' StatisticFieldLockInfo assumption
  +vm.por.sync_detection.agressive - look for supposed to be related locks (field owner, sibling field etc.) - THIS IS PRONE TO MISSING RACES IN SIMPLE EXAMPLES (hence it's now turned off by default)
  
The problem with this is that some of the options only make sense in a vm.por.field_boundaries & vm.por.sync_detection context

Modified Paths:
--------------
    trunk/default.properties
    trunk/src/gov/nasa/jpf/jvm/Area.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
    trunk/src/gov/nasa/jpf/jvm/ConfigAttributor.java
    trunk/src/gov/nasa/jpf/jvm/DefaultAttributor.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldLockInfo.java
    trunk/src/gov/nasa/jpf/jvm/KernelState.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FieldInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java
    trunk/test/gov/nasa/jpf/mc/TestRace.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/jvm/FieldLockInfoFactory.java
    trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfoFactory.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/jvm/SingleFieldLockInfo.java
    trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfo.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.