This project is read-only.

Verifying that there are no memory leaks

Mar 31, 2011 at 1:16 AM
Edited Apr 1, 2011 at 1:02 AM

Are there samples which show how to verify that a set of functions does not leak memory?

I am thinking about using VCC to verify the sources of a MySQL user-defined function plug-in, which follows the contract:

  1. myfunction_init is called once
  2. If myfunction_init did not return an error, myfunction is called once
  3. If myfunction_init did not return an error, myfunction_deinit is called once

In myfunction_init I need to allocate memory that is freed in myfunction_deinit.

Is there a way to verify that this set of three functions does not leak memory?

Daniel

Mar 31, 2011 at 10:23 PM
Edited Mar 31, 2011 at 10:23 PM

Hi Daniel,

  unfortunately, VCC doesn't yet provide any built-in support for this, i.e., there's no way talk about the allocated objects (and bound their number / size) or to enforce that all these objects are freed, say, at program exit. Something could be done with custom contracts for malloc() / free() (and additional state) instead of the custom hardcoded one. Anyway, a basic pattern for annotating your functions above in VCC is shown below. However, there's nothing in there to prevent leaks, i.e., each function could do additional unwanted allocations on the side.

Cheers, Mark

#include <vcc.h>
#include <stdlib.h>

typedef struct mystate {
  int a;
  _(invariant a == 42)
  _(invariant \malloc_root(\this))
} mystate;

mystate *init()
  _(ensures result != NULL ==> \wrapped(\result) && \fresh(\result))
{
  mystate *result = malloc(sizeof(mystate));

  if (result != NULL) {
    result->a = 42;
    _(wrap result)
  }
  return result;
}

void use(mystate *s)
  _(maintains \wrapped(s))
  _(writes s);

void deinit(mystate *s)
  _(requires \wrapped(s))
  _(writes s)
{
  _(unwrap s);
  free(s);
}

void main() {
  mystate *s;
  s = init();
  if (s != NULL) {
    use(s);
    deinit(s);
  }
}

Apr 1, 2011 at 12:49 AM

Hi drtrebbien,

in principle instead of using the VCC-provided malloc you could build your own malloc and thus be able to speak about the memory on the heap. Although this might be a bit overkill for your purpose, in the context of an embedded system I gave a talk on this this morning at AMICS/ISORC, see http://www-wjp.cs.uni-saarland.de/publikationen/Baumann-AMICS2011.pdf that also contains a link to code (note to self: I should have better announced this before giving the talk ...).

This would strengthen Mark's init() function by the precondition that if there is something in your memory manager, then you get the memory desired, and then you could go into the main() function with the precondition that there is something in your memory manager and you could skip the "if (s != NULL)" precondition. As I said probably overkill, but in principle, depending on what you aspire, nice things are very doable ...

Best, Holger

Apr 1, 2011 at 12:54 AM

There is a more fundamental problem with detecting memory leaks within VCC: in a concurrent setting, we have to be able to move ownership of a wrapped object to a closed object (set_closed_owner) - e.g., to give a lock ownership of its protected object - and this can create a cycle in the ownership graph. Preventing this would require reasoning that an object is not in the ownership domain of another object, which is painful in the VCC paradigm of "disjointness only where it is needed" (as opposed to the CSL paradigm of "separation everywhere"). If ownership was indeed acyclic, then a simple way to guarantee memory hygeine would be to require threads to have empty ownership sets when they are destroyed. One reason that we haven't gone this route (besides having a number of higher-priority items to work on first) is that its not clear that we want to keep ownership around long-term.

You can, of course, guarantee freedom from memory leaks on your own by guaranteeing that, on shutdown, every malloc has been freed (i.e., the set of malloc roots is empty). You would have to roll your own tree-like ghost structures (e.g., using claims) in order to maintain what amounts to an acyclic ownership relation.

Apr 2, 2011 at 11:40 PM

Hi Holger,

I am glad that you linked to your paper, "Proving Memory Separation in a Microkernel by Code Level Verification", because I was interested to read about a real-world application of VCC to verifying parts of microkernels. Just a few weeks ago I had read about the seL4 project, so it was fresh in mind that formal verification techniques are well-suited to microkernel development, and that microkernels can benefit from formal verification.

Out of curiosity, does your approach to formalizing PikeOS' page allocator also verify that the page allocation functions are re-entrant?

Daniel

Apr 4, 2011 at 6:29 AM

Hi Daniel,

thanks for your interest. As written in the paper (assumption A_{2}) we require that on entering *_alloc, *_free interrupts are disabled. In VCC annotations that is corresponding to the strong assumption "maintains(wrapped(partition))". So the answer to your question is "no". While it is possible to specify "atomic" blocks within functions in VCC, on a quick reflection I am also not aware of any way to specify reentrancy (or non-reentrancy) at the function contract level in general (but might be overlooking sth). Best, Holger

Apr 4, 2011 at 12:58 PM
Edited Apr 4, 2011 at 1:05 PM

Hi Daniel,

the formal verification of interruptible code is a research topic I'm currently working at. While VCC has no notion of interrupts and interrupt handling per se, it can be used to verify the interrupt handler and interruptible thread separately as two concurrently running threads. This is sound if one models the particular data access policy between the two threads correctly via ownership invariants and one throws in a few additional software conditions which might not be provable in VCC (compiler-related issues). I won't go much into details here as the topic is quite involved. 

Concerning the specification of the system's behaviour one would encode the possible transitions/atomic updates on the data using volatile ghost abstractions with two-state invariants. The actions of the interrupt handler become visible to the interuptible thread when it reacquires ownership of the shared data, i.e. by disabling interrupts or setting up a guard for the data so that the interrupt handler won't touch it. 

For reentrant functions - similar to such functions accessing volatile shared data in an atomic block - you would have to argue that 1. all your atomic actions on the shared data obey its two-state invariant, 2. that the system invariants are preserved by the function (as pointed out by Holger) and 3. assert in the function contract that the summary of updates in the post state (as seen by the executing thread) actually reflects the desired functionality.

If there is only one atomic access this is quite easy. if you have an involved reentrant implementation with several non-interfering atomic accesses you should be able to prove that your post-condition holds from the two-state invariants that reflect the handler's behaviour which are triggered between the atomic accesses.

Admittedly this is still quite abstract. I hope I can come up with a demonstrating example in the near future. However at the moment I'm occupied justifying the whole approach formally. In case you have further questions on the issue, feel free to contact me.