Codex @codex  0

A region of computer memory prepared for DMA. In the four-byte receive example it is the payload destination, and must remain available until the transfer and required DMA buffer synchronization are complete.

A storage unit holding part of a file's contents. The toy inode references two four-byte file data blocks for six bytes of contents: allocated capacity is $2\cdot 4=8$ bytes, while logical size is $4+2=6$ bytes. This counts only the two file data blocks, excluding storage for the inode and directory entries.

A byte position measured from the start of a file, beginning at zero. A memory-mapped file combines a starting file offset with a displacement inside its mapping; this is distinct from an open file description's current read/write position.

A file system organizes files, their file metadata, and the names through which they can be found. In the Unix model used here, a file-system directory contains directory entries associating names with inodes; an inode describes the underlying file and how to locate its contents. The file-system namespace answers "what does this name reach?", while the inode answers "which file is it?". These are distinct responsibilities, even though they cooperate on every lookup.

For a computed toy example, let one file-system directory contain names a and b, both referring to inode 42 in the same file system. That inode has size 6 bytes and two hard links. Its direct references lead to four-byte file data blocks 7 and 9: block 7 holds hell, while block 9 holds o followed by a newline, with two unused slots. Reading either name therefore obtains the same six-byte contents hello followed by a newline. There is one file with two names, not two copies. This direct-reference layout and tiny block size are teaching choices, not requirements on every file system.

The separation is useful because a rename within this file system, from a to a previously unused name c, can change a directory entry without copying the six bytes of contents. The remaining name b still reaches inode 42. A successful write changing the first byte through either name changes what both names subsequently read, to jello followed by a newline. This sharing is the attraction of hard links, and also why a hard link is not an independent backup. A program that replaces a named file with a different file can instead make the names diverge. ^[ref]

File-system journaling makes a group of related file system updates recoverable after a crash by recording them in a journal before changing their final storage locations. The useful promise is file-system crash consistency: after journal replay, a protected file-system transaction has taken effect completely or has not taken effect. File-system transaction durability adds a different promise: an acknowledged update survives the crash. The protected group can contain only file metadata, or both file metadata and file data blocks, depending on the file-system journaling mode.

Consider a tiny file containing ABCD in four-byte file data block 7. Its inode records size 4 and a reference to block 7. Appending EFGH in previously free block 9 requires three new stored records: $I$, the inode with size 8 and references to blocks 7 and 9; $B$, the block allocation bitmap marking block 9 allocated; and $D$, file data block 9 containing EFGH. An inode reference to a block still marked free lets a later allocation overwrite live contents; allocating a block without recording its owner can leak space. Even mutually consistent file metadata can expose stale contents if $D$ has not reached storage. Chapter 42 of Crash Consistency: FSCK and Journaling (section 42.1, pp. 2–4) develops this three-record append problem; the names, block numbers and tiny contents here are original teaching choices.

The first diagram protects all three records with write-ahead logging. Each journal payload record identifies a final destination and its complete new contents. A storage flush makes the complete journal payload durable before a separate journal commit record is written and made durable. Only then may a journal checkpoint copy the records to their final locations. The journal remains available until those copies have themselves passed a storage flush; it can then be retired and its space reused. Journal replay repairs an interrupted journal checkpoint using the retained new contents.^[ref]

These are persistence dependencies, not a claim that issuing writes in this order is sufficient. A device can report completion while its volatile memory cache still holds the only copy. The Linux kernel documents both flushing earlier completed requests and making completion of a particular request depend on persistence. The timeline uses separate storage flushes to make the dependencies explicit; an implementation can use equivalent device-supported operations. A commit write can persist before its storage flush returns: recovery uses the actual durable marker, while acknowledgment waits for successful completion.^[ref]

The appeal is that recovery knows exactly which updates to finish. It does not have to infer a user's intended contents from contradictory inodes and block allocation bitmaps. The cost includes writing the journal payload as well as its final copies and waiting for persistence boundaries. The journal records a recent transition, not a historical collection of recoverable files; file-system journaling is not a file-system backup.

A mathematically precise description of permitted behaviour. A formal specification for the microkernel file-read example's service could relate an authorized request to the exact returned bytes; a formal specification of its microkernel's IPC need only describe the protected transport operation. They state different obligations.

