<<>> <> <> <> <> <> <> <> <> <> <> DIRECTORY Basics USING [BITLSHIFT, BITRSHIFT]; <> <> <<>> VM: CEDAR DEFINITIONS IMPORTS Basics = BEGIN <> PageNumber: TYPE = INT; -- INT[0..2­(32-logBytesPerPage)) PageCount: TYPE = INT; -- INT[0..2­(32-logBytesPerPage)) <> <> <<>> Interval: TYPE = RECORD [page: PageNumber, count: PageCount]; <> <<>> nullInterval: Interval = [page: 0, count: 0]; <> ZeroPageCount: TYPE = PageCount[0..0]; NullInterval: TYPE = RECORD [page: PageNumber, count: ZeroPageCount]; FalseBool: TYPE = BOOL[FALSE..FALSE]; ZeroPageNumber: TYPE = PageNumber[0..0]; <> VMPartition: TYPE = { normalVM }; <> <<>> LogPageCount: TYPE = NAT[0..31--LogBase2[PageCount.LAST]-1--]; Allocate: PROC [count: PageCount, partition: VMPartition ¬ normalVM, subRange: NullInterval ¬ [0, 0], start: ZeroPageNumber ¬ 0, alignment: LogPageCount ¬ 0, in64K: FalseBool ¬ FALSE] RETURNS [interval: Interval]; <> <<(1) each page in it was previously unallocated>> <<(2) interval.count = count,>> <<(3) interval.page MOD 2alignment is zero>> <> <> <> SimpleAllocate: PROC [count: PageCount] RETURNS [interval: Interval]; <<... equivalent to Allocate[count: count], defaulting all other parameters.>> <<>> CantAllocate: ERROR [bestInterval: Interval]; <<... raised by Allocate; >> <<>> Free: UNSAFE PROC [interval: Interval]; <<... performs SetDataState[interval, none].>> <> <> <<>> <> Touch: PROC [interval: Interval]; <<... performs SwapIn[interval: interval].>> <> <> <> <> AddressFault: ERROR [address: LONG POINTER]; WriteProtectFault: ERROR [address: LONG POINTER]; <> <<>> <> <> <<>> wordsPerPage: READONLY NAT; logWordsPerPage: READONLY NAT; bytesPerPage: READONLY NAT; logBytesPerPage: READONLY NAT; unitsPerPage: READONLY NAT; logUnitsPerPage: READONLY NAT; PagesForWords: PROC [words: INT] RETURNS [pages: PageCount] = INLINE { RETURN[LOOPHOLE[Basics.BITRSHIFT[words+(wordsPerPage-1), logWordsPerPage]]] }; WordsForPages: PROC [pages: PageCount] RETURNS [words: INT] = INLINE { RETURN[Basics.BITLSHIFT[pages, logWordsPerPage]] }; PagesForBytes: PROC [bytes: INT] RETURNS [pages: PageCount] = INLINE { RETURN[LOOPHOLE[Basics.BITRSHIFT[bytes+(bytesPerPage-1), logBytesPerPage]]] }; BytesForPages: PROC [pages: PageCount] RETURNS [bytes: INT] = INLINE { RETURN[Basics.BITLSHIFT[pages, logBytesPerPage]] }; <<>> PageNumberForAddress: PROC [address: POINTER] RETURNS [page: PageNumber] = INLINE { RETURN[LOOPHOLE[Basics.BITRSHIFT[LOOPHOLE[address], logUnitsPerPage]]] }; AddressForPageNumber: PROC [page: PageNumber] RETURNS [address: POINTER] = INLINE { RETURN[LOOPHOLE[Basics.BITLSHIFT[page, logUnitsPerPage]]] }; END.