<> <> <> <> DIRECTORY PrincOps USING [flagsNone, flagsVacant, PageFlags, PageState, PageValue, RealPageNumber], PrincOpsUtils USING [DisableInterrupts, EnableInterrupts], ProcessorFace USING [firstSpecialRealPage, specialRealPages], VMBacking USING [BriefPageState], VMInternal USING [AddToFreeList, AllocCount, Crash, DataState, freeList, freePages, GetPageValue, GetVMMap, InitializeTables, InOut, Interval, IsVacant, Outcome, PageCount, PageNumber, PageState, PageStateFromFlags, RMEntryPointer, rmMap, RMMapEntries, RMMapEntry, SetPageFlags, SetPageValue, SetVMMap, SpecialMemoryOutcome, VMMapEntry, VMPartition], VMSideDoor USING [vmPages], VMStatistics USING []; VMStateImpl: MONITOR LOCKS vmStateLock IMPORTS PrincOpsUtils, ProcessorFace, VMInternal, VMSideDoor EXPORTS VMBacking, VMInternal, VMStatistics SHARES VMInternal = BEGIN OPEN PrincOps, VMInternal; <<>> <> <<>> <> <<>> <> <<>> <> <<>> <> <<>> <> <> <> vmStateLock: PUBLIC MONITORLOCK; <> freeList: PUBLIC RealPageNumber; freePages: PUBLIC INT _ 0; rmMap: PUBLIC LONG POINTER TO RMMapEntries; lastRealPage: PUBLIC RealPageNumber; <> cleaningRover: PUBLIC RealPageNumber _ RealPageNumber.FIRST; <> checkIn: PUBLIC CONDITION _ [timeout: 0]; <> <<>> vacantEntry: VMMapEntry = [ state: VMInternal.PageStateFromFlags[PrincOps.flagsVacant], body: out[ checkedOut: FALSE, readOnly: FALSE, dataState: undefined ] ]; <<>> <> <<>> 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 ] }; <> <<>> StateFromPageValue: PUBLIC SAFE PROC [map: PrincOps.PageValue] RETURNS [VMBacking.BriefPageState] = TRUSTED { <> 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; }; <> <<>> RecoverRealMemory: PUBLIC PROC = { <> vmPage: PageNumber _ 0; firstSpecialReal: RealPageNumber = ProcessorFace.firstSpecialRealPage; countSpecialReal: PageCount = ProcessorFace.specialRealPages; THROUGH [0..freePages) DO realPage: RealPageNumber = freeList; UNTIL VMInternal.IsVacant[vmPage] DO vmPage _ vmPage.SUCC; ENDLOOP; VMInternal.SetPageValue[ vmPage, [VMInternal.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] _ VMInternal.GetPageValue[vmPage].pv; IF state.flags ~= PrincOps.flagsVacant AND real IN [firstSpecialReal..firstSpecialReal+countSpecialReal) THEN VMInternal.SetPageFlags[vmPage, 0, PrincOps.flagsVacant]; ENDLOOP; }; <<>> <> <<>> <> <<>> partitions: PUBLIC ARRAY VMPartition OF Interval; <<>> --*stats*-- allocCounts: PUBLIC ARRAY VMPartition OF AllocCount _ ALL[[0, 0, 0, 0]]; <> 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 => <> 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: VMInternal.PageStateFromFlags[specialFlags], body: in[real: NULL] ]; IF ~([realPage: specialEntry.real] _ AllocateSpecialPage[newRME]).ok THEN RETURN[noMemory]; SetVMMap[vmPage, [ state: VMInternal.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; <> specialE.state.flags.readonly _ readOnly; SetVMMap[vmPage, specialE]; } ELSE { bufferEntry: VMMapEntry = GetVMMap[buffer]; <> SetVMMap[vmPage, bufferEntry]; FreeSpecialPage[specialE.real]; }; out => Crash[]; ENDCASE; BROADCAST checkIn; <> 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: VMInternal.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; <> 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[]; <> SetVMMap[vmPage, [ state: VMInternal.PageStateFromFlags[PrincOps.flagsVacant], body: out[ checkedOut: FALSE, readOnly: specialE.state.flags.readonly, dataState: rmE.dataState ] ]]; FreeSpecialPage[specialE.real]; }; ENDCASE => Crash[] ELSE <> SetVMMap[vmPage, specialEntry]; out => Crash[]; ENDCASE; BROADCAST checkIn; SetVMMap[special, vacantEntry]; }; <<>> <> State: PUBLIC ENTRY PROC [vmPage: PageNumber] RETURNS [state: PageState] = { <> 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] = { <> vmEntry: VMMapEntry _ GetCheckedInVMMap[vmPage].vmEntry; WITH vmE: vmEntry SELECT InOut[vmEntry] FROM out => IF vmE.dataState = none THEN outcome _ addressFault ELSE { IF ~(dataState = unchanged AND vmE.dataState = undefined) THEN { -- pages that are "undefined" are not modified to "unchanged". This is necessary to run without a backing file and is a slight optimization. vmE.dataState _ dataState; SetVMMap[vmPage, vmE]; }; }; in => { rmE: RMEntryPointer = @rmMap[vmE.real]; SELECT dataState FROM none => { SetVMMap[vmPage, [state: VMInternal.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: VMInternal.PageStateFromFlags[PrincOps.flagsVacant], body: out[checkedOut: FALSE, readOnly: FALSE, dataState: dataState]] ]; AddToFreeList[vmE.real]; }; pinned => { <> vmE.state.flags.dirty _ rmE.needsBackingStoreWrite _ FALSE; SetVMMap[vmPage, vmE]; rmE.dataState _ dataState; }; ENDCASE; }; unchanged => { newEntry: VMMapEntry; <> 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; }; < ReadWrite>> MakeReadOnly: PUBLIC ENTRY PROC [vmPage: PageNumber] RETURNS [outcome: Outcome _ ok] = { <> 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] = { <> 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[]; }; <<>> <> AllocateSpecialPage: PROC [rmE: RMMapEntry] RETURNS [ok: BOOL _ FALSE, realPage: RealPageNumber] = INLINE { count: CARDINAL = ProcessorFace.specialRealPages; realPage _ ProcessorFace.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 => <> 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; }; <> 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] = { <> 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] = { <> 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] = { < 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[]]; }; <<>> <> <<>> InitializeTables[]; <<>> END. <> <> <<>>