rust-sel4 icon indicating copy to clipboard operation
rust-sel4 copied to clipboard

term "granule" used through rust-sel4 crates not in sel4 itself

Open midnightveil opened this issue 5 months ago • 5 comments

I noticed that the rust-sel4 bindings seem to have used the "Granule" referring to the SmallPage, in the ARM sense, and it's defined as an alias for x86, RISC-V. And it has made its way into the tutorial: https://sel4.github.io/seL4-rust-tutorial/root-task/spawn-task.html#step-7e-challenge.

This confused a colleague (@dreamliner787-9) as it's not actually used anywhere in seL4, nor documented that well.

It seems to be a term derived from the ARM spec (which uses it because Granule is generic over 4K/16K/64K minimum memory unit size), though seL4 doesn't even support the 16K/64K page types.

At the very least I don't see why it would be defined for x86 or RISC-V, given it's not an architectural term there either.

midnightveil avatar Jul 18 '25 05:07 midnightveil

Like Arm says, "the selected granule is the smallest block that can be described in the last level table". It is not the minimum page itself, so calling pages granules is wrong for Arm too.

Indanz avatar Jul 18 '25 08:07 Indanz

Thanks for this feedback, you're right, the use of this term is confusing. My intent was to use it to mean literally the granule from the perspective of the seL4 API (that is, the smallest page size/unit of memory that the seL4 API deals in) rather than directly from the ARM ISA, but the use of this term in the ARM ISA makes its use in the sel4 crate confusing.

As for alternatives, how does SmallestPage sound?

nspin avatar Aug 22 '25 21:08 nspin

Do you mean seL4_PageBits? Smallest memory seL4 deals with via UTs is seL4_MinUntypedBits, which is 4.

Indanz avatar Aug 22 '25 23:08 Indanz

Do you mean seL4_PageBits? Smallest memory seL4 deals with via UTs is seL4_MinUntypedBits, which is 4.

Ah yes, sorry for being unclear, I meant the smallest unit on the VSpace facet of the API.

nspin avatar Aug 23 '25 01:08 nspin

Do you mean seL4_PageBits? Smallest memory seL4 deals with via UTs is seL4_MinUntypedBits, which is 4.

Ah yes, sorry for being unclear, I meant the smallest unit on the VSpace facet of the API.

That's what most people would call a "page", with large and huge pages being the exception.

Indanz avatar Aug 23 '25 09:08 Indanz