In contrast to VSU_stdlib which axiomatized malloc, free, and exit as external functions, in this chapter we construct them as ordinary C functions, and prove them correct. This chapter shows how to manage global variables that are private to a module. In the C code, there is a stdlib.h interface, with alternative implementations stdlib.c and stdlib2.c that are quite independent of each other. The the proofs, there is a specification Spec_stdlib.MallocFreeASI (that is, the "malloc-free Abstract Specification Interface") with two alternative implementations-with-proofs, VSU_stdlib.MallocFreeVSU and VSU_stdlib2.MallocFreeVSU. That second VSU is the one we build in this chapter.

The C program

Here is our C program. Notice the variables pool, pool_index, freelist that are global to the module, but meant to be private--not to be directly manipulated by clients of the module. Furthermore, these variables have initial values (pool_index=0, freelist=NULL, and pool zero-initialized implicitly) that represent a meaningful initial state.

/* stdlib2.c */
#include <stddef.h>
#include "stdlib.h"

struct cell {struct cell *a, *b, *c, *d;};

#define N 80000

struct cell pool[N];
int pool_index = 0;
struct cell *freelist=NULL;

void *malloc (size_t n) {
  struct cell *p;
  if (n>sizeof(struct cell)) return NULL;
  if (freelist) {
    p = freelist;
    freelist = p->a;
  } else if (pool_index < N) {
    p = pool+pool_index++;
  } else p=NULL;
  return (void* ) p;
}

void free (void *p) {
  struct cell *pp = p;
  if (pp==NULL) return;
  pp->a = freelist;
  freelist=pp;
}

void exit (int n) {
  while (1) ;
}

As you can see, malloc can allocate blocks whose size ranges from 0 to sizeof(struct cell), that is, up to four words long. Any malloc request larger than that will return NULL, which is legal behavior for malloc. Furthermore, the maximum size of the pool is N=80000, beyond which malloc will return NULL. The exit() function infinite-loops, so that it satisfies its postcondition of False in our Hoare logic of partial correctness.

The normal boilerplate

As usual, we define representation relations. First, for the free list, which is just a linked list much as in VSU_stack.

malloc_token

Suppose the user does p = malloc(7);. Then p points to a newly allocated block of 7 bytes. What does malloc_token(p) represent?

• Normally, there must be some way for free(p) to figure out the size of the block. This can be done by having a header word, just before address p, that gives the size (though there are other ways to do it). Normally, this header word is part of what malloc_token represents. But in this implementation, all blocks are the same size, so there's no need for such a header.
• The memory-manager's free list contains blocks all of size sizeof(tcell), which is 16 bytes when sizeof(size_t)=4 or 32 bytes when sizeof(size_t)=8. When malloc(7) splits a block into two pieces, the malloc_token represents the second piece, the portion of the block between offset 7 and the end. That is the memory_block shown in the definition below.
• In addition, the malloc_token has three propositional facts about address p, that will assist the free() function in reconstituting the two parts of the split block.

Exercise: 2 stars, standard (malloc_token_properties)

The next three lines define an opaque constant that, nevertheless, rep_lia can unfold. See VC.pdf, chapter 65 "Opaque Constants".

Digression (feel free to skip this)

Suppose someone changes the source program stdlib2.c, putting a different constant than 80000. You would like your verification script to automatically adjust. We will revise the line, Definition N : Z := ... to find the constant automagically. Step one is to find the constant. You can look in stdlib2.v, which is produced by CompCert clightgen from stdlib2.c, for the variable definition v_pool. And now look where the number 80000 appears in gvar_info(v_pool):

It's easy to extract that number automatically:

The following definition of N won't work well, because N will not be a constant, it'll be a match expression:

So instead, use this Coq trick:

Now, throw away N'' and we'll combine the two tricks together:

• opaque_constant to define a constant that won't unfold except by explicit rewriting; and
• extract the value of the constant from the program itself.

End of digression. Aren't you glad you skipped it?

Defining the mem_mgr APD

This mem_mgr predicate is the client-view abstract predicate that characterizes the contents of this module's global state variables, pool, pool_index, and freelist.

Constructing Vprog and Gprog

Exercise: 3 stars, standard (stdlib2_body_malloc)

Exercise: 3 stars, standard (stdlib2_body_free)

Exercise: 2 stars, standard (stdlib2_body_exit)

Initializers for global data

Each VSU may have private global variables that constitute its "local state". The client of the VSU should not access these directly; and in separation logic all these variables should be abstracted as a single abstract predicate. Since these variables may have initial values that concretely represent some abstract state, we need an axiom in the VSU interface (proved as a lemma in the VSU implementation), saying that the initial values properly represent a proper state of the abstract predicate.

Exercise: 2 stars, standard (stdlib2_initialize)

Defining the pieces of a VSU

And now, in the usual way, we can put totether the pieces:

Constructing the Component and the VSU

Next Chapter: VSU_main2