Types
FinalizationState: TYPE ~ Finalize.FinalizationState;
Handle: TYPE ~ REF FinalizableObject;
FinalizableObject:
PUBLIC
TYPE ~
WORD32
MACHINE
DEPENDENT
RECORD [
--the four first words are exactly as required by garbage collector
word1(0): CARD32,
word2(1): CARD32,
finalizationQueue(2): FinalizationQueue,
next(3): Handle,
--further fields are unknown to the garbage collector
clientData(4): REF
];
FinalizationQueue: TYPE ~ REF FinalizationQueueRep;
FinalizationQueueRep:
PUBLIC
TYPE ~
WORD32
MACHINE
DEPENDENT
RECORD [
head(0): Handle,
tail(1): Handle,
nonempty(2): CONDITION
];
IsHandle:
PUBLIC PROC [x:
REF]
RETURNS [
BOOL] = {
RETURN [ISTYPE [x, REF FinalizableObject]]
};
NarrowHandle:
PUBLIC
PROC [x:
REF]
RETURNS [Handle] = {
RETURN [NARROW [x, REF FinalizableObject]]
};
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] ];
};
XRFQNextNoAbort: PROC [fq: FinalizationQueue] RETURNS[handle: Handle] ~ TRUSTED MACHINE CODE { "XR𡤏QNextNoAbort" };
FQNextNoAbort:
PUBLIC
PROC [fq: FinalizationQueue]
RETURNS[handle: Handle] ~ {
RETURN [ XRFQNextNoAbort[fq] ];
};
FQNext:
PUBLIC
PROC [fq: FinalizationQueue]
RETURNS[handle: Handle ¬
NIL] ~ {
handle ¬ XRFQNextNoAbort[fq];
IF handle = NIL THEN ERROR ABORTED;
};
Object Finalization
EnableFinalization:
PUBLIC
PROC [object:
REF, fq: FinalizationQueue, clientData:
REF ¬
NIL]
RETURNS [handle: Handle] ~ {
XREnableFinalization: PROC [object: REF, fq: FinalizationQueue, handle: Handle] ~ TRUSTED MACHINE CODE { "XR𡤎nableFinalization" };
handle ¬ NEW[ FinalizableObject ¬ [0, 0, fq, NIL, clientData]];
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] ];
};
GetClientData:
PUBLIC
PROC [handle: Handle]
RETURNS [
REF] ~ {
RETURN[ handle.clientData ];
};