How to see memory usage

Stream: new members

[Asei Inoue]

This is a code which causes stack overflow error:

/-- non tail recursive function -/
def naivePower (x n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => x * naivePower x n

-- stack overflow !!
#eval naivePower 2 10000

Each recursive call increases memory usage, which leads to a stack overflow.

My Question:

Can the Lean code find out how much memory is being used by the execution of a particular function in Lean?

[Henrik Böving]

That's not possible.

[Asei Inoue]

Impossible in any programming language?

[Asei Inoue]

@Henrik Böving Thank you.

Can't we even check with the code without making an error that memory usage is increasing with each recursion?

[Henrik Böving]

There are so many open questions here. For one what do you mean by "find out how much memory is being used". Do you want this to happen at compile time? Then it's an undecidable problem in general but may be approximated for certain functions. If you want to decide it at runtime it depends on which kind of memory you are interested in. In this situation we would care about stack memory. We can figure that out by looking at the value of the stack pointer at different times while executing the program and thus figure out how much additional stack memory was allocated since then. This would require a bit of assembly code (maybe there is also some C libraries that already have the assembly code underneath). For heap memory you'd need to check the statistics of malloc but in multi threaded code you need to be careful about not counting memory that is consumed by other threads as well.

[Asei Inoue]

Thank you.

Do you want this to happen at compile time?

It would be nice to be able to check with #eval without compiling.

[Henrik Böving]

But #eval is already compiling and evaluating code?

[Asei Inoue]

But #eval is already compiling and evaluating code?

Oh, I seem to have misunderstood the behaviour of #eval.

I thought #eval was just running in the interpreter.

[Henrik Böving]

Yes but in order to run the interpreter the code needs to be compiled into bytecode already.

[Henrik Böving]

And I still don't really see what you are asking for. Do you want a static analysis that can tell you whether a function will fill up stack space or do you want something dynamic that checks at runtime how much stack space is currently in use?

[Asei Inoue]

do you want something dynamic that checks at runtime how much stack space is currently in use?

My motivation is to see how memory is wasted by not being tail-recursive. So I want to see something dynamic.

[Henrik Böving]

Do you know the difference between a static and a dynamic analysis?

[Asei Inoue]

Do you know the difference between a static and a dynamic analysis?

I honestly don't understand it.

[Henrik Böving]

An analysis is called static if it gives a result by just looking at the code itself while a dynamic analysis gives a result by executing the code.

[Asei Inoue]

An analysis is called static if it gives a result by just looking at the code itself while a dynamic analysis gives a result by executing the code.

It matches the image I had somewhat in mind.

[Henrik Böving]

Which one?

[Asei Inoue]

Which one?

both. My previous understanding of static and dynamic analysis seems to have been generally correct.

[Henrik Böving]

Yes but which one do you want for your use case here?

[Asei Inoue]

dynamic...?

Is it possible to find out how much memory is being used statically, i.e. without executing any code?

[Henrik Böving]

Is it possible to find out how much memory is being used statically, i.e. without executing any code?

Generally that is undecidable but we can decide for lots of functions (such as the one above) how much will be used at most with some effort.

dynamic...?

Okay so you wish to run something along the lines of

#resources func arg1 arg2 arg3

and be told how much stack and heap memory it uses?

[Asei Inoue]

but we can decide for lots of functions (such as the one above) how much will be used at most with some effort.

wao!!

and be told how much stack and heap memory it uses?

Yes.

[Henrik Böving]

Okay, for heap memory C provides the necessary APIs and we could lift them into surface level Lean in theory. For stack memory figuring out the maximum amount of stack memory used without touching the function that you want to look at is not nicely doable. If you want to touch it on the other hand it would be doable with some C as well.