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)
@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 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!