RE: https://social.rust-lang.org/@rust/117605013073050966

I'm not sure whether I'm more excited about the stable never type, or DropGuard in std.

Which is a reminder that I'm kind of strange, since the word "allocator" didn't appear in that sentence. 🤪

@cliffle allocators are runtime type checking and we would be better off without them. (In system programming)

@Moore @cliffle I think this is a reasonable point of view, but I don't know if it's correct yet. What do you think about the seL4 approach to resource management?

@xentrac I have not worked with it but have been following it. It looks interesting.

@Moore I haven't tried installing seL4 either, but I mean, what do you think about its approach to resource management, in the abstract?

@xentrac I don't know enough to have an option but it looks interesting. The time accounting is interesting.

@Moore An interesting thing about that is that they only enable the time accounting for "mixed-criticality systems", where you're relying on the kernel to prevent your Linux virtual machine or whatever from causing glitches in your motor control waveforms or 802.11 acks.

But the main interesting thing about the kernel in this context is that it doesn't allocate memory at runtime. There's no heap.

@xentrac @Moore I don't know if I would look at it that way: another perspective is that it has first class heaps as capabilities. And method invocations analogous to calloc/free (but safe). After all, no kernel has a heap unless it implements it's own; this one is just ocap style

@tonyg @Moore Most kernels do implement their own heaps, though, while, as I understand it, seL4 leaves that to userspace. As a result, seL4 system calls cannot fail due to running out of memory. The kernel doesn't have a "heap" capability type, either. Maybe I'm not understanding what you mean.

@xentrac @Moore Ah, I see. Yeah the kernel cannot fail due to no-memory-available; allocation calls done by userspace can fail. It's a heap still, but the difference is that the kernel never calls those APIs. So I may have misunderstood the scope of your remark, in which case oops and I retract everything :) The capability type I am meaning is "Untyped".

@tonyg @Moore Right, only userspace calls the Retype call on Untyped. That *can* fail with `seL4_NotEnoughMemory` (cf. https://sel4.systems/Info/Docs/seL4-manual-latest.pdf#page=125) but, as I understand it, that's something that the userspace code can predict in advance. It probably indicates a bug in the userspace code that called it; it doesn't call a heap allocator inside the kernel that might or might not succeed. It just advances the "watermark" bump pointer toward the end of the Untyped, which will start failing at a predictable moment.

The heap, if any, needs to be in the userspace code, and that's why the kernel never calls the heap-allocation APIs — they may not exist at all, and the userspace code is free to structure them however it pleases, and at any rate the seL4 kernel never calls into userspace.

@tonyg @Moore But maybe you mean "heap" in a sense that's broad enough to encompass allocation arenas that can't deallocate things — like the "per-frame heap" in many games or the nursery of many generational garbage collectors? In which case, oops, and I retract everything!