Types
FinalizationState: TYPE ~ Finalization.FinalizationState;
Handle: TYPE ~ REF FinalizableObject;
FinalizableObject:
PUBLIC
TYPE ~
WORD32
MACHINE
DEPENDENT
RECORD [
word1(0): CARD32,
word2(1): CARD32,
finalizationQueue(2): FinalizationQueue,
next(3): Handle
];
FinalizationQueue: TYPE ~ REF FinalizationQueueRep;
FinalizationQueueRep:
PUBLIC
TYPE ~
WORD32 MACHINE DEPENDENT RECORD [
head(0): Handle,
tail(1): Handle,
nonempty(2): CONDITION
];
FQ Manipulation
NewFQ:
PUBLIC
PROC
RETURNS [FinalizationQueue] ~ {
XRNewFQ: PROC RETURNS [FinalizationQueue] ~ TRUSTED MACHINE CODE { "XR←NewFQ" };
RETURN[ XRNewFQ[] ];
};
FQEmpty:
PUBLIC
PROC [fq: FinalizationQueue]
RETURNS[
BOOL] ~ {
XRFQEmpty: PROC [fq: FinalizationQueue] RETURNS[BOOL] ~ TRUSTED MACHINE CODE { "XR𡤏QEmpty" };
RETURN [ XRFQEmpty[fq] ];
};
FQNextNoAbort:
PUBLIC
PROC [fq: FinalizationQueue]
RETURNS[handle: Handle] ~ {
XRFQNextNoAbort: PROC [fq: FinalizationQueue] RETURNS[handle: Handle] ~ TRUSTED MACHINE CODE { "XR𡤏QNextNoAbort" };
RETURN [ XRFQNextNoAbort[fq] ];
};
FQNext:
PUBLIC
PROC [fq: FinalizationQueue]
RETURNS[handle: Handle ¬
NIL] ~ {
XRFQNextNoAbort: PROC [fq: FinalizationQueue] RETURNS[handle: Handle] ~ TRUSTED MACHINE CODE { "XR𡤏QNextNoAbort" };
handle ¬ FQNextNoAbort[fq];
IF handle = NIL THEN ERROR ABORTED;
};
Object Finalization
EnableFinalization:
PUBLIC
PROC [object:
REF, fq: FinalizationQueue]
RETURNS [handle: Handle] ~ {
XREnableFinalization: PROC [object: REF, fq: FinalizationQueue, handle: Handle] ~ TRUSTED MACHINE CODE { "XR𡤎nableFinalization" };
handle ¬ NEW[ FinalizableObject ¬ [0, 0, fq, NIL]];
XREnableFinalization[object, fq, handle];
};
DisableFinalization:
PUBLIC
PROC [handle: Handle]
RETURNS [oldState: FinalizationState] ~ {
XRDisableFinalization: PROC [handle: Handle] RETURNS [oldState: FinalizationState] ~ TRUSTED MACHINE CODE { "XR𡤍isableFinalization" };
RETURN[ XRDisableFinalization[handle] ];
};
ReenableFinalization:
PUBLIC
PROC [handle: Handle, fq: FinalizationQueue]
RETURNS [oldState: FinalizationState] ~ {
XRReenableFinalization: PROC [handle: Handle, fq: FinalizationQueue] RETURNS [oldState: FinalizationState] ~ TRUSTED MACHINE CODE { "XR←ReenableFinalization" };
RETURN[ XRReenableFinalization[handle, fq] ];
};
GetFinalizationState:
PUBLIC
PROC [handle: Handle]
RETURNS [state: FinalizationState] ~ {
XRGetFinalizationState: PROC [handle: Handle] RETURNS [state: FinalizationState] ~ TRUSTED MACHINE CODE { "XR←GetFinalizationState" };
RETURN[ XRGetFinalizationState[handle] ];
};
HandleToObject:
PUBLIC
PROC [handle: Handle]
RETURNS [object:
REF] ~ {
XRHandleToObject: PROC [handle: Handle] RETURNS [object: REF] ~ TRUSTED MACHINE CODE { "XR←HandleToObject" };
RETURN[ XRHandleToObject[handle] ];
};