[Javapathfinder-devel] SF.net SVN: javapathfinder: [723] trunk

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

Revision: 723
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=723&view=rev
Author:   pcmehlitz
Date:     2008-01-03 15:57:24 -0800 (Thu, 03 Jan 2008)

Log Message:
-----------
* the die-hard Verify.begin/endAtomic() is back! It's a different animal though - it works by short-cutting
the CG creation in the SchedulerFactory instances, and tolerates data CGs inside of atomic sections. It still
does not allow blocking inside an atomic section, but other than the old version reports this as a
deadlock, i.e. property violation, and not a silly JPF internal error (which it isn't - it's an
application problem).

* this required some reshuffle of the deadlock detection, which now mostly resides in ThreadList

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/KernelState.java
    trunk/src/gov/nasa/jpf/jvm/PrioritySchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadList.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
    trunk/test/gov/nasa/jpf/mc/TestAtomic.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/mc/TestAtomicJPF.java


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