Start on a programmer's model for capabilities #48
Conversation
|
are you a RISC-V member? If so you need to state your affiliation so we know who you are as you are currently anonymous. |
|
Stefan is a long-standing member of the community whose name features in multiple specifications |
|
Regardless of whether I contributed to the spec prior to RVI existing, I do have a current RVI membership e.g. https://lists.riscv.org/g/tech-unprivileged/message/629 . |
| based on XLENMAX regardless of the effective XLEN value. | ||
| define *XLENMAX* to be widest XLEN that the implementation supports. | ||
|
|
||
| {cheri_base_ext_name} defines capabilities which act on virtual addresses of |
There was a problem hiding this comment.
| {cheri_base_ext_name} defines capabilities which act on virtual addresses of | |
| {cheri_base_ext_name} defines capabilities which act on addresses of |
I'd drop the virtual here since we also want to support systems without virtual memory.
| determined by the environment. | ||
|
|
||
| A tag, together with a capability or CLEN bits of non-capability data, is | ||
| called a *capability value*. A capability value with a tag of 1 will be |
There was a problem hiding this comment.
I'm not sure about using "value" here since it's such an overloaded word. Maybe just use "capability" and "untagged/invalid capability" vs "valid capability"?
Not too important, but this would conflict with Arm's spec where they use "value" for the address bits of a capability
There was a problem hiding this comment.
Or maybe use "repreesntation" instead of "value"? Naming is difficult and I don't think we ever came up with an unambiguous terminology in the past...
There was a problem hiding this comment.
We've always used value to mean this, and it's the natural term to use. Arm's conflicting use is a bad idea that should be confined to the dustbin of history; it conflicts with the CHERI spec's terminology, is confusing, and makes it harder to refer to the whole capability. I am all for codifying "capability value" as being the whole capability.
| all integer registers, and a subset of CSRs if they are implemented, to hold a | ||
| single capability value. | ||
|
|
||
| There are two basic types of capability. An *unsealed capability* represents |
There was a problem hiding this comment.
| There are two basic types of capability. An *unsealed capability* represents | |
| There are two basic types of capabilities. An *unsealed capability* represents |
I think I'd use the plural here but I guess both works?
|
|
||
| A capability value may also be viewed in terms of the access it provides. In | ||
| this view, a capability value has a *tag*, an *address*, a *base*, a *length*, | ||
| *permissions*, and a *sealed state*; the CGETBASE, CGETLEN, and CGETPERM |
There was a problem hiding this comment.
| *permissions*, and a *sealed state*; the CGETBASE, CGETLEN, and CGETPERM | |
| *permissions*, and a *type*; the CGETBASE, CGETLEN, and CGETPERM |
We have generally use "type" for this field. While the initial spec only provides two types (unsealed and sentry) and thus sealed state would be sufficient, I very strongly believe we need more types in the future (e.g. software defines ones or indirect sentries as defined in the Morello spec).
| sum of the base and the length is also called the *top*, and will be no more | ||
| than 2^XLEN^ for a well-formed capability. A capability with base *B* and | ||
| length *L* authorizes access to all bytes of the address space whose address | ||
| *A* satisfies *B* <= *A* < *B* + *L*, as further defined by the sealing and |
There was a problem hiding this comment.
While it doesn't really make any difference to the semantics, over the past few years I've looked more at the top and base rather than the length. Historically, earlier prototypes of CHERI were defined mostly in terms of length, but since the compressed bounds format was introduced length is simply the difference between top and base.
How about rephrasing this to use base and top as the two components and length as the derived quantity?
| Subset and equality operations treat capability bounds as intervals, not as | ||
| sets. Two capabilities with length 0 and different bases are not equal and not |
There was a problem hiding this comment.
| Subset and equality operations treat capability bounds as intervals, not as | |
| sets. Two capabilities with length 0 and different bases are not equal and not | |
| Subset and equality operations treat capability bounds as intervals. Two capabilities with length 0 and different bases are not equal and not |
I'm not sure if the "set" terminology could be confusing for readers with less of a mathematical background. Maybe just clarifying that it's an interval is sufficient?
| subsets of each other. A capability of length 0 can be constructed only inside | ||
| an existing capability for an interval which surrounds the base. |
There was a problem hiding this comment.
You can construct a zero-length capability for any address between base and top.
First increment to the desired in-bounds (or == top) address, and then CSETBOUNDS with length zero.
But maybe I am just misparsing "surrounds the base"
| subsets of each other. A capability of length 0 can be constructed only inside | ||
| an existing capability for an interval which surrounds the base. | ||
|
|
||
| The bounds and address of a capability are subject to alignment and |
There was a problem hiding this comment.
I think it is very important to note representability, but I think the more detailed part with the table should be part of the bounds format section instead?
What we have here is a description of the rules governing CSETBOUNDS and CSETADDR which does not involve exponents (embedded, implied, or otherwise), mantissas, bitwise operations, Boolean lookup tables, arithmetic carry-out, or more than a passing mention of tops.
I anticipate reworking much of chapter 2 to clarify the various operations and reduce the conceptual complexity of explaining each part. I wanted to post this early since there's a high potential for merge conflicts, and to find out if this needs to be coordinated with anyone and how much to break it apart.