Safe Manual Memory Management

[DavePearce]

Currently Whiley has a somewhat unclear story about memory management. Specifically, how Whiley can be used without a garbage collector. There are essentially several pieces currently in play:

• (Value Types). You can, in fact, get along quite nicely without using references at all. Value types will be collected without garbage collection using (for example) reference counting or other mechanisms. Reference counting is a complete solution here, because value types cannot have cycles.
• (Lifetimes). Reference lifetimes provide a means for safe deallocation of memory allocated on the heap. In particular, when a lifetime goes out of scope, its corresponding memory can be safely deallocated.

At this stage, I propose to remove reference lifetimes for Whiley as I no longer believe they are necessary for a 1.0 release. However, in the future, they may well make a come back as, in general, they are a nice solution.

With the removal of reference lifetimes, we need an alternative approach to enable safe memory deallocation. The plan is to employ safe manual memory deallocation. This works by placing the burden of ensuring safety onto the verifier. Specifically, we pair the new expression for allocating memory with e.g. delete statement for deallocating it. The verifier is then responsible for ensuring that the reference passed to delete was unique.

[DavePearce]

There are some interesting questions surrounding safe memory deallocation:

• Runtime Checking. Is there any way to enable runtime checking of memory deallocation. For example, using reference counting or similar. Note that not all checked properties are runtime checked. For example, index-out-of-bounds checks might be omitted for deployment, etc.
• Destructors. An interesting question is whether deallocating an object can or should deallocate others it refers to. An alternative approach would be to employ destructors.
• Balloons. Another interesting question is how to deallocate cycles or balloons (i.e. where every node has one incoming reference from another in the cycle and, in addition, one has another incoming stack reference). If delete p requires |>p<| == 1 then balloons cannot be deallocated. However, it is still be safe to deallocate the balloon if the reference was externally unique. For example, if we require only that after the deallocation |>p<| == 0 (which is in fact what we actually care about).