#29 academic-capstone intro/prog-model revision

attributes.adoc

@@ -1,4 +1,4 @@
-:isa_name: Capstone-RISC-V
+:isa_name: Capstone-RISC-V Academic Version
 :isa_var_pure: Pure Capstone
 :isa_var_hybrid: TransCapstone
 :proj_name: Capstone

parts/intro.adoc

@@ -81,10 +81,10 @@ ____
 == {isa_name} ISA Overview
 
 While {proj_name} does not assume any specific modern ISA, we choose to propose
-a {proj_name} extension to RISC-V due to its open nature and the availability
+a {proj_name} variant to RISC-V due to its open nature and the availability
 of toolchains and simulators.
 
-The {isa_name} ISA is an {base_isa_name} extension that makes the following
+The {isa_name} ISA is an {base_isa_name} variant that makes the following
 types of changes to the base architecture:
 
 * Each general-purpose register is extended to 129 bits to accommodate 128-bit capabilities.
@@ -95,39 +95,6 @@ types of changes to the base architecture:
 * Semantics of some existing instructions are adjusted to support capabilities.
 * Semantics of interrupts and exceptions are adjusted to support capabilities.
 
-== {proj_name} Variants
-
-In addition to {proj_name}, which is referred to as _{isa_var_pure}_ in the {isa_name} ISA,
-we propose a variant of {proj_name}, called _{isa_var_hybrid}_.
-
-While memory accesses and control flow transfers are only possible using capabilities
-in _{isa_var_pure}_, _{isa_var_hybrid}_ fuses capabilities with privilege levels and
-virtual memory found in traditional architectures, which allows for a smooth transition
-from existing architectures to {proj_name}.
-
-The following types of changes are made to _{isa_var_pure}_ to obtain _{isa_var_hybrid}_:
-
-* The physical memory is partitioned into two disjoint regions,
-one exclusively for accesses through capabilities and the other exclusively for accesses
-through the virtual memory.
-* Software components are allowed to run in either of the two _worlds_, i.e., the _normal world_
-and the _secure world_.
-- The _normal world_ follows the traditional privilege levels, allows both capability-based accesses
-and virtual memory accesses, and is therefore compatible with existing software.
-- The _secure world_ follows the _{isa_var_pure}_ design, limits memory accesses to capability-based accesses
-and provides the security guarantees of {proj_name}.
-* A world switching mechanism is added to support the secure switching between the two worlds.
-* Semantics of some _{isa_var_pure}_ instructions are changed to support the two worlds separately.
-* Semantics of interrupts and exceptions are extended to support the two worlds separately.
-
-.Memory Accesses in _{isa_var_hybrid}_
-[%header%autowidth.stretch]
-|===
-| World | Memory Management Unit (MMU) | Capabilities
-| Normal world | Yes | Yes
-| Secure world | No | Yes
-|===
-
 == Assembly Mnemonics
 
 Each {isa_name} instruction is given a mnemonic prefixed with `CS.`.

parts/prog-model.adoc

@@ -27,15 +27,13 @@ Each capability has the following architecturally-visible fields:
 |`valid` | `0..1` | Whether the capability is valid: `0` = invalid, `1` = valid
 |`type` | `0..6` | The type of the capability:
 `0` = linear, `1` = non-linear, `2` = revocation,
-`3` = uninitialised, `4` = sealed, `5` = sealed-return, `6` = exit
+`3` = uninitialised, `4` = sealed, `5` = sealed-return
 |`cursor` | `0..2^XLEN-1` |  Not applicable when `type = 4` (sealed).
 The memory address the capability points to (to be used for the next memory access)
 |`base` | `0..2^XLEN-1` | The base memory address of the memory region associated with the capability
-|`end` | `0..2^XLEN-1` | Not applicable when `type = 4` (sealed), `type = 5` (sealed-return), or
-`type = 6` (exit).
+|`end` | `0..2^XLEN-1` | Not applicable when `type = 4` (sealed) or `type = 5` (sealed-return).
 The end memory address of the memory region associated with the capability
