:: commit e94d2b79938f34f5699410889b1eee93c7dab988

diff --git a/PROTOCOL.md b/PROTOCOL.md
index 90030bd6..50999b6c 100644
--- a/PROTOCOL.md
+++ b/PROTOCOL.md
@@ -112,6 +112,47 @@ If the kernel is a position independent executable, the bootloader is free to
 relocate it as it sees fit, potentially performing KASLR (as specified by the
 config).
 
+## Caching
+
+### x86-64
+
+The kernel executable, loaded at or above `0xffffffff80000000`, sees all of its
+segments mapped using write-back (WB) caching at the page tables level.
+
+All HHDM and identity map memory regions are mapped using write-back (WB) caching at the page
+tables level, except framebuffer regions which are mapped using write-combining
+(WC) caching at the page tables level.
+
+The PAT's (Page Attribute Table) layout is specified to be as follows:
+```
+PAT0 -> WB
+PAT1 -> WT
+PAT2 -> UC-
+PAT3 -> UC
+PAT4 -> WP
+PAT5 -> WC
+PAT6 -> unspecified
+PAT7 -> unspecified
+```
+
+The MTRRs are left as the firmware set them up.
+
+### aarch64
+
+The kernel executable, loaded at or above `0xffffffff80000000`, sees all of its
+segments mapped using Normal Write-Back RW-Allocate non-transient caching mode.
+
+All HHDM and identity map memory regions are mapped using the Normal Write-Back RW-Allocate
+non-transient caching mode, except for the framebuffer regions, which are
+mapped in using an unspecified caching mode, correct for use with the
+framebuffer on the platform.
+
+The `MAIR_EL1` register will at least contain entries for the above-mentioned
+caching modes, in an unspecified order.
+
+In order to access MMIO regions, the kernel must ensure the correct caching mode
+is used on its own.
+
 ## Machine state at entry
 
 ### x86-64
@@ -163,27 +204,25 @@ All other general purpose registers are set to 0.
 unless the an Entry Point feature is requested (see below), in which case,
 the value of `PC` is going to be taken from there.
 
-The contents of the `VBAR_EL1` register are undefined, and the kernel must load it's own.
-
-The `MAIR_EL1` register will contain at least these entries, in an unspecified order:
- - Normal, Write-back RW-Allocate non-transient (`0b11111111`),
- - Unspecified, correct for use with the framebuffer.
+The contents of the `VBAR_EL1` register are undefined, and the kernel must load
+its own.
 
-The kernel and the lower-half identity mapping will be mapped with Normal write-back memory,
-while the framebuffer is mapped with the correct caching mode. The kernel must ensure that
-MMIO it wants to access is mapped with the correct caching mode.
+The `MAIR_EL1` register contents are described above, in the caching section.
 
 All interrupts are masked (`PSTATE.{D, A, I, F}` are set to 1).
 
-The kernel is entered in little-endian AArch64 EL1t (EL1 with `PSTATE.SP` set to 0, `PSTATE.E` set to 0, and `PSTATE.nRW` set to 0).
+The kernel is entered in little-endian AArch64 EL1t (EL1 with `PSTATE.SP` set to
+0, `PSTATE.E` set to 0, and `PSTATE.nRW` set to 0).
 
 Other fields of `PSTATE` are undefined.
 
-At entry: the MMU (`SCTLR_EL1.M`) is enabled, the I-Cache and D-Cache (`SCTLR_EL1.{I, C}`) are enabled,
-data alignment checking (`SCTLR_EL1.A`) is disabled. SP alignment checking (`SCTLR_EL1.{SA, SA0}`) is enabled.
-Other fields of `SCTLR_EL1` are reset to 0 or to their reserved value.
+At entry: the MMU (`SCTLR_EL1.M`) is enabled, the I-Cache and D-Cache
+(`SCTLR_EL1.{I, C}`) are enabled, data alignment checking (`SCTLR_EL1.A`) is
+disabled. SP alignment checking (`SCTLR_EL1.{SA, SA0}`) is enabled. Other fields
+of `SCTLR_EL1` are reset to 0 or to their reserved value.
 
-Higher ELs do not interfere with accesses to vector or floating point instructions or registers.
+Higher ELs do not interfere with accesses to vector or floating point
+instructions or registers.
 
 Higher ELs do not interfere with accesses to the generic timer and counter.
 
@@ -195,7 +234,8 @@ If booted by EFI/UEFI, boot services are exited.
 at least 64KiB (65536 bytes) in size, or the size specified in the Stack
 Size Request (see below).
 
-All other general purpose registers (including `X29` and `X30`) are set to 0. Vector registers are in an undefined state.
+All other general purpose registers (including `X29` and `X30`) are set to 0.
+Vector registers are in an undefined state.
 
 ## Feature List