From a30fb6da4f2e2596e15c7d3d2d1fddd3e0b9690f Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Mon, 22 Jan 2024 08:15:16 +0000 Subject: [PATCH 1/7] Removed exceptions for prefetch instructions --- src/insns/prefetch.i.adoc | 2 -- src/insns/prefetch.r.adoc | 2 -- src/insns/prefetch.w.adoc | 4 ++-- 3 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/insns/prefetch.i.adoc b/src/insns/prefetch.i.adoc index 21dc1f5d..ab423d5f 100644 --- a/src/insns/prefetch.i.adoc +++ b/src/insns/prefetch.i.adoc @@ -46,8 +46,6 @@ likely to be accessed by an instruction fetch in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is <>. -:prefetch_i: -include::cbo_exceptions.adoc[] Prerequisites for PREFETCH.I.CAP:: Zicbop, {cheri_base_ext_name} diff --git a/src/insns/prefetch.r.adoc b/src/insns/prefetch.r.adoc index 03d3e916..94fad0fa 100644 --- a/src/insns/prefetch.r.adoc +++ b/src/insns/prefetch.r.adoc @@ -46,8 +46,6 @@ likely to be accessed by a data read (i.e. load) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is <>. -:prefetch_r: -include::cbo_exceptions.adoc[] Prerequisites for PREFETCH.R.CAP:: Zicbop, {cheri_base_ext_name} diff --git a/src/insns/prefetch.w.adoc b/src/insns/prefetch.w.adoc index 1b2e8a34..69284f84 100644 --- a/src/insns/prefetch.w.adoc +++ b/src/insns/prefetch.w.adoc @@ -47,10 +47,10 @@ encoding is only valid if imm[4:0]=0. The authorising capability for this operation is <>. Prerequisites for PREFETCH.W.CAP:: -{cheri_base_ext_name} +Zicbop, {cheri_base_ext_name} Prerequisites for PREFETCH.W:: -{cheri_legacy_ext_name} +Zicbop, {cheri_legacy_ext_name} Operation:: [source,sail] From 9196c1044d6347cce084875402276a4d022f3ddb Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Mon, 22 Jan 2024 13:59:35 +0000 Subject: [PATCH 2/7] Added explanation for prefetching instructions --- src/insns/prefetch.i.adoc | 4 +++- src/insns/prefetch.r.adoc | 4 +++- src/insns/prefetch.w.adoc | 4 +++- src/riscv-integration.adoc | 7 +++++++ 4 files changed, 16 insertions(+), 3 deletions(-) diff --git a/src/insns/prefetch.i.adoc b/src/insns/prefetch.i.adoc index ab423d5f..779cc314 100644 --- a/src/insns/prefetch.i.adoc +++ b/src/insns/prefetch.i.adoc @@ -36,7 +36,9 @@ effective address is the sum of the base address specified in `cs1` and the sign-extended offset encoded in imm[11:0], where imm[4:0] equals 0b00000, is likely to be accessed by an instruction fetch in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is -`cs1`. +`cs1`. This instruction does not throw any exceptions. However, following +<>, this instruction does not perform a prefetch if it is +not authorized by `cs1`. Legacy Mode Description:: A PREFETCH.I instruction indicates to hardware that the cache block whose diff --git a/src/insns/prefetch.r.adoc b/src/insns/prefetch.r.adoc index 94fad0fa..b6760ce2 100644 --- a/src/insns/prefetch.r.adoc +++ b/src/insns/prefetch.r.adoc @@ -36,7 +36,9 @@ effective address is the sum of the base address specified in `cs1` and the sign-extended offset encoded in imm[11:0], where imm[4:0] equals 0b00000, is likely to be accessed by a data read (i.e. load) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this -operation is `cs1`. +operation is `cs1`. This instruction does not throw any exceptions. However, +in following <>, this instruction does not perform a prefetch +if it is not authorized by `cs1`. Legacy Mode Description:: A PREFETCH.R instruction indicates to hardware that the cache block whose diff --git a/src/insns/prefetch.w.adoc b/src/insns/prefetch.w.adoc index 69284f84..9514b3d8 100644 --- a/src/insns/prefetch.w.adoc +++ b/src/insns/prefetch.w.adoc @@ -36,7 +36,9 @@ effective address is the sum of the base address specified in `cs1` and the sign-extended offset encoded in imm[11:0], where imm[4:0] equals 0b00000, is likely to be accessed by a data write (i.e. store) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this -operation is `cs1`. +operation is `cs1`. This instruction does not throw any exceptions. However, +following <>, this instruction does not perform a prefetch if it +is not authorized by `cs1`. Legacy Mode Description:: A PREFETCH.W instruction indicates to hardware that the cache block whose diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc index 1616e918..6738b63d 100644 --- a/src/riscv-integration.adoc +++ b/src/riscv-integration.adoc @@ -1067,6 +1067,13 @@ NOTE: <>, <> issues as a cache line wide store NOTE: ^1^Other CBOs (<>, <>, <>, <>, <>, <>) require at least one byte of the access to be in `auth_cap` bounds +[#CHERI_SPEC,reftext="CHERI Exceptions and speculative execution"] +=== CHERI Exceptions and speculative execution + +CHERI adds architectural guarantees that can prove to be microarchitecturally useful. +Speculative-execution attacks can -- among other factors -- rely on instructions that fail CHERI permission checks not to take effect. +When implementing any of the extension proposed here, microarchitects need to carefully consider the interaction of late-exception raising and side-channel attacks. + === Physical Memory Attributes (PMA) Typically, the entire memory space need not support tagged data. Therefore, it From 74839bb0faec80ddf839704eb152df0b52ace4a3 Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Mon, 22 Jan 2024 15:22:18 +0000 Subject: [PATCH 3/7] Added conditions under which prefetch instructions evaluate to NOPs --- src/insns/prefetch.i.adoc | 7 ++++++- src/insns/prefetch.r.adoc | 7 ++++++- src/insns/prefetch.w.adoc | 7 ++++++- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/src/insns/prefetch.i.adoc b/src/insns/prefetch.i.adoc index 779cc314..3abaf9f3 100644 --- a/src/insns/prefetch.i.adoc +++ b/src/insns/prefetch.i.adoc @@ -38,7 +38,12 @@ likely to be accessed by an instruction fetch in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, following <>, this instruction does not perform a prefetch if it is -not authorized by `cs1`. +not authorized by `cs1`. This instruction evaluates to a NOP if one or +more of the following conditions of `cs1` are met: +* The tag is not set +* The sealed bit is set +* No bytes of the cache line requested is in bounds +* The X permission is not set Legacy Mode Description:: A PREFETCH.I instruction indicates to hardware that the cache block whose diff --git a/src/insns/prefetch.r.adoc b/src/insns/prefetch.r.adoc index b6760ce2..433e8ff0 100644 --- a/src/insns/prefetch.r.adoc +++ b/src/insns/prefetch.r.adoc @@ -38,7 +38,12 @@ likely to be accessed by a data read (i.e. load) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, in following <>, this instruction does not perform a prefetch -if it is not authorized by `cs1`. +if it is not authorized by `cs1`. This instruction evaluates to a NOP if one +or more of the following conditions of `cs1` are met: +* The tag is not set +* The sealed bit is set +* No bytes of the cache line requested is in bounds +* The R permission is not set Legacy Mode Description:: A PREFETCH.R instruction indicates to hardware that the cache block whose diff --git a/src/insns/prefetch.w.adoc b/src/insns/prefetch.w.adoc index 9514b3d8..2775f9d8 100644 --- a/src/insns/prefetch.w.adoc +++ b/src/insns/prefetch.w.adoc @@ -38,7 +38,12 @@ likely to be accessed by a data write (i.e. store) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, following <>, this instruction does not perform a prefetch if it -is not authorized by `cs1`. +is not authorized by `cs1`. This instruction evaluates to a NOP if one or +more of the following conditions of `cs1` are met: +* The tag is not set +* The sealed bit is set +* No bytes of the cache line requested is in bounds +* The W permission is not set Legacy Mode Description:: A PREFETCH.W instruction indicates to hardware that the cache block whose From fb87c51fe772e6c6182e24e4170d392808bb8fc8 Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Mon, 22 Jan 2024 15:38:22 +0000 Subject: [PATCH 4/7] Slight change in phrasing; it must not issue the prefetch; all prefetch instructions can be considered as NOPs --- src/insns/prefetch.i.adoc | 2 +- src/insns/prefetch.r.adoc | 2 +- src/insns/prefetch.w.adoc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/insns/prefetch.i.adoc b/src/insns/prefetch.i.adoc index 3abaf9f3..63e38521 100644 --- a/src/insns/prefetch.i.adoc +++ b/src/insns/prefetch.i.adoc @@ -38,7 +38,7 @@ likely to be accessed by an instruction fetch in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, following <>, this instruction does not perform a prefetch if it is -not authorized by `cs1`. This instruction evaluates to a NOP if one or +not authorized by `cs1`. This instruction does not issue a prefetch if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set diff --git a/src/insns/prefetch.r.adoc b/src/insns/prefetch.r.adoc index 433e8ff0..b3fd55b2 100644 --- a/src/insns/prefetch.r.adoc +++ b/src/insns/prefetch.r.adoc @@ -38,7 +38,7 @@ likely to be accessed by a data read (i.e. load) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, in following <>, this instruction does not perform a prefetch -if it is not authorized by `cs1`. This instruction evaluates to a NOP if one +if it is not authorized by `cs1`. This instruction does not issue a prefetch if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set diff --git a/src/insns/prefetch.w.adoc b/src/insns/prefetch.w.adoc index 2775f9d8..cc9e1892 100644 --- a/src/insns/prefetch.w.adoc +++ b/src/insns/prefetch.w.adoc @@ -38,7 +38,7 @@ likely to be accessed by a data write (i.e. store) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, following <>, this instruction does not perform a prefetch if it -is not authorized by `cs1`. This instruction evaluates to a NOP if one or +is not authorized by `cs1`. This instruction does not issue a prefetch if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set From ce10dddec98ea9204164cccb8fd4efcb2dc9f761 Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Mon, 22 Jan 2024 15:43:17 +0000 Subject: [PATCH 5/7] typo fix --- src/riscv-integration.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc index 6738b63d..9d55bd77 100644 --- a/src/riscv-integration.adoc +++ b/src/riscv-integration.adoc @@ -1072,7 +1072,7 @@ NOTE: ^1^Other CBOs (<>, <>, <>, < Date: Mon, 22 Jan 2024 16:23:49 +0000 Subject: [PATCH 6/7] changed wording --- src/insns/prefetch.i.adoc | 4 ++-- src/insns/prefetch.r.adoc | 4 ++-- src/insns/prefetch.w.adoc | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/insns/prefetch.i.adoc b/src/insns/prefetch.i.adoc index 63e38521..a50a1aba 100644 --- a/src/insns/prefetch.i.adoc +++ b/src/insns/prefetch.i.adoc @@ -38,8 +38,8 @@ likely to be accessed by an instruction fetch in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, following <>, this instruction does not perform a prefetch if it is -not authorized by `cs1`. This instruction does not issue a prefetch if one or -more of the following conditions of `cs1` are met: +not authorized by `cs1`. This instruction does not perform a memory access +if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set * No bytes of the cache line requested is in bounds diff --git a/src/insns/prefetch.r.adoc b/src/insns/prefetch.r.adoc index b3fd55b2..7b8aafcb 100644 --- a/src/insns/prefetch.r.adoc +++ b/src/insns/prefetch.r.adoc @@ -38,8 +38,8 @@ likely to be accessed by a data read (i.e. load) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, in following <>, this instruction does not perform a prefetch -if it is not authorized by `cs1`. This instruction does not issue a prefetch if one -or more of the following conditions of `cs1` are met: +if it is not authorized by `cs1`. This instruction does not perform a memory +access if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set * No bytes of the cache line requested is in bounds diff --git a/src/insns/prefetch.w.adoc b/src/insns/prefetch.w.adoc index cc9e1892..43ced63a 100644 --- a/src/insns/prefetch.w.adoc +++ b/src/insns/prefetch.w.adoc @@ -38,8 +38,8 @@ likely to be accessed by a data write (i.e. store) in the near future. The encoding is only valid if imm[4:0]=0. The authorising capability for this operation is `cs1`. This instruction does not throw any exceptions. However, following <>, this instruction does not perform a prefetch if it -is not authorized by `cs1`. This instruction does not issue a prefetch if one or -more of the following conditions of `cs1` are met: +is not authorized by `cs1`. This instruction does not perform a memory access +if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set * No bytes of the cache line requested is in bounds From 5699b91eaa19afb45686a797987064353bfc54f4 Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Tue, 23 Jan 2024 07:53:34 +0000 Subject: [PATCH 7/7] added cross references for permissions --- src/insns/prefetch.i.adoc | 2 +- src/insns/prefetch.r.adoc | 2 +- src/insns/prefetch.w.adoc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/insns/prefetch.i.adoc b/src/insns/prefetch.i.adoc index a50a1aba..7a844e49 100644 --- a/src/insns/prefetch.i.adoc +++ b/src/insns/prefetch.i.adoc @@ -43,7 +43,7 @@ if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set * No bytes of the cache line requested is in bounds -* The X permission is not set +* The <> is not set Legacy Mode Description:: A PREFETCH.I instruction indicates to hardware that the cache block whose diff --git a/src/insns/prefetch.r.adoc b/src/insns/prefetch.r.adoc index 7b8aafcb..28c81592 100644 --- a/src/insns/prefetch.r.adoc +++ b/src/insns/prefetch.r.adoc @@ -43,7 +43,7 @@ access if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set * No bytes of the cache line requested is in bounds -* The R permission is not set +* The <> is not set Legacy Mode Description:: A PREFETCH.R instruction indicates to hardware that the cache block whose diff --git a/src/insns/prefetch.w.adoc b/src/insns/prefetch.w.adoc index 43ced63a..ed845385 100644 --- a/src/insns/prefetch.w.adoc +++ b/src/insns/prefetch.w.adoc @@ -43,7 +43,7 @@ if one or more of the following conditions of `cs1` are met: * The tag is not set * The sealed bit is set * No bytes of the cache line requested is in bounds -* The W permission is not set +* The <> is not set Legacy Mode Description:: A PREFETCH.W instruction indicates to hardware that the cache block whose