-|`perms` | `0..7` | Not applicable when `type = 4` (sealed), `type = 5` (sealed-return), or
-`type = 6` (exit).
+|`perms` | `0..7` | Not applicable when `type = 4` (sealed) or `type = 5` (sealed-return).
 One-hot encoded permissions associated with the capability:
 `0` = no access, `1` = execute-only, `2` = write-only, `3` = write-execute,
 `4` = read-only, `5` = read-execute, `6` = read-write, `7` = read-write-execute
@@ -126,41 +124,28 @@ The table below summarises the fields used for each type of capabilities.
 |Uninitialised |`3` |Yes |Yes |Yes |Yes |Yes |- |-
 |Sealed |`4` |Yes |- |Yes |- |- |Yes |-
 |Sealed-return |`5` |Yes |Yes |Yes |- |- |Yes |Yes
-|Exit |`6` |Yes |Yes |Yes |- |- |- |-
 |===
 
 When the `async` field of a sealed-return capability is `0` (synchronous),
-or when the `type` field of the capability is `6` (exit),
 some memory accesses are granted by this capability.
 The following table shows the memory accesses granted in such scenarios,
 where `size` is the size of the memory access in bytes.
 
-.Memory accesses granted by sealed-return and exit capabilities
+.Memory accesses granted by sealed-return
 [%header%autowidth.stretch]
 |===
 | Capability type | `async` | Read | Write | Execute
 | Sealed-return | `0` | `cursor in [base + 3 * CLENBYTES, base + 33 * CLENBYTES - size]` | `cursor in [base + 3 * CLENBYTES, base + 33 * CLENBYTES - size]` | No
-| Exit | - | `cursor in [base + 3 * CLENBYTES, base + 33 * CLENBYTES - size]` | `cursor in [base + 3 * CLENBYTES, base + 33 * CLENBYTES - size]` | No
 |===
 
 In other scenarios and for other capability types without the `perms` field, no read/write/execute
 memory accesses are granted by the capability.
 
-****
-The following figure shows the overview of different types of capabilities in _{isa_var_pure}_,
+The following figure shows the overview of different types of capabilities in {isa_name},
 and the operations that change the type of a capability.
 
-.Overview of different types of capabilities in _{isa_var_pure}_
+.Overview of different types of capabilities in {isa_name}
 image::pure-types.svg[pure-types]
-****
-
-****
-The following figure shows the overview of different types of capabilities in _{isa_var_hybrid}_,
-and the operations that change the type of a capability.
-
-.Overview of different types of capabilities in _{isa_var_hybrid}_
-image::trans-types.svg[trans-types]
-****
 
 == Extension to General-Purpose Registers
 
@@ -226,55 +211,25 @@ register with index `i`.
 
 === Program Counter
 
-The following changes are made to the program counter (`pc`):
-
-* _{isa_var_pure}_: the program counter (`pc`) is changed to contain a capability only.
-* _{isa_var_hybrid}_: similar to the general-purpose registers,
-the program counter (`pc`) is extended to contain a capability or an integer.
-
-.*Note: what is `cwrld`*
-[%collapsible]
-====
-****
-`cwrld` is a special register added in _{isa_var_hybrid}_ that indicates the world currently in execution.
-Please see <<additional-regs,Added Registers>> for details.
-****
-====
+The program counter (`pc`) is changed to contain a capability only.
 
 *During the instruction fetch stage, an exception is raised when any of the following conditions is met:*
 
 ****
-_{isa_var_pure}_
-
 * `Instruction access fault (1)`
 - `pc.valid` is `0` (invalid).
 - `pc.type` is neither `0` (linear) nor `1` (non-linear).
 - `pc.perms` is not executable (i.e., `1 \<=p pc.perms` does not hold).
 - `pc.cursor` is not in the range `[pc.base, pc.end - 4]`.
 * `Instruction address misaligned (0)`
 - `pc.cursor` is not aligned to `4`.
-
-_{isa_var_hybrid}_
-
-* `cwrld` is `1` (secure world) and any of the conditions for _{isa_var_pure}_ is met.
-* `cwrld` is `0` (normal world) and any of the conditions for {base_isa_name} is met.
-* `Instruction access fault (1)`
-- `cwrld` is `1` (secure world) and `pc` does not contain a capability.
-- `cwrld` is `0` (normal world) and `pc` does not contain an integer.
 ****
 
 *If no exception is raised:*
 
 ====
