• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Community
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
        • Dynamic-instrumentation
        • Initialize-x86-state
        • Binary-file-load-fn
        • Read-channel-into-memory
        • Setting-up-page-tables
          • Construct-pml4-table
          • Construct-pdp-table
          • Load-qwords-into-physical-memory-list
          • Construct-pdp-tables
          • Load-qwords-into-physical-memory
          • Construct-page-tables
          • Physical-addr-qword-alistp
          • Add-pml4-entry
          • Add-pdp-entry
          • Physical-addr-qword-alist-listp
        • Read-channel-into-byte-list
        • Init-zero-page
        • Linux-load
        • Read-file-into-memory
        • Read-file-into-byte-list
        • Init-sys-view
        • Load-elf-sections
        • Chars-to-c-str
        • String-to-c-str
        • Pack-u64
        • Pack-u32
        • Concrete-simulation-examples
        • Gdt-entry
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• 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.