		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Setting-up-page-tables

Setting up the page tables for a user-level program's run.

Recall that when the value of the field app-view is nil, the x86 model offers the system-level view of x86 machines. It's only in this view that memory read and write functions like rml08 and wml08 will do a page-table walk. See section app-view for details.

Subtopics

Construct-pml4-table: Construct a PML4 table, one entry at a time, each of which references a Page-Directory-Pointer Table.
Construct-pdp-table: Construct a PDP table, one entry at a time, each of which map a 1GB page.
Load-qwords-into-physical-memory-list: Load lists of physical-addr-qword-alistp into the physical memory.
Construct-pdp-tables: Construct PDP tables, where each table has entries that map a 1GB page.
Load-qwords-into-physical-memory: Load 64-bit entries into the physical memory.
Construct-page-tables: Construct page tables that do linear address translation to 1GB page using IA32e paging.
Physical-addr-qword-alistp: Recognizer for a list of pairs of up to 52-bit wide physical address and byte.
Add-pml4-entry: Add a PML4 entry that references a Page-Directory-Pointer Table.
Add-pdp-entry: Add a PDP entry that maps a 1GB page.
Physical-addr-qword-alist-listp: Recognizer for a list of physical-addr-qword-alistp.