Prohibiting double frees

[Evan Shaw]

Hi,

The project page says Deca provides:

"A strong region-and-effect system that prohibits unsafe escaping pointers and double-free errors"

I have a basic understanding of region and effects systems, but don't understand how they can prevent double frees.

I imagine that the free function would have the effect of invalidating the pointer passed into it, preventing future uses of that pointer. But what about aliases? And what about a function like this:

function maybeFree<a>(object: @a, b: Boolean): Unit {
    if b then free(object)
}

What effect does this function have? Its effect is entirely dependent on the value of b. Am I thinking about this the wrong way?

- Evan

[Eli Gottlieb]

That function's statically-computed effect will be: !+(),-(!destroy('a)), where 'a is the region variable describing the region of the obj pointer.

So Deca statically guarantees you can't use that region after calling maybeFree.  The possible error here is that you might get a free/destroy effect computed statically without actually freeing the memory -- a memory leak that leaves your checked accesses safe, same as garbage collection could provide.

[Evan Shaw]

Alright, so it sounds like the answer is basically "don't write a
function like that". :) Harsh, but maybe the prevented errors outweigh
potential use cases.

And what about aliasing? Here's some obviously bad code to help
illustrate my question:

function aliasAndFree<a>(object: @a): Unit {
global1 = global2
global2 = object
free(object)
}

Here "global1" and "global2" are global pointers. Clearly object's
region can't be used after this function runs, but is the global
region also considered free? Are both global1 and global2 unusable
after this function runs?

And how does this system hold up in the face of concurrency, where a
thread can potentially free a shared region?

- Evan

[Eli Gottlieb]

The second assignment will be illegal.  Global2 won't be polymorphic in its region, it will only be able to take pointers from regions equal to or contained in the region where it was defined.