CTSRD-CHERI / cheri-specification

CHERI ISA Specification
Other
20 stars 6 forks source link

Is CLoadTags cap mode only? #77

Closed tariqkurd-repo closed 1 year ago

tariqkurd-repo commented 1 year ago

The SAIL in the v9 spec for CLoadTags doesn't give the option of authorising via DDC, but the text doesn't say that it's cap mode only. Can you clarify whether it in valid in integer mode, or should it be an illegal instruction?

jrtc27 commented 1 year ago

It’s valid in both modes and always uses a capability operand, hence why it doesn’t mention any option of using DDC and doesn’t say it’s mode-specific.

bsdjhb commented 1 year ago

Note though that the choice to make the addressing mode always cap-relative does make it different from both Morello and the proposed CHERI-x86 which default to integer addressing in hybrid and cap-relative addressing in purecap requiring the following #ifdef in CheriBSD's code to deal with cloadtags use in the hybrid kernel:

#ifdef __riscv
#define cheri_loadtags(m)                       \
    __builtin_cheri_cap_load_tags((__cheri_tocap void * __capability)(m))
#else
#define cheri_loadtags(m)   __builtin_cheri_cap_load_tags((m))
#endif

In practice all the uses of CLoadTags in CheriBSD's hybrid kernel currently use an explicit CFromPtr to derive a cap from DDC anyway, and it seems unlikely that other hybrid uses of CLoadTags would not also end up using a DDC-derived capability in practice.

All this to say that I'm tempted to say that the addressing mode should be dependent on the encoding mode. Certainly the instruction is needed (and currently used in CheriBSD) in both modes.

jrtc27 commented 1 year ago

The theory is that you can always use the capability one in hybrid but you can’t always use the integer one even in hybrid, as converting to a capability is a one-way operation unless your DDC covers it. If you ever want to CLoadTags on user memory then you need the capability version. It just so happens that we currently only use the direct map (what Linux calls the linear map IIRC) for CLoadTags of user memory (both swapping in and out and for revocation) I think, but unless you want to burn encoding space on both addressing modes, you can get away with only the capability version, at the expense of having to do a single CFromPtr before your big loop over all the tag blocks in the range.

Though I do seem to recall Morello’s lack of a capability one in A64 (integer mode) causing some friction in libcaprevoke.

tariqkurd-repo commented 1 year ago

As it only uses cs1 as an address operand then the minimum change required is to following the .dcc/.cap naming scheme showing that the address operand is not mode dependant, so it should be CLoadTags.cap. Or make it cap mode only, either way the current spec is inconsistent.

jrtc27 commented 1 year ago

The suffixes are only there to avoid mnemonic collisions. If you were to rename it to CLoadTags.cap that would strongly hint at the existence of a CLoadTags.ddc, which there is not. The current approach was entirely deliberate.