Open jasonyu1996 opened 5 days ago
The "tag set, but bounds malformed" case should only be possible due to an error in the memory subsystem/bit flips, maybe we should more explicitly call out that these will not exist in a well-defined execution?
The "tag set, but bounds malformed" case should only be possible due to an error in the memory subsystem/bit flips, maybe we should more explicitly call out that these will not exist in a well-defined execution?
I think the culprit is "A capability is malformed if its encoding does not describe a valid capability because its bounds cannot be correctly decoded" in 2.2.6. The reader would expect that sentence to be a definition of "malformed capabilities", which should be something like "A capability is malformed when its bounds cannot be correctly decoded." Whether it is a valid capability is irrelevant here. Also, it's not "because its bounds cannot be correctly decoded" that a malformed capability "does not describe a valid capability". In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.
In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.
Not quite, and this is something we've been working on very recently.
If a corrupted (tagged and malformed capability) is read by the memory system it will be propagated through stores, and register moves without modification.
Any instruction which needs to decode the bounds will take action, e.g. setting the result to 0 for GCBASE
.
We didn't want to clean up bad caps as LC/SC/CMV
should just propagate what's there to avoid complicating the micro-architecture.
In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.
Not quite, and this is something we've been working on very recently. If a corrupted (tagged and malformed capability) is read by the memory system it will be propagated through stores, and register moves without modification. Any instruction which needs to decode the bounds will take action, e.g. setting the result to 0 for
GCBASE
.We didn't want to clean up bad caps as
LC/SC/CMV
should just propagate what's there to avoid complicating the micro-architecture.
But the only source of malformed but tagged capabilities is errors in the memory subsystem or hardware bugs? The ISA level makes sure that tagged capabilities that can ever be created/derived are all well-formed right?
Chapter 2 mentions:
and
So one would expect "valid capabilities = capabilities with tag set"
But in 2.2.6
which suggests that a capability can be invalid because its bounds cannot be decoded, even if the tag is set.
The consequence is one doesn't know if this in 2.2.1 applies to tagged capabilities with non-decodable bounds: