VMStateImpl.mesa
Copyright © 1984 by Xerox Corporation. All rights reserved.
Russ Atkinson on June 8, 1984 7:36:31 pm PDT
Bob Hagmann on May 4, 1984 1:24:49 pm PDT
DIRECTORY
BootFileChanges
USING [
GetPageValue, IsVacant, PageStateFromFlags, PageValue, SetPageFlags, SetPageValue],
PrincOps USING [flagsNone, flagsVacant, PageFlags, PageState],
PrincOpsUtils
USING [
DisableInterrupts, EnableInterrupts],
ProcessorFaceExtras USING [firstSpecialRealPage, specialRealPages],
VMBacking USING [BriefPageState],
VMBackingChanges USING [],
VMInternal
USING [
AddToFreeList, AllocCount, Crash, DataState, GetVMMap, InitializeTables, InOut, Interval, Outcome, PageCount, PageNumber, PageState, RealPageNumber, RMMapEntry, RMMapEntries, RMEntryPointer, SetVMMap, SpecialMemoryOutcome, VMMapEntry, VMPartition],
VMSideDoor USING [vmPages],
VMStatistics USING [];
VMStateImpl:
MONITOR
LOCKS vmStateLock
IMPORTS BootFileChanges, PrincOpsUtils, ProcessorFaceExtras, VMInternal, VMSideDoor
EXPORTS VMBacking, VMBackingChanges, VMInternal, VMStatistics
SHARES VMInternal =
BEGIN
OPEN VMInternal;
Notes on the implementation:
The representation of the mapping from virtual page number to its associated PageState is partitioned into two pieces. A portion called the VM map is used for virtual memory pages that do not have an associated real memory page. A portion called the RM map is used for virtual memory pages that have an associated real memory page. (The RM map also holds other information, as will be discussed shortly.) Thus, to locate the PageState for a given (virtual) page, one first consults the hardware PageMap. If the flags say "vacant", the PageState is stored in the VM map; otherwise, it is stored in the RM map.
The representation of information in the VM map can be considerably optimized. First, PageState.hasRealMemory is implicitly FALSE and PageState.pinCount isn't meaningful. Thus, only PageState.readOnly and PageState.dataState need to be explicitly represented, requiring 3 bits per page. Second, we can use a trick that relies on the hardware implementation of the PageMap on all of the machines of interest (Dolphin, Dorado, Dandelion). Although the PrincOps specifies that if both dirty and write-protected are TRUE (indicating "vacant"), the real page number is undefined, the hardware does not enforce this restriction and is capable of retaining a few bits of information (<= 12) in what would otherwise be the real page number. This is simply because the map is implemented as a table lookup in a memory at least 16 bits wide of which at most 4 are used for flags. The VM map can therefore be comfortably stored in the available memory of the PageMap.
If RMEntry.rmState is "reclaimable", the real memory is available for reclamation by the real memory allocator (if it does so, it uses the "virtual" field to set the PageMap entry to "vacant"). If RMEntry.rmState is "pinned", the real memory allocator is prohibited from reclaiming this page. Note that the RMMap does not encode the virtual memory location of pinned real memory. This is not necessary, since the operation that changes rmState from "pinned" to "reclaimable" (Unpin) supplies the necessary PageNumber. Furthermore, this representation permits the reservation of specific real memory without necessarily associating it with virtual memory, a convenience in dealing with the Dandelion's display memory. If the needsBackingStoreWrite Boolean is TRUE, the bits in this page of real memory are known not to be present on backing storage. The "or" of needsBackingStoreWrite and the PageMap "dirty" bit is used to decide if the page must be written out as part of reclaiming it (see the AllocateForSwapIn and ConsiderCleaning procedures, below). The dataState field in an RMMap entry should never be "none", but may be "undefined" (implying "killed"). Finally, if RMEntry.rmState is "free", the "next" field is used to chain unallocated real memory pages together. This provides the real memory allocator with a list of prime candidates for allocation.
All of the procedures in this interface share a monitor that protects the RM map, VM map, and PageMap. AllocateRealMemoryInternal needs to be available to the frame fault handler (via AllocateForLocalFrames) and therefore must be a coroutine (AllocateRealMemoryInternal) with its two callers, AllocateForLocalFrames and AllocateForSwapIn, entering the monitor to ensure mutual exclusion. To avoid possible recursion in frame fault handling, AllocateRealMemoryInternal must not call any procedures. To avoid deadlock, therefore, all other procedures that enter the monitor must not call procedures either.
A note on checkout/checkin:
This is not a general purpose facility. It is intended to permit parellelism between the VM operations that do not require I/O and those that do (SwapIn, Clean). Thus, a page can only be checked out when its hardware map entry says "vacant" (the map is always in this state during swapper I/O). The procedures below that implement non-I/O VM operations all test if the page in question is checked out and, if so, wait until it is checked in (releasing the monitor while they wait). Checkout occurs only as a part of AllocateForSwapIn and ConsiderCleaning, and checkin occurs only as a part of RelocateAfterSwapIn and MarkClean.
The following monitor lock is used to protect the data structures of this module. It is exported so that the inline procedures in the VMInternal interface (which logically belong to this implementation module) can use it.
vmStateLock: PUBLIC MONITORLOCK;
The following global variables are protected by vmStateLock.
freeList: PUBLIC RealPageNumber;
freePages: PUBLIC INT ← 0;
rmMap: PUBLIC LONG POINTER TO RMMapEntries;
lastRealPage:
PUBLIC RealPageNumber;
index of last entry in rmMap
cleaningRover:
PUBLIC RealPageNumber ← RealPageNumber.
FIRST;
rover for GetCleaningCandidate
checkIn: PUBLIC CONDITION ← [timeout: 0];
The following constant is useful in various places
vacantEntry: VMMapEntry = [
state: BootFileChanges.PageStateFromFlags[PrincOps.flagsVacant],
body: out[
checkedOut: FALSE,
readOnly: FALSE,
dataState: undefined
]
];
Exports to VMStatistics
rmCleanPasses: PUBLIC INT ← 0;
readOnlyPages: PUBLIC INT ← 0;
pinnedPages, trappedPages: PUBLIC INT ← 0;
checkoutConflicts: PUBLIC INT ← 0;
VirtualAllocation:
PUBLIC
PROC [partition: VMPartition]
RETURNS [pagesAllocated, pagesFreed, pagesInPartition: PageCount] = {
RETURN[
pagesAllocated: allocCounts[partition].pagesAllocated,
pagesFreed: allocCounts[partition].pagesFreed,
pagesInPartition: partitions[partition].count
]
};
Exports to VMBackingChanges
StateFromPageValue:
PUBLIC
SAFE
PROC [map: BootFileChanges.PageValue]
RETURNS [VMBacking.BriefPageState] = TRUSTED {
The following works even if we are presented with a non-vacant map entry, but Andrew assures me that we won't!
vmEntry: VMMapEntry ← [
state: map.state,
body: in[real: map.real]
];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out =>
RETURN[
SELECT vmE.dataState
FROM
none => free,
undefined => killed,
ENDCASE => active
];
in => RETURN[active];
ENDCASE => ERROR;
};
Exports to VMBacking
RecoverRealMemory:
PUBLIC
PROC = {
See comment in the interface for a description of this crock. It completely trashes the virtual memory abstraction, except for those pages that already have real memory.
vmPage: PageNumber ← 0;
firstSpecialReal: RealPageNumber = ProcessorFaceExtras.firstSpecialRealPage;
countSpecialReal: PageCount = ProcessorFaceExtras.specialRealPages;
THROUGH [0..freePages)
DO
realPage: RealPageNumber = freeList;
UNTIL BootFileChanges.IsVacant[vmPage] DO vmPage ← vmPage.SUCC; ENDLOOP;
BootFileChanges.SetPageValue[
vmPage, [BootFileChanges.PageStateFromFlags[PrincOps.flagsNone], realPage]];
vmPage ← vmPage.SUCC;
WITH rmMap[realPage]
SELECT
FROM
rmE: free RMMapEntry => freeList ← rmE.next;
ENDCASE => Crash[];
ENDLOOP;
IF countSpecialReal > 0
THEN
FOR vmPage
IN [0..VMSideDoor.vmPages)
DO
state: PrincOps.PageState;
real: RealPageNumber;
[state, real] ← BootFileChanges.GetPageValue[vmPage].pv;
IF state.flags ~= PrincOps.flagsVacant
AND
real IN [firstSpecialReal..firstSpecialReal+countSpecialReal) THEN
BootFileChanges.SetPageFlags[vmPage, 0, PrincOps.flagsVacant];
ENDLOOP;
};
Exports to VMInternal
Virtual Memory Allocation
partitions: PUBLIC ARRAY VMPartition OF Interval;
--*stats*-- allocCounts: PUBLIC ARRAY VMPartition OF AllocCount ← ALL[[0, 0, 0, 0]];
Real Memory Allocation
Unpin:
PUBLIC ENTRY
PROC [vmPage: PageNumber]
RETURNS [outcome: Outcome ← ok] = {
vmEntry: VMMapEntry = GetCheckedInVMMap[vmPage].vmEntry;
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
in => {
rmE: RMEntryPointer = @rmMap[vmE.real];
WITH rmE: rmE
SELECT
FROM
free => Crash[];
reclaimable => NULL;
pinned =>
Perhaps we should complain if rmE.pinReason ~= normal?
IF rmE.pinReason = normal
THEN
SELECT rmE.pinCount
FROM
0 => Crash[];
1 => {
rmMap[vmE.real].body ← reclaimable[virtual: vmPage];
--*stats*-- pinnedPages ← pinnedPages.PRED;
};
ENDCASE =>
rmE.pinCount ← rmE.pinCount - 1;
ENDCASE;
};
out => IF vmE.dataState = none THEN outcome ← addressFault;
ENDCASE;
};
PrepareToAllocateSpecialRealMemory:
PUBLIC
ENTRY
PROC [
vmPage: PageNumber, buffer: PageNumber, special: PageNumber]
RETURNS [outcome: SpecialMemoryOutcome ← needsCopy] = {
vmEntry: VMMapEntry ← GetCheckedInVMMap[vmPage].vmEntry;
specialFlags: PrincOps.PageFlags ← PrincOps.flagsNone;
readOnly: BOOL ← FALSE;
specialEntry: in VMMapEntry;
newRME: RMMapEntry ← [
dataState: NULL, needsBackingStoreWrite: FALSE,
body: pinned[pinReason: specialRealPageInUse, pinCount: 0]
];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out => {
SELECT (newRME.dataState ← vmE.dataState)
FROM
none => RETURN[addressFault];
undefined => outcome ← noTransfer;
ENDCASE => outcome ← needsIO;
readOnly ← vmE.readOnly;
};
in => {
WITH rmE: rmMap[vmE.real]
SELECT
FROM
free => Crash[];
reclaimable => {
SELECT (newRME.dataState ← rmE.dataState)
FROM
none => Crash[];
undefined =>
outcome ← IF vmE.state.flags.dirty THEN needsCopy ELSE noTransfer;
ENDCASE => outcome ← needsCopy;
newRME.needsBackingStoreWrite ← rmE.needsBackingStoreWrite;
};
pinned => RETURN[badParameter]; -- either already special or pinned
ENDCASE;
specialFlags ← vmE.state.flags;
readOnly ← specialFlags.readonly;
specialFlags.readonly ← FALSE;
};
ENDCASE;
specialEntry ← [
state: BootFileChanges.PageStateFromFlags[specialFlags],
body: in[real: NULL]
];
IF ~([realPage: specialEntry.real] ← AllocateSpecialPage[newRME]).ok
THEN
RETURN[noMemory];
SetVMMap[vmPage, [
state: BootFileChanges.PageStateFromFlags[PrincOps.flagsVacant],
body: out[checkedOut: TRUE, readOnly: readOnly, dataState: newRME.dataState]
]];
SetVMMap[buffer, vmEntry];
SetVMMap[special, specialEntry];
};
FinishAllocateSpecialRealMemory:
PUBLIC
ENTRY
PROC [
vmPage: PageNumber, buffer: PageNumber, special: PageNumber, worked: BOOL] = {
specialEntry: VMMapEntry ← GetVMMap[special];
vmEntry: VMMapEntry = GetVMMap[vmPage];
readOnly: BOOL;
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out => readOnly ← vmE.readOnly;
ENDCASE => Crash[];
WITH specialE: specialEntry
SELECT InOut[specialEntry]
FROM
in =>
IF worked
THEN {
bufferEntry: VMMapEntry = GetVMMap[buffer];
WITH bE: bufferEntry
SELECT InOut[bufferEntry]
FROM
in => AddToFreeList[bE.real];
ENDCASE;
The following implicitly checks in vmPage.
specialE.state.flags.readonly ← readOnly;
SetVMMap[vmPage, specialE];
}
ELSE {
bufferEntry: VMMapEntry = GetVMMap[buffer];
The following implicitly checks in vmPage.
SetVMMap[vmPage, bufferEntry];
FreeSpecialPage[specialE.real];
};
out => Crash[];
ENDCASE;
BROADCAST checkIn;
Now we make the swap buffer pages vacant.
SetVMMap[buffer, vacantEntry];
SetVMMap[special, vacantEntry];
};
PrepareToReleaseSpecialRealMemory:
PUBLIC
ENTRY
PROC [
vmPage: PageNumber, special: PageNumber]
RETURNS [outcome: SpecialMemoryOutcome] = {
vmEntry: VMMapEntry ← GetCheckedInVMMap[vmPage].vmEntry;
checkedEntry: out VMMapEntry ← [
state: BootFileChanges.PageStateFromFlags[PrincOps.flagsVacant],
body: out[checkedOut: TRUE, readOnly: vmEntry.state.flags.readonly, dataState: NULL]
];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out => RETURN[IF vmE.dataState = none THEN addressFault ELSE badParameter];
in =>
WITH rmE: rmMap[vmE.real]
SELECT
FROM
pinned => {
IF rmE.pinCount > 0 THEN RETURN[badParameter];
checkedEntry.dataState ← rmE.dataState;
Need to set this to keep from having none in the data state (sigh).
outcome ←
IF rmE.dataState = undefined
AND ~vmE.state.flags.dirty
THEN noTransfer ELSE needsIO;
};
ENDCASE => RETURN[badParameter];
ENDCASE;
SetVMMap[vmPage, checkedEntry];
SetVMMap[special, vmEntry];
};
FinishReleaseSpecialRealMemory:
PUBLIC
ENTRY
PROC [
vmPage: PageNumber, special: PageNumber, worked: BOOL] = {
specialEntry: VMMapEntry = GetVMMap[special];
WITH specialE: specialEntry
SELECT InOut[specialEntry]
FROM
in =>
IF worked
THEN
WITH rmE: rmMap[specialE.real]
SELECT
FROM
pinned => {
IF rmE.pinReason ~= specialRealPageInUse THEN Crash[];
The following implicitly checks in vmPage.
SetVMMap[vmPage, [
state: BootFileChanges.PageStateFromFlags[PrincOps.flagsVacant],
body: out[
checkedOut: FALSE,
readOnly: specialE.state.flags.readonly,
dataState: rmE.dataState
]
]];
FreeSpecialPage[specialE.real];
};
ENDCASE => Crash[]
ELSE
The following implicitly checks in vmPage.
SetVMMap[vmPage, specialEntry];
out => Crash[];
ENDCASE;
BROADCAST checkIn;
SetVMMap[special, vacantEntry];
};
State Examination and Modification
State:
PUBLIC ENTRY
PROC [vmPage: PageNumber]
RETURNS [state: PageState] = {
It's OK to call GetVMMap instead of GetCheckedInVMMap, since we have the monitor lock and the data structures won't change under us.
vmEntry: VMMapEntry = GetVMMap[vmPage];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out => state ← [
dataState: vmE.dataState,
readOnly: vmE.readOnly,
hasRealMemory: FALSE,
needsCleaning: FALSE,
pinCount: 0
];
in => {
rmE: RMEntryPointer = @rmMap[vmE.real];
state ← [
dataState: IF vmE.state.flags.dirty THEN changed ELSE rmE.dataState,
readOnly: vmE.state.flags.readonly,
hasRealMemory: TRUE,
needsCleaning: vmE.state.flags.dirty OR rmE.needsBackingStoreWrite,
pinCount: WITH rmE^ SELECT FROM pinned => pinCount, ENDCASE => 0
];
};
ENDCASE;
};
SetDataState:
PUBLIC ENTRY
PROC [vmPage: PageNumber, dataState: DataState]
RETURNS [outcome: Outcome ← ok] = {
Note: If this procedure were made a coroutine (with an appropriate INLINE entry procedure), it could be invoked directly from the frame fault handler's "FlushLargeFrames" logic. Otherwise, that logic must reside in a separate process, which is allowed to call procedures and therefore take frame faults.
vmEntry: VMMapEntry ← GetCheckedInVMMap[vmPage].vmEntry;
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out =>
IF vmE.dataState = none THEN outcome ← addressFault
ELSE {vmE.dataState ← dataState; SetVMMap[vmPage, vmE]};
in => {
rmE: RMEntryPointer = @rmMap[vmE.real];
SELECT dataState
FROM
none => {
SetVMMap[vmPage,
[state: BootFileChanges.PageStateFromFlags[PrincOps.flagsVacant],
body: out[checkedOut: FALSE, readOnly: FALSE, dataState: dataState]]
];
WITH rmE: rmE
SELECT
FROM
free => Crash[];
reclaimable => AddToFreeList[vmE.real];
pinned =>
IF rmE.pinReason = specialRealPageInUse THEN FreeSpecialPage[vmE.real]
ELSE AddToFreeList[vmE.real];
ENDCASE;
};
undefined => {
WITH rmE: rmE
SELECT
FROM
free => Crash[];
reclaimable => {
SetVMMap[vmPage,
[state: BootFileChanges.PageStateFromFlags[PrincOps.flagsVacant],
body: out[checkedOut: FALSE, readOnly: FALSE, dataState: dataState]]
];
AddToFreeList[vmE.real];
};
pinned => {
Strictly speaking, we should disable interrupts, reread the map, clear the dirty bit, and set the map before enabling interrupts. This will avoid losing the referenced bit. However, since the page is being killed, the referenced bit isn't very interesting now anyway.
vmE.state.flags.dirty ← rmE.needsBackingStoreWrite ← FALSE;
SetVMMap[vmPage, vmE];
rmE.dataState ← dataState;
};
ENDCASE;
};
unchanged => {
newEntry: VMMapEntry;
We must do the following atomically to avoid losing the referenced bit.
PrincOpsUtils.DisableInterrupts[];
newEntry ← GetVMMap[vmPage];
WITH newE: newEntry
SELECT InOut[newEntry]
FROM
in =>
IF newE.state.flags.dirty
THEN {
rmE.needsBackingStoreWrite ← TRUE;
newE.state.flags.dirty ← FALSE;
SetVMMap[vmPage, newE];
};
out => Crash[];
ENDCASE;
PrincOpsUtils.EnableInterrupts[];
rmE.dataState ← dataState;
};
changed => rmE.dataState ← dataState;
ENDCASE;
};
ENDCASE;
};
ReadOnly <==> ReadWrite
MakeReadOnly:
PUBLIC ENTRY PROC [vmPage: PageNumber]
RETURNS [outcome: Outcome ← ok] = {
Interrupts must be disabled if the map entry says present, so that the test for "dirty" and subsequent resetting of "dirty" are atomic. Interrupts need not be disabled if the map entry says "vacant", but it doesn't hurt, since we spend minimal time in that state and it simplifies the code.
vmEntry: VMMapEntry ← GetCheckedInVMMap[vmPage].vmEntry;
PrincOpsUtils.DisableInterrupts[];
vmEntry ← GetVMMap[vmPage]; -- reread map to ensure atomicity
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out =>
IF vmE.dataState = none THEN outcome ← addressFault
ELSE
IF ~vmE.readOnly
THEN {
vmE.readOnly ← TRUE;
SetVMMap[vmPage, vmE];
--*stats*-- readOnlyPages ← readOnlyPages.SUCC;
};
in =>
IF ~vmE.state.flags.readonly
THEN {
IF vmE.state.flags.dirty
THEN {
rmMap[vmE.real].needsBackingStoreWrite ← TRUE;
vmE.state.flags.dirty ← FALSE;
rmMap[vmE.real].dataState ← changed;
};
vmE.state.flags.readonly ← TRUE;
SetVMMap[vmPage, vmE];
--*stats*-- readOnlyPages ← readOnlyPages.SUCC;
};
ENDCASE;
PrincOpsUtils.EnableInterrupts[];
};
MakeReadWrite:
PUBLIC ENTRY PROC [vmPage: PageNumber]
RETURNS [outcome: Outcome ← ok] = {
Interrupts must be disabled if the map entry says present, so that the resetting of "readonly" is atomic (otherwise, the "referenced" bit might be lost). Interrupts need not be disabled if the map entry says "vacant", but it doesn't hurt, since we spend minimal time in that state and it simplifies the code.
vmEntry: VMMapEntry ← GetCheckedInVMMap[vmPage].vmEntry;
PrincOpsUtils.DisableInterrupts[];
vmEntry ← GetVMMap[vmPage]; -- reread map to ensure atomicity
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
out =>
IF vmE.dataState = none THEN outcome ← addressFault
ELSE
IF vmE.readOnly
THEN {
vmE.readOnly ← FALSE;
SetVMMap[vmPage, vmE];
--*stats*-- readOnlyPages ← readOnlyPages.PRED;
};
in =>
IF vmE.state.flags.readonly
THEN {
vmE.state.flags.readonly ← FALSE;
SetVMMap[vmPage, vmE];
--*stats*-- readOnlyPages ← readOnlyPages.PRED;
};
ENDCASE;
PrincOpsUtils.EnableInterrupts[];
};
INTERNAL procedures
AllocateSpecialPage:
PROC [rmE: RMMapEntry]
RETURNS [ok: BOOL ← FALSE, realPage: RealPageNumber] = INLINE {
count: CARDINAL = ProcessorFaceExtras.specialRealPages;
realPage ← ProcessorFaceExtras.firstSpecialRealPage;
THROUGH [0..count)
DO
WITH rmE: rmMap[realPage]
SELECT
FROM
pinned => IF rmE.pinReason = specialRealPageAvailable THEN EXIT;
ENDCASE;
realPage ← realPage + 1;
REPEAT
FINISHED => RETURN;
ENDLOOP;
rmMap[realPage] ← rmE;
ok ← TRUE;
};
FreeSpecialPage:
PROC [realPage: RealPageNumber] =
INLINE {
WITH rmE: rmMap[realPage]
SELECT
FROM
pinned =>
IF rmE.pinReason = specialRealPageInUse THEN rmE.pinReason ← specialRealPageAvailable
ELSE Crash[];
ENDCASE => Crash[];
};
GetCheckedInVMMap:
INTERNAL
PROC [vmPage: PageNumber, dontWait:
BOOL ← FALSE]
RETURNS [vmEntry: VMMapEntry, success: BOOL ← TRUE] = INLINE {
firstTime: BOOL ← TRUE;
DO
vmEntry ← GetVMMap[vmPage];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
in => EXIT;
out =>
A note in VMInternal.VMMapEntry explains the following non-intuitive test.
IF ~vmE.checkedOut OR vmE.dataState = none THEN EXIT;
ENDCASE;
IF dontWait THEN {success← FALSE; EXIT};
--*stats*--
IF firstTime THEN {checkoutConflicts ← checkoutConflicts.SUCC; firstTime ← FALSE};
WAIT checkIn;
ENDLOOP;
};
Debugging procedures (Russ Atkinson, February 9, 1984)
VMPageInfo:
TYPE =
RECORD [
body:
SELECT inOut: *
FROM
in => [inEntry: VMMapEntry[in], entry: RMMapEntry],
out => [outEntry: VMMapEntry[out]],
none => NULL,
ENDCASE];
ShowVirtual:
PROC [vmPage: PageNumber]
RETURNS [VMPageInfo] = {
Given a virtual page, returns VMPageInfo which will contain the virtual page info and real page info for a legal page that is mapped in, or virtual page info for a legal page that is mapped out, or an indication of illegal page number.
IF vmPage
IN [0..VMSideDoor.vmPages)
THEN {
vmEntry: VMMapEntry ← GetVMMap[vmPage];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
in => RETURN [[in[vmE, rmMap[vmE.real]]]];
out => RETURN [[out[vmE]]];
ENDCASE;
};
RETURN [[none[]]];
};
ShowReal:
PROC [rmPage: RealPageNumber]
RETURNS [ok: BOOL ← FALSE, info: RMMapEntry] = {
Given a valid real page, show its state (ok = TRUE). If not valid, ok = FALSE.
info ← rmMap[0];
IF rmPage IN [0..lastRealPage] THEN {ok ← TRUE; info ← rmMap[rmPage]};
};
FindVirtual:
PROC
[rmPage: RealPageNumber, last: PageNumber ← 0]
RETURNS [vmPage: PageNumber ← 0, info: VMPageInfo] = {
Given a real page number, find the corresponding virtual page > last and report on its contents. If no such virtual page, a null result is returned. Note that we are reasonably sure that virtual page 0 is not mapped.
FOR vmPage
IN (last..VMSideDoor.vmPages)
DO
vmEntry: VMMapEntry ← GetVMMap[vmPage];
WITH vmE: vmEntry
SELECT InOut[vmEntry]
FROM
in => IF vmE.real = rmPage THEN {info ← [in[vmE, rmMap[vmE.real]]]; RETURN};
ENDCASE;
ENDLOOP;
info ← [none[]];
};
Initialization
InitializeTables[];
END.