In RFC 3407 (Explicit Tail Calls), there has been a discussion about whether stack consumption can be formally required. Specifically, while stack consumption has not been treated as observable so far, it seems useful to make tail call elimination mandatory rather than just optimization or quality of implementation.

"Formally required" may or may not have anything to do with operational semantics per se. minirust has a concept of StackFrame, but the idea that a StackFrame requires a certain number of bytes just to store the abstract data like func and caller_return_info is clearly in the domain of the concrete machine, and thus target-dependent. So the requirement may be better defined as part of what it means to be a conforming Rust compiler for a given target, similar to the handling of asm! or even command line arguments. Or it may be a guarantee given specifically by rustc (but not necessarily other Rust compilers), but I find that unsatisfactory.

Anyway, I am responding to this comment from @digama0, but I agree that the conversation is getting off-topic there, so I'm posting the response here.

@digama0 I see what you're objecting to.

Well, the idea that "a program which makes a finite number of non-tail nested calls does not consume an unbounded amount of stack" can be almost-equivalently expressed without infinity in this form:

• For a given implementation and program, there exists some number B such that for all executions of that program under that implementation, the total stack consumption (not counting consumption by unsized locals) is at most B times the number of nested non-tail calls.

Optimizations don't have to keep B the same, just preserve the property that some B exists.

Technically this definition is not equivalent to the "does not consume an unbounded amount of stack" definition, because that definition would allow stack usage to grow super-linearly (e.g. O(n^2) in the number of calls), while the new definition limits it to linear growth.

But B doesn't have to be anywhere near the actual number of bytes used by any particular function. It also doesn't have to be explicitly calculated. It just has to be an upper bound.

For an AOT implementation, B can be calculated relatively straightforwardly once you have the final program. Basically, for every machine code function, calculate its maximum stack usage, including all paths through the function. Then set B to the maximum of all those values.

Compiler optimizations are then handled as follows:

• Outlining: When calculating maximum stack usage of a function, also include the maximum stack usage of any outlined chunks that it might call, recursively. (There must be a maximum, or else you're saying that outlining could create infinite recursion where it didn't previously exist.)

• Inlining: Not a problem. Inlined calls use 0 bytes of stack, and 0 is less than B. The stack usage for variables from the inlined function was already accounted for in the calling function.

• Tail calls: If they're implemented as true tail calls at the machine code level, then no extra work is needed. If they're implemented by adding some extra 'driver' frame to the stack, then just add the stack usage of that to B.

Again, the important thing is not the value of B; the important thing is the fact that some procedure exists to calculate an upper bound. The procedure needs to account for all compiler optimizations that can change which concrete frames are created for a given series of abstract calls. If the procedure , then the compiler is correct.

But what about a JIT implementation, where the program might have their stack usage randomly changed on the fly when the JIT decides to optimize or deoptimize a function, potentially based on data measured during execution of the program? Well, it doesn't make too much difference. There must be some maximum amount of stack it could use for all possible compilations of a given program, under all possible measurement outcomes. The maximum may be impractical to calculate, but it exists. If not, then by definition there is some circumstance where you have unbounded stack usage. For example, an optimization that turns dynamically-sized heap allocations into stack allocations must have a limit on the size of allocations that are transformed this way, because otherwise you could get arbitrarily high stack usage by making larger and larger heap allocations.

(What if the JIT upgrades itself while the program is still running? Then you can still define B after the fact with respect to the 'implementation' consisting of the JIT plus all upgraded versions ever used. You have to include the upgrades in the implementation; you can't just say "an implementation is correct if it only upgrades itself to implementations that are also correct". Because otherwise you could have an implementation that 'upgrades' itself every second to a version that uses 1 more byte of stack than the last, or in other words, one that leaks stack at a rate of 1 byte per second. That can't be considered bounded.)