cost type for Space - how does a suitable cost modell look like for LLVM?

[maxhaslbeck]

In

isabelle_llvm_time/thys/vcg/Sep_Generic_Wp.thy

Line 476 in b76f6ff

section \<open>experiment: cost type for Space\<close>

we define a cost type for space. It could be used to reason about space consumption of LLVM programs, similarly to time.
Abstract arguments should be moved upwards to the level of NREST. There an analog concept should exist.

what would be a suitable cost model for space in LLVM?
counting the number of words occupied?

[lammich]

The bytes of allocated memory on the heap can be precisely measured. The real size will only contain an memory-manager implementation specific overhead. Stack space is harder to measure: variables might be held in registers (decreases actual space), or be subject to architecture specific alignment constraints (increases actual space). I think, however, that a safe over-approximation by a constant factor is possible. Another problem with stack space is that we don't see variables in the shallow embedding at all.