[bitc-dev] {,de}allocation

[Mark S. Miller]

Jonathan S. Shapiro wrote:
> The "free" keyword is reserved, but allowing it to be invoked without
> discharge creates safety issues. Having said that, I should admit a
> sleazy hidden fact: the prover will need DEFAXIOM to allow programmers
> to introduce facts that cannot be proved. In particular, DEFAXIOM is
> needed to describe the behavior of assembly support routines. So free
> can be used badly if desired.

Could the use of unsafe-free be controlled, in much the way that BitC 
currently controls the ability to introduce mutable static state? If not, then 
a malicious library writer can use unsafe-free to violate memory safety.


> Haskell, so far as I know, does not have free.

AFAIK too, that's correct. But Haskell does have a primitive, unsafePerformIO, 
that allows code to violate declared constraints on side effects. AFAIK, in 
Haskell currently, the ability to use unsafePerformIO to escape this checking 
in uncontrolled. Were someone to do an Emily-like[1] taming of Haskell, to 
derive a corresponding object-capability language, I would advocate that they 
make the ability to unsafePerformIO into a controllable permission that is 
denied by default. For BitC, could unsafe-free (or perhaps even DEFAXIOM) be 
similarly controlled?

Any module that has permission to unsafe-free is a central point of failure 
for that process as a whole, since the correct function of everything else in 
that process relies on that module to use unsafe-free safely.

[1] http://www.hpl.hp.com/techreports/2006/HPL-2006-116.html

-- 
Text by me above is hereby placed in the public domain

     Cheers,
     --MarkM