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

[midnightveil]

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.

[Indanz]

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.

[nspin]

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?

[Indanz]

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

[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.

[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.

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