gov.nasa.jpf.vm.serialize

Class TopFrameSerializer

java.lang.Object

gov.nasa.jpf.vm.AbstractSerializer

gov.nasa.jpf.vm.serialize.FilteringSerializer

gov.nasa.jpf.vm.serialize.CFSerializer

gov.nasa.jpf.vm.serialize.TopFrameSerializer

All Implemented Interfaces:

Processor<ElementInfo>, KernelState.ChangeListener, ReferenceProcessor, StateSerializer

public class TopFrameSerializer
extends CFSerializer

even more aggressive under-approximation than AdaptiveSerializer. This one only looks at the top frame of each thread, and only serializes objects referenced from there. It ignores static fields and deeper heap objects that are not directly referenced. While this seems too aggressive, it actually finds a lot of concurrency defects in real world applications. This is esp. true if there are a lot of field access CGs, i.e. shared objects. In this case, the TopFrameSerializer can behave an order of magnitude better than CFSerializer

Field Summary

Fields inherited from class gov.nasa.jpf.vm.serialize.FilteringSerializer

buf, filter, refQueue

Fields inherited from class gov.nasa.jpf.vm.AbstractSerializer

cached, ks, nativeStateHolders, vm

Constructor Summary

Constructors

Constructor and Description
TopFrameSerializer()

Method Summary

Modifier and Type	Method and Description
protected void	initReferenceQueue()
protected void	processReferenceQueue()
protected void	queueReference(ElementInfo ei)
protected void	serializeClassLoaders()
protected void	serializeStackFrames(ThreadInfo ti)

Methods inherited from class gov.nasa.jpf.vm.serialize.CFSerializer

getSerializedReferenceValue, processReference, serializeFrame, serializeStackFrames

Methods inherited from class gov.nasa.jpf.vm.serialize.FilteringSerializer

attach, computeStoringData, dumpData, getFramePolicy, getInstanceFilterMask, getInstanceRefMask, getStaticFilterMask, getStaticRefMask, process, processArrayFields, processNamedFields, serializeClass, serializeLockedObjects, serializeNativeStateHolder, serializeNativeStateHolders, serializeStatics, serializeThreadState, serializeThreadStates

Methods inherited from class gov.nasa.jpf.vm.AbstractSerializer

addNativeStateHolder, getCurrentStateVectorLength, getStoringData, kernelStateChanged

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

TopFrameSerializer

public TopFrameSerializer()

Method Detail

initReferenceQueue

protected void initReferenceQueue()

Overrides:

initReferenceQueue in class CFSerializer

serializeStackFrames

protected void serializeStackFrames(ThreadInfo ti)

Overrides:

serializeStackFrames in class FilteringSerializer

queueReference

protected void queueReference(ElementInfo ei)

Overrides:

queueReference in class CFSerializer

processReferenceQueue

protected void processReferenceQueue()

Overrides:

processReferenceQueue in class CFSerializer

serializeClassLoaders

protected void serializeClassLoaders()

Overrides:

serializeClassLoaders in class FilteringSerializer