<> <> DIRECTORY Basics USING [BITAND, BITSHIFT, LongNumber], PrincOps USING [bytesPerPage, PageCount, PageNumber, wordsPerPage]; VM: CEDAR DEFINITIONS IMPORTS Basics = BEGIN <> <> PageNumber: TYPE = PrincOps.PageNumber; <> PageCount: TYPE = PrincOps.PageCount; <> <> <> Interval: TYPE = RECORD [page: PageNumber, count: PageCount]; nullInterval: Interval = [page: 0, count: 0]; <> <> <<>> PageState: TYPE = RECORD [ dataState: DataState, readOnly: BOOL, -- altered only by MakeReadOnly and MakeReadWrite hasRealMemory: BOOL, -- altered only by SwapIn and MakeUndefined needsCleaning: BOOL, -- a hint for clients of "Clean" pinCount: INT -- altered only by Pin and Unpin ]; DataState: TYPE = { none, undefined, unchanged, changed}; <> <> State: PROC [page: PageNumber] RETURNS [state: PageState]; <> SetDataState: PRIVATE UNSAFE PROC [interval: Interval, dataState: DataState]; <> <<>> <> <> <> VMPartition: TYPE = {lowCore, pda, mds, normalVM}; <> LogPageCount: TYPE = NAT[0..23--LogBase2[PageCount.LAST]-1--]; Allocate: PROC [count: PageCount, partition: VMPartition _ normalVM, subRange: Interval _ nullInterval, start: PageNumber _ 0, alignment: LogPageCount _ 0, in64K: BOOL _ FALSE] RETURNS [interval: Interval]; <<>> <> <<(1) for each page in "interval", State[page].dataState = none,>> <<(2) interval.count = count,>> <<(3) if subRange.count >= count, then "interval" is contained in "subRange",>> <<(4) interval.page MOD 2alignment is zero, and>> <<(5) if start is non-zero, then interval.page-start is minimal, and>> <<(6) if in64K is TRUE, then the interval does not cross a 64K word boundary.>> <> <> <> <<(1) for each page in "bestInterval", State[page].dataState = none,>> <<(2) bestInterval.count < count with count-bestInterval.count minimal, and>> <<(3) if subRange.count >= count, then "bestInterval" is contained in "subRange",>> <> <> CantAllocate: ERROR [bestInterval: Interval]; <> Free: UNSAFE PROC [interval: Interval] = TRUSTED INLINE {SetDataState[interval, none]}; <> <<>> <> <> SwapIn: UNSAFE PROC [interval: Interval, kill: BOOL _ FALSE, pin: BOOL _ FALSE, nextPage: PageNumber _ 0]; <> <> <> <> <> <> <> <> <> <> Kill, MakeUndefined: UNSAFE PROC [interval: Interval] = TRUSTED INLINE {SetDataState[interval, undefined]}; <> Touch: PROC [interval: Interval] = TRUSTED INLINE {SwapIn[interval: interval]}; <> <> <> Pin: PROC [interval: Interval] = TRUSTED INLINE {SwapIn[interval: interval, pin: TRUE]}; <> <> <> <> Unpin: PROC [interval: Interval]; <> <> <> <> <> <> MakeReadOnly: PROC [interval: Interval]; <> MakeReadWrite: PROC [interval: Interval]; <> <> MakeUnchanged: PROC [interval: Interval] = TRUSTED INLINE {SetDataState[interval, unchanged]}; <> <> MakeChanged: PROC [interval: Interval] = TRUSTED INLINE {SetDataState[interval, changed]}; <> <> <> <<>> Clean: PROC [interval: Interval]; <> Age: PROC [interval: Interval]; <> <> <> AddressFault: ERROR [address: LONG POINTER]; WriteProtectFault: ERROR [address: LONG POINTER]; <> CantDoIO: ERROR [reason: IOErrorType, page: PageNumber]; IOErrorType: TYPE = {software, hardware}; <> <> <<>> wordsPerPage: NAT = PrincOps.wordsPerPage; bytesPerPage: NAT = PrincOps.bytesPerPage; <> PagesForWords: PROC [words: INT] RETURNS [pages: PageCount] = INLINE { <> longA: Basics.LongNumber = [li[li: words+wordsPerPage-1]]; longB: Basics.LongNumber = [bytes[lh: longA.hl, ll: longA.lh, hh: 0, hl: longA.hh]]; RETURN[longB.li] }; WordsForPages: PROC [pages: PageCount] RETURNS [words: INT] = INLINE { <> longA: Basics.LongNumber = [li[li: pages]]; longB: Basics.LongNumber = [bytes[lh: longA.ll, ll: 0, hh: longA.hl, hl: longA.lh]]; RETURN[longB.li] }; PagesForBytes: PROC [bytes: INT] RETURNS [pages: PageCount] = INLINE { <> n1: Basics.LongNumber = [li[li: bytes+1]]; n2: Basics.LongNumber = [num[ lowbits: Basics.BITSHIFT[n1.lowbits, -1] + (IF Basics.BITAND[n1.highbits, 1] = 1 THEN 100000B ELSE 0), highbits: Basics.BITSHIFT[n1.highbits, -1] ]]; RETURN[PagesForWords[n2.li]] }; BytesForPages: PROC [pages: PageCount] RETURNS [bytes: INT] = INLINE { <> words: INT = WordsForPages[pages]; RETURN[words+words] }; <<>> AddressForPageNumber: UNSAFE PROC [page: PageNumber] RETURNS [address: LONG POINTER] = INLINE { <> longA: Basics.LongNumber = [li[li: page]]; longB: Basics.LongNumber = [bytes[lh: longA.ll, ll: 0, hh: longA.hl, hl: longA.lh]]; RETURN[LOOPHOLE[longB.lc]] }; PageNumberForAddress: PROC [address: LONG POINTER] RETURNS [page: PageNumber] = INLINE { <> longA: Basics.LongNumber = LOOPHOLE[address]; longB: Basics.LongNumber = [bytes[lh: longA.hl, ll: longA.lh, hh: 0, hl: longA.hh]]; RETURN[longB.li] }; <> <> lowCore: UNCOUNTED ZONE; END.