Statically compute upper bound for stack usage?

1

I understand, due to halting problem, we can not compute exact stack size usage.

However, is there a tool that can compute a upper bound for how much stack a function will consume in the worst case over all inputs ?

For example, a function that does not call any other function, in the worst case, uses O(1) stack space.

The motivation behind this is: for rust/wasm32, I'm somewhat concerned my functions might be "too recursive", so I'd like to have some tool that tells me which functions are O(1), and which functions are not. (If it can't distinguish O(log n) vs O(n), that is fine -- just knowing which functions are not O(1) would be useful enough.)

2

Even if it is O(1) making the stack usage bounded, the bound may still be too large.

3

The halting problem means that you can't compute an upper bound, not that you can't compute an exact number. Of course, it doesn't apply if you're working on a non-Turing-complete subset of language, but that subset must also forbid general recursion.

You could probably do some kind of estimation of stack usage, but I'd expect there are better ways to go about solving your problem. And I would not be surprised if such a tool, if it exists, would be heavily unmaintained due to its inherent unreliability.

4

It's not uncommon to do this for embedded firmware, and simply forbid recursion to make the analysis possible. One tool that can help with this is cargo-call-stack.

1 Like
5

You can absolutely compute an upper bound: +infinity.

6

Yeah, I think this is really the key. The moment we have recursion, it is hard to have any time of guarantee, so it boils down to "fixed # call stacks" vs "has recursion".

7

Ok, "least upper bound."

8

If we are looking at the space of functions from input to "stack size used", I believe the "least upper bound" is equivalent to "exact # of bytes this function call on this input takes" -- so it is equiv to computing the exact stack space usage.

9

Ah, you're probably right and I'm just being a goober. :slight_smile:

10

Any finite bound. If you could say "this halts within X steps or runs forever", all you would have to do to solve the halting problem is run it for X+1 steps.

For a more refined result, see this StackOverflow thread showing that if you could distinguish between programs that are O(n*n) and O(n*n*n), you could solve the halting problem.

11

Technically none of modern hardware is a TM. "Well what is it then?" I hear you asking. Technically each host is an LBA. The difference is that true TMs have infinite memory, which no physical machine has, nor will ever have.
The reason I bring this up is, the Halting Problem doesn't apply to LBAs. So at least hardware-wise it should be possible to calculate the amount of space used¹. It's a different story with software though, modern PLs and OSes seem to assume that there's infinite memory available (OOMs still aren't handled nicely in 2021, just causing massive slowdowns due to paging or just altogether crashing) and their conceptual models reflect that.

¹ Don't count on such a procedure being efficient in either time or space though.

I've run into this with a project at work. The most viable solution was a total rewrite that uses a heap-allocated stack to offload a bunch of state that used to be stored on the callstack. And as a result we don't run into stack overflows on WASM anymore.
The takeaway lesson was: if you need to deploy to WASM (or any other target that has limited stack space), dont write functions that can recur arbitrarily deeply.

2 Likes
12

I read an interesting paper a number of years ago (reference lost in the mists of time) describing a system that could prove if a given program halted. The authors could construct programs that the system could not prove, some of which actually halted, but all useful programs they tried had a proof. That sounds like something you could use.

13

Halting Problem is definitely "solvable" if the program is allowed to return {Halts, does not halt, don't know}. Any chance you recall the authors / searchable term?

14

Termination analysis or for something more general, formal verification.

15

Sorry, no. I tried some of the obvious search terms before posting.

16

I mean, the Rust compiler is also an example of this kind of thing. If it says that it compiles, then it has no memory safety bugs, but if it says that it doesn't compile, then it might or might not have memory safety bugs.

1 Like
17

Due to drop handlers, is it possible to have 'innocent' looking code that blows up the stack?

fn looks_innocent(&mut self) {
  self.blah = None; // BAM, triggers drop handler
}

and then this drop handler might in turn free up other resources, causing other drop handlers to trigger ...

Hypothetical, but in theory possible right?

18

Drop handlers are ordinary functions, so yes, they can blow up the stack. For example, drop handlers that blow up the stack is the topic of this chapter from Learn Rust With Entirely Too Many Linked Lists.

1 Like
19

FML. I'm not using linked lists, but I have a DAG, where nodes have drop handlers, so when the "linchpin" is freed, there is going to be a callstack worth of drop handlers O(depth of DAG) tall. FML.

1 Like
20 
pub struct BadStruct(Option<Rc<BadStruct>>);

#[test]
fn it_works() {
    println!("start");
    let mut obj: BadStruct = BadStruct(None);
    for i in 0..1_000_000 {
        obj = BadStruct(Some(Rc::new(obj)))
    }
    println!("done");
}

I can't believe I did not realize this until now, but we don't even need customer drop handlers to blowup the stack. Just using the existing ones suffice.

EDIT: Just realized, this is basically identical to the linked-list example @alice cited above.