Memory-mapped file offset translation 2026-10-14
Let be the memory page size, the aligned starting file offset, the mapping length and its base virtual address. A valid displacement with corresponds to file offsetHere is the relative memory page index, the floor function selects its integer part, and Euclidean division gives the within-page displacement . The backing page begins at . This identifies file contents; the page table separately selects a resident page frame and enforces permissions.
Take , and bytes in a file of at least 12288 bytes. A has a shared file mapping at . B has a shared file mapping at and a private file mapping at . These bases are illustrative chosen results, not requested fixed addresses. All three mappings cover the same two backing pages: file offsets 4096–8191 and 8192–12287. Displacement selects relative page 1, within-page displacement 37 and file offset . Thus A's
0x10001025, B's shared 0x20001025 and B's private 0x30001025 initially identify the same byte. The adjacent displacement 4134 identifies file offset 8230. Different virtual addresses can reach the same backing contents.Two operating-system processes map two backing pages at different virtual addresses; displacement 4133 identifies file offset 8229
. Details. To access a requested file offset that is not aligned, choose and displacement . Mapping enough bytes to cover that displacement plus the requested length makes the desired data start inside the aligned mapping. Do not pass the unaligned directly as the Linux kernel
mmap offset. For example, uses and displacement 37; that one-page start differs from our two-page mapping's . Microkernel file-read example 2026-10-14
Consider an original toy file system service in address space B and a client in address space A, on one CPU. The service holds a five-byte cached file containing
LIME followed by a newline. The client already has service handle 9, permission to read that file, and a security capability to send requests to IPC endpoint E. Handle 9 is interpreted by the service; it is neither a virtual address nor an operating-system kernel object identifier. All relevant memory pages are resident, and this read needs no device driver.A cached file read uses IPC between separate address spaces, with authority checked by the microkernel
. Details. - The client submits
READ(7, 9, 0, 4): request identifier7, handle9, byte offset0, and requested length4. A system call enters the microkernel; the security capability is checked before delivery on IPC endpoint E. The client waits for a reply. - A waiting service software thread receives the request. The service checks the handle's read permission and the requested range, then obtains the first four bytes from its cached file. The microkernel transports the request; the service supplies its file system meaning.
- The service uses reply capability authority to return
OK(7, 4, LIME). The client resumes, checks the request identifier and returned length, and copies those four bytes into its own local buffer. There were two logical IPC messages: request and reply. The four arrows show delivery stages, not four separate requests.
This protocol is an illustrative design, not an actual seL4 file system interface. Its call/reply structure follows seL4's documented IPC:
seL4_Call waits using reply authority, and small payloads can travel in processor registers. [ref]An ordinary pointer in A refers to A's address space. Sending its numeric value does not make B's private computer memory appear there. This example explicitly transfers bytes. Sharing a mapped memory page instead would require intentional memory protection permissions and a protocol for ownership and synchronization; passing a pointer alone establishes neither.
The same IPC mechanism could carry
WRITE, but this client could still be refused by the service's read-only handle policy. Conversely, possession of an IPC endpoint security capability permits communication without automatically granting access to every file the service manages. The separation of mechanism and policy appears twice: endpoint authority gates delivery, and the service's handle policy gates the requested operation. mmap 2026-10-14
The POSIX mapping interface. Ordinary Linux kernel file mappings require a positive length and an aligned file offset. A null address lets the operating-system kernel choose an aligned base; length need not be aligned. Check for
MAP_FAILED. After success the file descriptor may be closed without invalidating the mapping; munmap or process termination removes it.[ref]mmap(2) — Linux manual page. DESCRIPTION: address, length, offset and descriptor lifetime; munmap; RETURN VALUE
Mapping does not extend the backing file. Under POSIX, for an initially partial last memory page, the tail beyond the file's end is zero-filled and is not written back as file data; accesses to whole mapped memory pages beyond the end raise
SIGBUS. POSIX leaves access to portions added or removed by later resizing unspecified. Establish the required file size first and coordinate resizing with readers; a mapping's length is not proof that those bytes exist in the file.[ref]mmap — POSIX.1-2024. POSIX.1-2024, DESCRIPTION: partial end page, whole pages beyond the object, and changed file size; RATIONALE: references beyond the end do not extend the object
The Linux kernel documents a tail-cache exception: modified beyond-end bytes can survive in the page cache and appear in later mappings, although never written to the file. Do not use that tail as reliable storage.[ref]
mmap(2) — Linux manual page. BUGS: modified contents beyond the object end can remain in the page cache
Page frame 2026-10-14
A slot in main computer memory that can hold one memory page of the selected size. Physical frame number
0x07 with 256-byte page frames starts at physical address 0x0700. Page table 2026-10-14
A page table is the data structure describing an address space's mappings from virtual page numbers to page frames, together with access and status information. A page table entry can describe a resident memory page and its permissions. Nonresident or unmapped memory pages require a representation that lets the operating system distinguish them; a hardware not-present flag alone need not make that distinction. On x86, additional operating system information determines whether a not-present mapping is legitimate. [ref]
https://pages.cs.wisc.edu/~remzi/OSTEP/vm-paging.pdf. Arpaci-Dusseau and Arpaci-Dusseau, OSTEP chapter 18, section 18.3: page-table contents and the x86 present bit
The four rows drawn under paging are an illustrative model, combining page table and operating system information: virtual page
0x12 is resident in physical frame 0x07 with read-only permission; 0x13 is resident in 0x02 with read/write permission; 0x14 is mapped read/write but nonresident; 0x15 is unmapped. The labels deliberately separate mapping policy, residency and permission. They are not a literal x86 entry layout. A translation lookaside buffer valid flag is a fourth, independent notion: it says that a cached translation can be considered, not that every resident memory page has a cached translation.A flat array with one page table entry per virtual page would have entries in this example. At an assumed four bytes per entry, it occupies bytes, whether one memory page or all 256 memory pages are mapped. A multi-level page table saves space in sparse address spaces by allocating lower-level tables only for the regions that need them. The tradeoff is extra dependent lookups during a page table walk; a translation lookaside buffer avoids repeating those lookups on a hit. [ref]
https://pages.cs.wisc.edu/~remzi/OSTEP/vm-smalltables.pdf. Arpaci-Dusseau and Arpaci-Dusseau, OSTEP chapter 20: Paging, Smaller Tables, section 20.3
Paging 2026-10-13
Paging divides an address space into fixed-size memory pages and main computer memory into equally sized page frames. Here assume byte addressing, one memory page size bytes, and an unsigned virtual address . Its virtual page number and offset areThe brackets denote the floor function, and gives the remainder in Euclidean division. If the page table maps to physical frame number and permits the access, the physical address isThe low bits are unchanged; the other bits select the memory page or page frame. A bit shift and bit mask can extract these fields. [ref]
https://pages.cs.wisc.edu/~remzi/OSTEP/vm-paging.pdf. Arpaci-Dusseau and Arpaci-Dusseau, OSTEP chapter 18: Paging, Introduction, sections 18.1–18.2
For a 16-bit virtual address and bytes, take in hexadecimal. Then and . A mapping to givesThus the eight high bits choose a mapping; the eight low bits choose the same position in the resulting page frame. The 256-byte size is for illustration, not a claim about an actual architecture's supported memory page sizes.
Translating 0x1234 through an illustrative page table, with a separate offset and access check
. Details. The useful freedom is that adjacent memory pages can occupy unrelated page frames. In the diagram, virtual pages
0x12 and 0x13 occupy page frames 0x07 and 0x02; virtual addresses 0x12ff and 0x1300 are consecutive, but translate to physical addresses 0x07ff and 0x0200. Uniform units simplify placement and page replacement, at the cost of page table storage and unused bytes within partly filled memory pages. For example, placing 300 bytes in exclusive 256-byte page frames requires two page frames, leaving bytes unused. Shared-bus timing example 2026-10-13
Stipulated bus arbitration and payload timing for two competing bus bursts
. Details. 


