diff --git a/src/cheri-pte-ext.adoc b/src/cheri-pte-ext.adoc index 364beb35..a42f8c26 100644 --- a/src/cheri-pte-ext.adoc +++ b/src/cheri-pte-ext.adoc @@ -71,7 +71,9 @@ The page table entry format remains unchanged for Sv32. However, two new bits, Capability Write (CW) and Capability Read Generation (CRG), are added to leaf PTEs in Sv39, Sv48 and Sv57 as shown in xref:sv39pte[xrefstyle=short], xref:sv48pte[xrefstyle=short] and -xref:sv57pte[xrefstyle=short] respectively. +xref:sv57pte[xrefstyle=short] respectively. For non-leaf PTEs these bits +remain reserved and must be cleared by software for forward compatibility, +or else a page-fault exception is raised. .Sv39 page table entry [#sv39pte] @@ -85,9 +87,10 @@ include::img/sv48pte.edn[] [#sv57pte] include::img/sv57pte.edn[] -NOTE: All behavior related to {cheri_pte_ext_name} requires the authorizing capability to have - <>. If <> is _not_ granted then all capability load/stores and AMOs always clear - the tag and the behavior in this section is not relevant. +NOTE: The behavior in this section isn't relevant if: + +. The authorizing capability doesn't have <>, for loads, stores and AMOs. +. {cheri_levels_ext_name} has cleared the stored tag, for stores and AMOs. The CW bit indicates whether reading or writing capabilities with the tag set to the virtual page is permitted. When the CW bit is set, capabilities are written @@ -102,11 +105,15 @@ If the CW bit is clear then: of the capability being written is set. * When CRG is set, the "pre-CW state", two schemes are permitted (also see <>): +NOTE: The tag bit of the stored capability is checked _after_ it is potentially +cleared <>. + ** The same behavior as when CRG is clear, allowing software interpretation of this state. ** When a capability store or AMO instruction is executed and the tag bit of the capability being written is set, the implementation sets the CW bit and assigns the CRG bit equal to <>.CRG. ++ The PTE update must be atomic with respect to other accesses to the PTE, and must atomically check that the PTE is valid and grants sufficient permissions. Updates to the CW bit @@ -128,13 +135,10 @@ When CW is set, the CRG bit indicates the current generation of the virtual memo regards to the ongoing capability revocation cycle. Two schemes are permitted: * A load page fault exception is raised when a capability load or AMO instruction is executed -and the virtual page's CRG bit does not equal <>.CRG. -* A load page fault exception is raised when a capability load or AMO instruction is executed, -the capability read from memory has tag set -and the virtual page's CRG bit does not equal <>.CRG. - -NOTE: An implementation may avoid a dependency on the tag -bit value of the capability read. This will introduce additional traps during revocation sweeps. +with <> granted and the virtual page's CRG bit does not equal <>.CRG. +* A load page fault exception is raised when a capability load or AMO instruction is executed +with <> granted and the virtual page's CRG bit does not equal <>.CRG +and the capability read from memory optionally has its tag set^1^. [[pte_cw_crg_load_summary]] .Summary of Load CW and CRG behavior in the PTEs @@ -159,6 +163,7 @@ bit value of the capability read. This will introduce additional traps during re ^1^ The choice here is whether to take data dependent exceptions on loads or atomic operations. It is legal for the implementation to fault even if the tag is not set since this behavior is only an optimization for software. This means it is also legal to only check the tag under certain conditions and conservatively fault otherwise. + Taking a trap when the tag is not set will introduce additional traps during revocation sweeps. ^2^ See <>. diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc index e1c48fe8..776ba28c 100644 --- a/src/riscv-integration.adoc +++ b/src/riscv-integration.adoc @@ -216,6 +216,7 @@ misaligned address fault exceptions when the effective address to access is misaligned, even if the implementation supports Zicclsm. To transfer CLEN misaligned bits without a tag, use integer loads and stores. +[#tags_cleared_by_permissions] For loads, the tag of the capability loaded from memory is cleared if the authorizing capability does not grant permission to read capabilities (i.e. both <> and <> must be set in AP). For stores, the tag of the