When C code allocates on the Coq heap

A Coq data structure is one built using OCaml-style representations, traversable by Coq or by C code. Coq always builds its Coq data structures on the garbage-collected heap. C programs may build such data structures either on the g.c. heap or outside the heap (in extern global memory or in malloc/free memory), each with its own special discipline that must be followed.

Building Coq data structures outside the Coq heap

C programs may build Coq data structures outside the g.c. heap, and the Coq programs can traverse such structures without problems. These are called "outliers". But such structures must not point into the g.c. heap unless special care is taken; see below under "global variables that point into the Coq heap."

For example, one simple model of calling Coq from C is: build a query in the form of a Coq value, using Coq data structures outside the g.c. heap. Pass the root pointer to the Coq program, which will build its answer on the g.c. heap and return it. Then the C program can traverse the response.

This is a quite simple model, and it allows the C program to almost ignore that there is a garbage collector at all. To use this model, build the query data structure using the "C heap" forms of glue-code constructor functions, such as make_Coq_Init_Datatypes_list_cons described in the Glue Code and FFI chapter. Call the top-level certicoq-generated C function, passing the root of this data structure as an argument. That function will create its own g.c. heap, run, and return a pointer into that g.c. heap. Then the C code traverses the answer, oblivious of the fact that it's in the g.c. heap. Finally, the g.c. heap can be deallocated with free_heap(h); or it can be reset by calling reset_heap(h); before the next call to a Coq function.

This protocol avoids all problems with calling the garbage collector from C, or (from C) calling functions that call functions that call the garbage collector, because there are never any non-outlier pointers within C variables at the time the garbage collector runs.

C programs that allocate on the g.c. heap, or call Coq (or the garbage collector) while retaining non-outlier pointers

Some C programs need to interact more intimately with Coq functions: for example, if the C function is a primitive called from Coq, or if the C program calls Coq while retaining a pointer into the g.c. heap, or if the C program calls the garbage collector directly. (The protocol in the previous section avoids all these situations.)

In a garbage-collected language, the collector needs to be told where all the roots of the graph are, within the stack or local variables of the executing program. Source languages that are designed to be garbage-collected have compilers that produce stack-maps showing where are all the pointers. But C is not such a language, and C compilers do not produce such maps. Therefore we adapt a technique from McCreight, Chevalier, and Tolmach: we embed a linked list of root-pointer frames within the stack frames of the C functions, in source code.

C functions participating in this protocol take an tinfo argument of type struct thread_info *. Within the tinfo are pointers to the garbage-collector's heap-management data as well as the stack of root-pointer frames that the C program must manage.

Local variables that point into the Coq heap

When we enter the C function, we can assume that all the C and Coq functions below it on the stacks may have local variables that are live pointers into the g.c. heap; and that these are recorded in the stack-of-frames. If the C function calls the garbage collector, or calls another C or Coq function that might eventually call the garbage collector, it simply passes this tinfo along.

But if the C function creates or retains (in its own local variables) pointers into the g.c. heap that are live across a call to (a function which might call) the collector, then it must record these pointers into a new frame on the stack-of-frames before the outgoing call, and then fetch these pointers back (popping the frame) after the outgoing call. "Live across the call" means that the value of this local variable might be used by the C function after the called function returns.

Each frame in the stack-of-frames looks like this. In the local variable declarations of the C function we have:

value roots[N];  /* N is the largest number of live roots across any outgoing call in this function*/
struct stack_frame fr;
fr.root=roots;
fr.prev=tinfo->fp;
/*  fr.next is left uninitialized right now */

Now, suppose we call an outgoing function g(x,y), such that variables a,x,z (but not y) need to be preserved across the call and could possibly be pointers into the g.c. heap. Purely integer and outlier variables need not be treated in this way. Then we must do:

assert (3<=sizeof(roots)/sizeof(value));   /* the assertion is optional, of course, but the point is that the size of the roots array must be large enough! */
roots[0]=a; roots[1]=b; roots[2]=c;
fr.next=roots+3;   /* where 3 is the number of roots we are preserving right now */
tinfo->fp= &fr;   /* push the new frame on the stack */
temp=g(tinfo,x,y);
a=roots[0]; b=roots[1]; c=roots[2];
tinfo->fp=fr.prev;  /* pop the frame from the stack */

The same struct stack_frame can be used for all the outgoing calls from this function.

We are developing some C macros to assist in producing this code; watch this space in the future for more information:

• BEGINFRAME allocates and initializes the frame at the beginning of the function
• LIVEPOINTERS1, LIVEPOINTERS2, etc. generate the pattern for saving variables, calling a function, and fetching variables back
• ENDFRAME provides matching close braces for BEGINFRAME.

Global variables (and fields of malloc/free data structures) that point into the Coq heap

Global variables or fields of malloc/free data structures that contain Coq heap pointers must also be registered with the garbage collector. There are two ways of doing this.

• The simplest method is: instead of assigning p.field = q; say instead certicoq_modify(tinfo,&p.field,q); where p.field is in the C program's global memory or malloc/free heap, q is a pointer into the Coq heap, and tinfo is the thread-info pointer. The disadvantage to this method is that p.field must never be deallocated, i.e., you can't call free(p). But when you're done with the pointer you can, and should, assign a null pointer into p, that is, certicoq_modify(tinfo,p,(value)1); so that the garbage collector can at least free up the data structure in the Coq heap that q pointed to.
• If you want to be able to free(p), then don't use certicoq_modify. Instead, you will add p to the stack of frames (described above), at the bottom of the stack, underneath all the frames that are used for C function local variables. This is demonstrated in the Certicoq Set Library. Since struct stack_frame is a singly linked list, that implementation wraps a doubly-linked list around the bottom portion of it (i.e., the global-variables portion) for convenience in deleting single items.

Allocating on the g.c. heap

C programs may allocate on the g.c. heap using glue-code functions for constructors of inductive data types whose names start with the word alloc, such as

value alloc_make_Coq_Init_Datatypes_nat_S(struct thread_info *, value);

which is the S constructor of the nat data type. Those functions never call the garbage collector, so a precondition for calling them is that there is enough space in the "nursery" of the heap. This can be tested as,

N+1 <= tinfo->limit-tinfo->alloc

where N is the arity of the constructor. For the S constructor, N=1.

If there are not enough words remaining, then one must call the collector before calling the alloc_make_... function. This is done by

/* save live pointers into stack-of-frames as shown above*/
tinfo->nalloc=(N+1);
garbage_collect(tinfo);
/* fetch live pointers from stack-of-frames as shown above*/

When the garbage collector returns, it's guaranteed that N+1 words will be available and this need not be retested.

If you are allocated several constructors in a row, of sizes A,B,C, you can call the collector just once to ensure that there will be space for all of them:

/* save live pointers into stack-of-frames as shown above*/
tinfo->nalloc=(A+1)+(B+1)+(C+1);
garbage_collect(tinfo);
/* fetch live pointers from stack-of-frames as shown above*/

and then you can call the various alloc_make_... functions without retesting tinfo->limit-tinfo->alloc.

In the current collector, if you set tinfo->nalloc to a value greater than 2^16 then it will complain and abort. We may remove this restriction in the future.