gov.nasa.jpf.vm.serialize

Class CFSerializer

java.lang.Object

gov.nasa.jpf.vm.AbstractSerializer

gov.nasa.jpf.vm.serialize.FilteringSerializer

gov.nasa.jpf.vm.serialize.CFSerializer

All Implemented Interfaces:

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

Direct Known Subclasses:

AdaptiveSerializer, DebugCFSerializer, TopFrameSerializer

public class CFSerializer
extends FilteringSerializer

a FilteringSerializer that performs on-the-fly heap canonicalization to achieve heap symmetry. It does so by storing the order in which objects are referenced, not the reference values themselves. Use this serializer if the Heap implementation does not provide sufficient symmetry, i.e. reference values depend on the order of thread scheduling. Ad hoc heap symmetry is hard to achieve in the heap because of static initialization. Each time a thread loads a class all the static init (at least the class object and its fields) are associated with this thread, hence thread reference values depend on which classes are already loaded by other threads. Associating all allocations from inside of clinits to one address range doesn't help either because then this range will experience scheduling dependent orders. A hybrid approach in which only this segment is canonicalized might work, but it is questionable if the overhead is worth the effort.

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
CFSerializer()

Method Summary

Modifier and Type	Method and Description
protected int	getSerializedReferenceValue(ElementInfo ei)
protected void	initReferenceQueue()
void	processReference(int objref)
protected void	processReferenceQueue()
protected void	queueReference(ElementInfo ei)
protected void	serializeFrame(StackFrame frame) more generic, but less efficient because it can't use block operations protected void _serializeFrame(StackFrame frame){ buf.add(frame.getMethodInfo().getGlobalId()); buf.add(frame.getPC().getInstructionIndex()); int len = frame.getTopPos()+1; buf.add(len); // this looks like something we can push into the frame int[] slots = frame.getSlots(); for (int i = 0; i < len; i++) { if (frame.isReferenceSlot(i)) { processReference(slots[i]); } else { buf.add(slots[i]); } } }
protected void	serializeStackFrames()

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

attach, computeStoringData, dumpData, getFramePolicy, getInstanceFilterMask, getInstanceRefMask, getStaticFilterMask, getStaticRefMask, process, processArrayFields, processNamedFields, serializeClass, serializeClassLoaders, serializeLockedObjects, serializeNativeStateHolder, serializeNativeStateHolders, serializeStackFrames, 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

CFSerializer

public CFSerializer()

Method Detail

initReferenceQueue

protected void initReferenceQueue()

Overrides:

initReferenceQueue in class FilteringSerializer

queueReference

protected void queueReference(ElementInfo ei)

processReference

public void processReference(int objref)

Specified by:

processReference in interface ReferenceProcessor

Overrides:

processReference in class FilteringSerializer

serializeStackFrames

protected void serializeStackFrames()

Overrides:

serializeStackFrames in class FilteringSerializer

serializeFrame

protected void serializeFrame(StackFrame frame)

Description copied from class: FilteringSerializer

more generic, but less efficient because it can't use block operations protected void _serializeFrame(StackFrame frame){ buf.add(frame.getMethodInfo().getGlobalId()); buf.add(frame.getPC().getInstructionIndex()); int len = frame.getTopPos()+1; buf.add(len); // this looks like something we can push into the frame int[] slots = frame.getSlots(); for (int i = 0; i < len; i++) { if (frame.isReferenceSlot(i)) { processReference(slots[i]); } else { buf.add(slots[i]); } } }

Overrides:

serializeFrame in class FilteringSerializer

processReferenceQueue

protected void processReferenceQueue()

Overrides:

processReferenceQueue in class FilteringSerializer

getSerializedReferenceValue

protected int getSerializedReferenceValue(ElementInfo ei)

Overrides:

getSerializedReferenceValue in class FilteringSerializer