Frequently asked quesions about LFD:

• Why must all heap cells be of the same size?
  Because a heap cell should represent the smallest atomic heap portion that might be allocated, such as a byte or a word. However, in some examples we voluntarily choose a bigger size since we are interested in a different memory model, e.g. in the uniform memory model, where we assume that a single cell is big enough to hold any node. Equivalenty we could assume for the uniform memory model that each node occupies x cells rather than a single cell, which would yield the same result multiplied by x.
• Do different memory models affect the generated LP?
  Changing the memory model will result in some changed constants within certain inequalities, but the constructed linear programs will be structurally equal.
• What are the benefits of the uniform memory model?
  The uniform memory model, where all data nodes occupy the same number of heap cells, has the advantage that there is no need for heap defragmentation. It is the preferred memory model for Camelot, as it fits the Java memory model quite well: all classes are assumed to inherit from a common object and are thus interchangable memory-wise.
• What about memory fragmentation?
  Non-uniform memory models give rise to the question of memory defragmentation, which we leave unanswered. One reason being that our main application, Camelot, prefers a uniform memory model anyway and the other that defragmentation is rather a question of time than space.
• Safe deallocation is vital for the derived heap bounds, how can you ignore that?
  We cannot, but the problem of statically guaranteeing safe deallocation is difficult enough to be treated on its own, as existing works show. These existing works solve the problems with different trade offs, yet our work builts on top of any arbitrary solution to this problem.
• How is in-place updating achieved? Our system treats an update of a node of a data structure on the heap simply as destroying and building anew. Since we are only interested in the overall balance of used heap cells we abstract away from heap addresses. We speak of an in-place update of e.g. a list in a sorting algorithm, if for each list node allocated another node was deallocated before. Hence the number of live heap cells never exceeds the initial value during the whole computation. Whether a real execution reuses or disposes a specific address is not of importance to our statical analysis.
• How can you call your system efficient, when one example requires 17 minutes of real time?
  First, we see that the time required to complete the analysis and to built the LP grows linearly in the size of the program, hence scales well. Second, our system does not incur any runtime overhead, so the time is spent at compile time: Either to produce a certificate to be shipped with the program or to guide a programmer to optimize his code. The 17 minutes realtime refer to a very huge worst-case example on an average laptop computer, which we still deem acceptable for a compile time. All other examples were dealt with within less than a single second.
• Why is there no runtime overhead?
  Our system is solely a statical analysis of a given program. Code is never changed, only examined. Thus our system might be used to guide a programmer to optimize the heap space consumption of his program; or to convince someone else to run a program within an environment where heap space is a valued resource.
• Can I fool your system by stack-allocating as much as possible?
  Sure, but why would you want to do that and thus ignore the help our system offers? One should rather restrict programming to known methods which minimize stack allocation, such as tail-recursion, in order gain a good understanding of a program's true memory consumption.
• Why is your statical analysis modular?
  Despite the necessary code transformation, each constructed linear inequality of the LP can be traced back to a single instruction within the source code. All constraints generated individually without a global view of the program: a change to a function of a program does not affect the constraints generated for the rest of a program. However, the LP must be solved as a whole at once for a program.