Linear-memory
Linear Memory Accessor and Updater Functions
First, a quick note about virtual, linear, and physical
addresses:
- Linear (or Virtual) Address: In the flat memory model (see
Intel Vol. 1, Section 3.3.1), memory appears to a program as a single,
continuous address space, called a linear (or virtual) address
space. An address for any byte in linear address space is called a
linear address. When paging is disabled, then a linear address is the
same as a physical address.
- Physical Address: The memory that the processor addresses
on its bus is called physical memory. Physical memory is organized as
a sequence of 8-bit bytes. Each byte is assigned a unique address,
called a physical address. When employing the processor's memory
management facilities, programs do not directly address physical
memory.
Subtopics
- Reasoning-about-memory-reads-and-writes
- Definitions of rb and wb
- Wml256
- Rml256
- Wml512
- Rml512
- Rml128
- Rml80
- Program-location
- Rml64
- Wml128
- Rml48
- Rml32
- Rml08
- Rml16
- Wml80
- Wml64
- Wml08
- Byte-listp
- Recognizer of a list of bytes
- Wml48
- Parametric-memory-reads-and-writes
- Functions to read/write 8/16/32/64/128/256 bits into the memory.
- Combine-n-bytes
- Wml32
- Program-at
- Predicate that makes a statement about a program's location
in the memory
- Wml16
- Combine-bytes
- Combine a list of bytes, LSB-first, into a single unsigned number
- Write-canonical-address-to-memory-user-exec
- Write-canonical-address-to-memory
- Riml64
- Wml-size
- Rml-size
- Riml32
- Riml16
- Riml08
- Wiml64
- Wiml32
- Wiml16
- Wiml08
- Wiml-size
- Generate-xr-over-write-thms
- Generate-write-fn-over-xw-thms
- Generate-read-fn-over-xw-thms
- Riml-size
