[bitc-dev] {,de}allocation

[Jonathan S. Shapiro]

On Sun, 2007-01-28 at 13:17 +0100, Pierre THIERRY wrote:
> Scribit Jonathan S. Shapiro dies 27/01/2007 hora 11:13:
> > As things have progressed, I am coming increasingly to believe that
> > the second model will never be used. In Coyotos, we appear to have
> > three cases:
> > 
> >   1. Critical processes. These must operate in bounded resource
> >   anyway.  These processes have the property that they allocate but
> >   never free.
> > 
> >   2. Event-loop processes: these processes have a natural point where
> >   GC can be done efficiently (the top of the event loop), and when it
> >   is done at that point the result is probably more efficient than
> >   free.
> > 
> >   3. General processes. These were unlikely to be able to accomplish
> >   the proof discharge in any case, and we always assumed GC for these.
> 
> What about providing the free primitive anyway? As you say, BitC won't
> have dependencies on Coyotos, and the free primitive could prove useful
> somewhere else. And it could prove useful in Coyotos, after all.
> 
> Do you know if other system-level implementations in functional
> languages also went without primitives like alloc and free? (like the
> House project in Haskell)

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.

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

None of these languages have anything like malloc -- all allocations are
typed.

> > > I'm also wondering how a process like the network stack described in
> > > "Network Subsystems Reloaded" would be written: it should at least
> > > be able to specify where to allocate space for objects according to
> > > the client they will be used for.
> > This is outside the scope of the language definition.
> 
> Is it? I'd tend to think that it is impossible (or hard or inefficient)
> with BitC as it is currently specified. But I didn't dig that issue
> much.

The issue is a matter of language runtime design. Those applications
require multiple heaps and explicitly reified heap backing store. We
haven't tried to deal with that. It isn't hard to get it right
pragmatically, but understanding it formally is very challenging.
-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100