Merge pull request #7 from francislaus/prefetch_insts

Removed that prefetch instructions can throw exceptions

src/insns/prefetch.i.adoc

@@ -36,7 +36,14 @@ 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
+<<CHERI_SPEC>>, this instruction does not perform a prefetch 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
+* The <<x_perm>> is not set
 
 Legacy Mode Description::
 A PREFETCH.I instruction indicates to hardware that the cache block whose
@@ -46,8 +53,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
 <<ddc>>.
 
-:prefetch_i:
-include::cbo_exceptions.adoc[]
 
 Prerequisites for PREFETCH.I.CAP::
 Zicbop, {cheri_base_ext_name}

src/insns/prefetch.r.adoc

@@ -36,7 +36,14 @@ 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 <<CHERI_SPEC>>, this instruction does not perform a prefetch
+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
+* The <<r_perm>> is not set
 
 Legacy Mode Description::
 A PREFETCH.R instruction indicates to hardware that the cache block whose
@@ -46,8 +53,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 <<ddc>>.
 
-:prefetch_r:
-include::cbo_exceptions.adoc[]
 
 Prerequisites for PREFETCH.R.CAP::
 Zicbop, {cheri_base_ext_name}

src/insns/prefetch.w.adoc

@@ -36,7 +36,14 @@ 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 <<CHERI_SPEC>>, this instruction does not perform a prefetch 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
+* The <<w_perm>> is not set
 
 Legacy Mode Description::
 A PREFETCH.W instruction indicates to hardware that the cache block whose
@@ -47,10 +54,10 @@ encoding is only valid if imm[4:0]=0. The authorising capability for this
 operation is <<ddc>>.
 
 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]

src/riscv-integration.adoc

@@ -1067,6 +1067,13 @@ NOTE: <<CBO.ZERO.CAP>>, <<CBO.ZERO>> issues as a cache line wide store
 
 NOTE: ^1^Other CBOs (<<CBO.FLUSH.CAP>>, <<CBO.FLUSH>>, <<CBO.CLEAN.CAP>>, <<CBO.CLEAN>>, <<CBO.INVAL.CAP>>, <<CBO.INVAL>>) 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 extensions 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