Type theory for memory safe data structures

Question

Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed.

I have heard of ideas based around linear typing for guaranteeing memory safety in the case of a single pointer to the memory. I believe the Rust language is based around this.

But suppose, for example, I wanted a memory safe implementation of a B+ tree in a systems language that has no garbage collection or reference counting. What exists in type theory that could be used to guarantee that the B+ tree implementation is memory safe?

Answer 1

There has been a lot of work around the idea of statically checking the memory safety properties of programs.

Francois Pottier give an excellent overview of various approaches in this presentation. The main technique you probably would be interested in is region typing.

The Wikipedia article is quite complete, but the basic idea is to keep explicit regions which references are required to explicitly be assigned to a given region, which can be managed by the programmer or left to be inferred by the compiler. This is somewhat reminiscent of the RAII approach to memory management used mainly in C++ (the wiki article is terrible however).

In practice, region inference hasn't gained widespread use in compilers, mainly because of the complexity of the analyses involved.

Again related, there has been a flurry in work on separation logic over the last decade, which is an extension of Hoare Logic which allows reasoning over separate regions of the heap, in order to analyze whether objects can share memory locations or not. This method of reasoning is quite difficult to apply to a language like C with "real" pointers, because of the possibility of pointer aliasing.