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

@Moore How do you envision statically checked memory management working? Are you satisfied with Rust?

@xentrac the easiest way is to statically allocate everything but that can lead to more allocations then strictly necessary if there are two allocations that never overlap in use.

Another idea is to have an allocator as an explicit argument and add capacity to the type of the allocator and an API like:

let (value, allocator) = Box::new(allocator);

This way it would be a type error to over commit.

@xentrac Another idea is that if you have something like an event loop you can require all functions to be total and then use static analysis to compute the worst case allocation which would be easy if you used a bump allocator in the event loop. (Long lived allocations would need to be moved to statically allocated structures before returning out of the event loop.)

Really the root idea is no computer has infinite memory, so why do we write programs like they do.

@Moore perhaps by coincidence, last week I was working on a purely functional language called 5emel, which has an event loop and does its heap allocations initially with a bump allocator and then moves long-lived allocations out of the bump-allocated region. But it's the minor garbage collector that moves the surviving objects into the main heap, it features general recursion, and it's dynamically typed, so it's sort of the opposite direction from what you're talking about.

The 5emel event loop is there to make it possible to write purely functional programs that do things like read and write files. So I have programs that look like:

def main(:state, :ev) =
| Start { [:argv0, :infile, ...:args] } = ev;
Do { Open { infile, "r" },
Starting { infile, args } }
| Opened { :fd } = event;
Do { Read { fd } , Reading { state } }

and so on. The runtime invokes main() repeatedly with I/O events, and it's expected to return a Do with an action and a next state, a process which generally involves pattern-matching on the I/O event.

If it were a Total Functional Programming system, you could guarantee that it would periodically return to the event loop, and maybe do the worst-case allocation analysis there. But that would involve a static type system, and probably a dependent type system at that.

@xentrac I have built out some language experiments that make functions " trivially total" by removing recursion and unbounded iteration. So it has foreach but not for/while/ect.

The top level of a program is an explicit state machine. This means at the top level it is unbounded in scope but static in memory, which then call total event holders which are bounded in scope and memory. You can play with it here:

https://0xa9f4.com/playground/

@Moore Ooh, this sounds really interesting!

@xentrac it is just garbage code to try out ideas.

@Moore I'll try it out!

@xentrac here is the repo with more info:

https://github.com/moore/langlog

Just to set expectations this is mostly AI generated code to play with ideas. This is nowhere near anything anyone would want to use.

@Moore Yeah, 5emel is too.

@xentrac I would be interested to look at it if you have anything to share.

@Moore The current version of 5emel (100% #AI output) is in https://canonical.org/~kragen/sw/5emel-m5d.1.tar.gz. Example 5emel programs include zero-dependency unzip, TrueType text rendering, PNG encodng, and the 5emel compiler.

The REPL is pretty bad; the in-browser notebook interface (build/notebook.html) and the native-code compiler are better. The build requires make, tsc, awk, node, and cc (to assemble the compiler's assembly output), and it's kind of annoyingly slow because it runs a lot of regression tests under the interpreter, which is slow partly because it's written in TypeScript. The test run is the default when you type `make`, and it takes about 15 minutes on my laptop.

The main question 5emel is trying to answer is whether automatic memoization can yield usable performance in a mutation-free eager pure functional language. This sort of presupposes a decent garbage collector and at least a basic native-code compiler, though, and those may actually matter more than the automatic memoization, and, so far, not in a good way! Programs written in 5emel are still several times slower than similarly-structured programs written in C and compiled with optimization, 8× on average, and sensibly written programs in C are typically 20× faster.

I still need to write this up properly. If you try it out, your feedback will be very valuable!

@Moore
I think the basic answer to "Why do we write programs like the computer has infinite memory?" is a little complicated.

In what I think you're calling "system programming", we write programs because we know what they will output, and we want them to output it reliably, without failing. For example, firmware for a motor controller. In those cases it is very bad to write programs like the computer has infinite memory, because it means those programs will fail sometimes, and we don't want them to fail.

Other times, though, we write programs because we *don't* know what they will output, and we are running the program to find out. Like, if you already have the output that a compiler will produce in a given case, there's no point in running the compiler on the same input again. In those cases, it's very helpful to be able to pretend that the computer has infinite memory, because usually we have a pretty good plan for what to do if the program fails.

This dichotomy is more glib than the reality, of course, and there are lots of complexities and fuzzinesses, but I think these two general attractors do sort of exist in the real world.

@xentrac my hypothesis is that with advances in programming languages we can get ergonomic programming environments that produce programs that cannot crash outside of hardware faults. You could give them input that is too large to process but that they would always return with an error that explains what would be required to succeed.

@Moore hmm, so like a dependent type thing where "allocator" is a dependent type with an integer parameter, or something?

@xentrac yes

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

@xentrac @Moore Haha yes I was using a fairly expansive view of what might constitute a heap!

@tonyg @Moore If I can be a little mischievous, it sounds like your view of what might constitute a heap is so expansive that it probably includes program stacks!