A single memory region may use both normal and device memory

[dreamliner787-9]

For example, if seL4 gives userspace these untypeds:

Normal: [0x0 ... 0x200_000)
Device: [0x200_000 ... 0x201_000)
Normal: [0x201_000 ... 0x400_000)

It is technically valid for a memory region to use both type of untypeds, for example [0x100_000 ... 0x300_000). All Microkit releases < 2.1.0 does not have this problem as they allocate Frame objects for a memory region from a single untyped. But with the capDL integration in >= 2.1.0 this is no longer the case. Which caused weird issues for me such as a VM hanging when guest RAM used both normal and device untypeds.

The first problem is that there is no way for the user to tell the tool whether they want a memory region to be allocated from normal or device untypeds. They get automatically allocated by the capDL initialiser's algorithm.

Secondly we should add a way of detecting this issue and print an error message. This is not too hard on ARM and RISC-V since the tool already emulated the kernel boot process to obtain the list of untypeds that you will get at run time.

But on x86 it is unclear to me what is the best way to solve this problem since you don't know the memory map at compile time. The cleanest way I could think of is that we add a device: bool attribute to the Frame spec object to restrain the capDL initialiser from mixing untypeds.

[lsf37]

But on x86 it is unclear to me what is the best way to solve this problem since you don't know the memory map at compile time. The cleanest way I could think of is that we add a device: bool attribute to the Frame spec object to restrain the capDL initialiser from mixing untypeds.

I might be wrong, but I thought that already existed. Is that just a thing that is not yet implemented in the Rust version or missing overall? The capDL formalisation of FrameCap definitely has a device flag. The frame object currently does not.

[dreamliner787-9]

I think it's missing overall. The C capDL loader have this:

typedef struct {
    CDL_FrameFill_Element_t fill[CONFIG_CAPDL_LOADER_FILLS_PER_FRAME];
    seL4_Word paddr;
} CDL_FrameExtraInfo;

The Rust implementation is similar:

pub struct Frame<D> {
    pub size_bits: u8,
    pub paddr: Option<Word>,
    pub init: D,
}

From my understanding and I could be wrong, where they diverge is their allocation algorithm. The C one does this and allocate out of device untypeds for any objects with a paddr attached :

bool isDeviceObject(CDL_Object *obj)
{
    return CDL_Obj_Paddr(obj) != 0;
}

Where as the Rust implementation will allocate objects with paddr out of whichever untyped that can satisfy the allocation. Which is where the problem comes in. I don't think it is a good idea to copy the C implementation's strategy since it is valid for the user to allocate normal memory at a fixed physical address.

[Indanz]

But both only allocate from device memory when the user ask for a specific physical address? So you get what you asked for? Doesn't look like the problem is with capDL then.

[dreamliner787-9]

only allocate from device memory when the user ask for a specific physical address

Yes that is the C version's behaviour. But the Rust one can allocate from normal untyped if the object's physical address is within a normal untyped's physical address range.

So you get what you asked for?

In this case, technically yes you will get what you asked for, but the end result might not be what you expected. Since your memory region is now using both untyped and device memory.

[Indanz]

only allocate from device memory when the user ask for a specific physical address

Yes that is the C version's behaviour.

And the Rust one's too. Or are you claiming the Rust version may allocate from device memory when a physical address is not specified?

But the Rust one can allocate from normal untyped if the object's physical address is within a normal untyped's physical address range.

But if the user asks for that, you can either error out, like I suppose the C version does, or honour the request.

So you get what you asked for?

In this case, technically yes you will get what you asked for, but the end result might not be what you expected.

Why? I ask for a specific memory region and get it, what's unexpected about that?

Since your memory region is now using both untyped and device memory.

Ah, so the actual problem is overflowing from one type into another type of memory. Yes, agreed that the allocator should probably stay within the same UT type for one range, as that's likely a user error.

The first problem is that there is no way for the user to tell the tool whether they want a memory region to be allocated from normal or device untypeds. They get automatically allocated by the capDL initialiser's algorithm.

I disagree with this, the user can specify that by providing physical address. Users never get device memory when they don't specify a physical address, and if they do, they should know what it is.

Secondly we should add a way of detecting this issue and print an error message.

That should be easy enough, just remember the initial UT's type and check that for further allocations.

That said, this is only a problem if the user gets the size of their memory region wrong, for something that should be thoroughly checked by the user already, so I wouldn't put much effort into adding extra checks for catching this corner case.

[dreamliner787-9]

And the Rust one's too. Or are you claiming the Rust version may allocate from device memory when a physical address is not specified?

For the Rust one, if you don't specify a paddr, then an object will be allocated from any normal untyped. If you do specify a paddr then it will be allocated from an untyped that can satisfy the allocation, regardless of whether its normal or device untyped.

Ah, so the actual problem is overflowing from one type into another type of memory. Yes, agreed that the allocator should probably stay within the same UT type for one range, as that's likely a user error.

Yes that's right.

I disagree with this, the user can specify that by providing physical address. Users never get device memory when they don't specify a physical address, and if they do, they should know what it is.

Ok that's fair, still, my goal is that I want to print some warning when the user find themselves a situation like this.

That should be easy enough, just remember the initial UT's type and check that for further allocations.

For ARM and RISC-V this will work since we can do it in the tool. But the problem is on x86, we don't know the memory map at build time, and the capDL initialiser doesn't know about memory regions. It just knows that you want Frame objects, and some of them at certain physical addresses. That's why the mixing of memory type within one memory region is possible now since allocation is at object rather than region granularity. So I'm not quite sure what's the best way to convey this higher level information to the initialiser via the spec without bloating it too much.

[Indanz]

But the problem is on x86, we don't know the memory map at build time, and the capDL initialiser doesn't know about memory regions. It just knows that you want Frame objects, and some of them at certain physical addresses.

But exactly because you don't know the memory map beforehand, on x86 there shouldn't be many fixed physical addresses requested, so it should be less of a practical problem. That is, it's fine to ignore this for x86 and not warn, because people shouldn't use static addresses on a dynamic system.

[midnightveil]

Something that might be a factor (which I think is a ailly design) is that the way to allocate a frame that lies within contiguous physical memory is to specify a physical address. This forces you to specify this if you want this property, such as for DMA (without IOMMU able to remap DMA addresses).

microkit/docs/manual.md

Line 225 in 1d0d3e4

Typically, memory regions with a fixed physical address represent memory-mapped device registers or DMA regions.

This is something I've disliked since the move to capDL, because like Indan said: there's almost no reason to want a specific physical address except for MMIO peripherals: for DMA you should only ever want to know what it is, you shouldn't need to care. (Prior to capDL, because we only allocated from one UT, everything was contiguous. And this feels like making a (bad) part of sdfgen where we hardcode physical addresses of most memory regions so that we can patch in that metadata (and thus not even use microkit's setvar). Which can't possibly even work on x86, so all our x86 sDDF examples currently hardcode all the details of everything because we can't deal with that.