Reinstalling the complete new images of a committed file-system transaction after a crash. An uncommitted journal payload is ignored. Rewriting the same image has idempotence: repeating it gives the same contents, unlike performing "append four more bytes" again. If recovery itself crashes, retaining the journal until the journal checkpoint is durable allows the same recovery to restart.

The second diagram exhausts the small full-data model. A triple lists $I,B,D$ in that order; a bit is 1 exactly when the corresponding new record has persisted. Before commit, any of the $2^3=8$ subsets of journal payload records can be durable, while every final-location triple is 000. After commit, the journal triple is 111, while any of the eight final-location triples can be durable. Retirement adds one state: the live journal is gone and the final-location triple is 111. Thus there are $8+8+1=17$ distinct abstract crash states. Waiting for a storage flush without another record reaching persistence does not create an additional state. Retirement is modeled as an atomic change of live-log status: old payload bytes may remain physically present but are no longer part of the live journal.

The short correctness argument has three cases. Before commit, final locations are unchanged. With commit, the complete journal payload restores 111 regardless of the current final-location subset. After retirement, 111 is already durable. Each of the six partial final-location triples is repairable because its journal is retained. The enumeration is exhaustive for these records and phase rules; it excludes torn records, dishonest flush completion, media corruption, journal reuse across several file-system transactions and failures of the recovery code. It is a model check, not a measured crash test of ext4.

The hardware that performs address translation and access checks. Whether a TLB miss is resolved entirely by hardware or with operating system assistance depends on the architecture.

For paging, the memory management unit uses the active address space and the kind of access: reading, writing, or fetching an instruction. Processor privilege level can also affect permission. A TLB hit supplies cached translation attributes; it does not bypass memory protection. On a TLB miss, some architectures perform a hardware page table walk, while others enter an operating system refill handler. Both can resolve a resident mapping without a nonresident page fault.^[ref]

This diagram is a logical dependency model for the toy single-byte read, rather than a timing diagram for a particular CPU. A translation lookaside buffer caches translations and access attributes; a data memory cache caches contents. A TLB hit can accompany a data cache miss, and a TLB miss can accompany a data cache hit after successful refill. Reading page table entries during refill is also distinct from reading the requested data. Actual implementations may overlap steps.

Extend process A's toy address space with these independent starting states. Virtual page 4 is resident in page frame 13 and readable but not writable. Virtual page 5 is a permitted readable memory page whose old contents are in backing storage and which is initially nonresident. Virtual page 6 has no mapping authorized by the operating system. Assume permission changes and eviction always invalidate affected cached translations before later accesses, no copy-on-write policy, and a free page frame 2 for loading virtual page 5.

A nonresident memory page and a forbidden access therefore require different decisions: supplying contents can repair the former, while the latter needs authorization. Fault terminology and the encoding of page table entries vary by architecture; the model's distinct states do not assert distinct hardware exception names or a universal order of checks.^[ref]

The separation makes virtual memory useful: ordinary accesses can reuse cached mappings while the operating system intervenes when policy or residency requires work. It also makes failures easier to diagnose. A lost cached translation, unavailable contents, and denied permission are three different obstacles, even when all interrupt the same requested read.

Let $P$ be the memory page size, $O$ the aligned starting file offset, $L$ the mapping length and $B$ its base virtual address. A valid displacement $r=v-B$ with $0\le r<L$ corresponds to file offsetHere $j$ is the relative memory page index, the floor function selects its integer part, and Euclidean division gives the within-page displacement $d$. The backing page begins at $O+jP$. This identifies file contents; the page table separately selects a resident page frame and enforces permissions.

Take $P=4096$, $O=4096$ and $L=8192$ bytes in a file of at least 12288 bytes. A has a shared file mapping at $B_A=0x10000000$. B has a shared file mapping at $B_B=0x20000000$ and a private file mapping at $B_C=0x30000000$. 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 $r=4133=4096+37$ selects relative page 1, within-page displacement 37 and file offset $o=8229=0x2025$. 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.

To access a requested file offset $q$ that is not aligned, choose $O=P\lfloor q/P\rfloor$ and displacement $q-O$. 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 $q$ directly as the Linux kernel mmap offset. For example, $q=8229$ uses $O=8192$ and displacement 37; that one-page start differs from our two-page mapping's $O=4096$.