-_{isa_var_pure}_ or _{isa_var_hybrid}_ secure world (i.e., `cwrld = 1`)
-
 . The instruction pointed to by `pc.cursor` is fetched and executed.
 . Set `pc.cursor` to `pc.cursor + 4` at the end of the instruction.
-
-_{isa_var_hybrid}_ normal world (i.e., `cwrld = 0`)
-
-. The instruction pointed to by `pc` is fetched and executed.
-. Set `pc` to `pc + 4` at the end of the instruction.
 ====
 
 [#additional-regs]
@@ -283,40 +238,17 @@ _{isa_var_hybrid}_ normal world (i.e., `cwrld = 0`)
 The {isa_name} ISA adds the following registers.
 
 .Additional Registers in {isa_name} ISA
-[#additional-regs]
-[#add-reg-list, cols="1,3a", options="header"]
+[#add-reg-list]
+[%header%autowidth.stretch]
 |===
-|{proj_name} Variant   | Additional Registers
-|_{isa_var_pure}_|
-[cols="1,1,1,4", options="header"]
-!===
-! Mnemonic ! CCSR encoding ! CSR encoding ! Description
-! `ceh`  ! `0x000` ! - ! The sealed capability or PC entry for the exception handler
-! `cih`  ! `0x001` ! - ! The sealed capability for the interrupt handler
-! `cinit` ! `0x002` ! - ! The initial capability covering the entire address space of the memory
-! `epc` ! `0x003` ! - ! The exception program counter register
-! `cis` ! - ! `0x800` ! The interrupt status register
-! `tval` ! - ! `0x801` ! The exception data (trap value) register
-! `cause` ! - ! `0x802` ! The exception cause register
-!===
-
-|_{isa_var_hybrid}_|
-[cols="1,1,1,4", options="header"]
-!===
-! Mnemonic ! CCSR encoding ! CSR encoding ! Description
-! `ceh`  ! `0x000` ! - ! The sealed capability or PC entry for the exception handler
-! `cinit` ! `0x002` ! - ! The initial capability covering the entire address space of the secure memory
-! `epc` ! `0x003` ! - ! The exception program counter register
-! `cwrld`! - ! - ! The world currently in execution. `0` = normal world, `1` = secure world
-! `normal_pc`!-!- !The program counter for the normal world before the secure world is entered
-! `normal_sp`!-!-!The stack pointer for the normal world before the secure world is entered
-! `switch_reg`!-!-! The index of the general-purpose register used when switching worlds
-! `switch_cap`! `0x004` !-! The capability used to store contexts when switching worlds asynchronously
-! `exit_reg`!-!-! The index of the general-purpose register for receiving the exit code when exiting the secure world 
-! `tval` ! - ! `0x801` ! The exception data (trap value) register
-! `cause` ! - ! `0x802` ! The exception cause register
-! `emode` ! - ! `0x804` ! The encoding mode of the machine. `0` = integer encoding mode, `1` = capability encoding mode
-!===
+| Mnemonic | CCSR encoding | CSR encoding | Description
+| `ceh`  | `0x000` | - | The sealed capability or PC entry for the exception handler
+| `cih`  | `0x001` | - | The sealed capability for the interrupt handler
+| `cinit` | `0x002` | - | The initial capability covering the entire address space of the memory
+| `epc` | `0x003` | - | The exception program counter register
+| `cis` | - | `0x800` | The interrupt status register
+| `tval` | - | `0x801` | The exception data (trap value) register
+| `cause` | - | `0x802` | The exception cause register
 |===
 
 Some of the registers only allow capability values and have special semantics
@@ -331,11 +263,10 @@ The manipulation constraints for each CCSR are indicated below.
 [%header%autowidth.stretch]
 |===
 |Mnemonic | Read | Write
-|`ceh` | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world
-|`cih` | - | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world; the original content must not be a capability
-|`cinit` | _{isa_var_pure}_ or _{isa_var_hybrid}_ normal world; one-time only | -
-|`epc` | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world
-|`switch_cap` | _{isa_var_hybrid}_ normal world | _{isa_var_hybrid}_ normal world
+|`ceh` | No constraint | No constraint
+|`cih` | - | The original content must not be a capability
+|`cinit` | Oone-time only | -
+|`epc` | No constraint | No constraint
 |===
 
 Some of the registers are added as _control and status registers_ (CSRs).
@@ -351,10 +282,9 @@ The manipulation constraints for each additional CSR are indicated below.
 [%header%autowidth.stretch]
 |===
 |Mnemonic | Read | Write
-|`cis`| _{isa_var_pure}_ | _{isa_var_pure}_
-|`tval`| _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world
-|`cause`| _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world | _{isa_var_pure}_ or _{isa_var_hybrid}_ secure world
-|`emode`| _{isa_var_hybrid}_ normal world | _{isa_var_hybrid}_ normal world
+|`cis`| No constraint | No constraint
+|`tval`| No constraint | No constraint
+|`cause`| No constraint | No constraint
 |===
 
 .*Note: `ceh` and `cih`*
@@ -393,34 +323,19 @@ and any attempt to read it after the first time will return the content of `cnul
 
 The memory is addressed using an `XLEN`-bit integer at byte-level
 granularity.
+
 In addition to raw integers, each `CLEN`-bit aligned address can
 also store a capability.
 The type of data contained in a memory location is maintained and
 confusion of the type is not allowed.
-
-In _{isa_var_pure}_, the memory can _only_ be accessed through capabilities.
+The physical memory can _only_ be accessed through capabilities.
 
 [%header%autowidth.stretch]
 |===
 | Address Space | Access Method
 | `[0, 2^XLEN)` | Capabilities
 |===
 
-In _{isa_var_hybrid}_, the physical memory is divided into two disjoint regions:
-the _normal memory_ and the _secure memory_.
-While the normal memory is only accessible through _Memory Management Unit_ (MMU),
-the secure memory can only be accessed through capabilities.
-
-The bounds of the secure memory `[SBASE, SEND)` are implementation-defined.
-But both `SBASE` and `SEND` are required to be `CLENBYTES`-byte aligned.
-
-[%header%autowidth.stretch]
-|===
-| Memory Region | Address Space | Access Method
-| Normal memory | `[0, SBASE) U [SEND, 2^XLEN)` | MMU
-| Secure memory | `[SBASE, SEND)` | Capabilities
-|===
-
 == Instruction Set
 
 The {isa_name} instruction set is based on the {base_isa_name} instruction set.
@@ -460,8 +375,6 @@ They receive up to two register operands and a 5-bit-wide immediate operand.
 Upon reset, the system state must conform to the following
 specifications.
 
-_{isa_var_pure}_
-
 ****
 * Each general-purpose register either contains an integer, or a capability with `valid = 0` (invalid).
 * No addressable memory location can contain a capability.
@@ -471,16 +384,3 @@ capabilities with `valid = 0` (invalid).
 * `cinit = { valid = 1, type = 0, cursor = INIT_DATA_BASE, base = INIT_DATA_BASE, end = INIT_DATA_END, perms = 7 }`,
 and `pc = { valid = 1, type = 0, cursor = INIT_CODE_BASE, base = INIT_CODE_BASE, end = INIT_CODE_END, perms = 7 }`, where `INIT_DATA_BASE`, `INIT_DATA_END`, `INIT_CODE_BASE`, and `INIT_CODE_END` are implementation-defined, and `[INIT_CODE_BASE, INIT_CODE_END)` does not overlap with `[INIT_DATA_BASE, INIT_DATA_END)`.
 ****
-
-_{isa_var_hybrid}_
-
-****
-* Each general-purpose register either contains an integer, or a capability with `valid = 0` (invalid).
-* No addressable memory location can contain a capability.
-* `ceh`, `epc` and `switch_cap` contain either an integer or
-a capability with `valid = 0` (invalid).
-* `cwrld = 0` (normal world).
-* `emode = 0` (integer encoding mode).
-* `cinit = { valid = 1, type = 0, cursor = SBASE, base = SBASE, end = SEND, perms = 7 }`.
-* Specifications for {base_isa_name}.
-****

parts/version.adoc

@@ -1,6 +1,6 @@
 :reproducible:
 
-*Version Information:* Draft version. Refer to the commit hash.
+*Version Information:* Version 1.0
 
 ifdef::backend-html5[]
 *Other formats:* This document is also available in the following formats: