[bitc-dev] memory management primitives

[Eric Northup]

Sam Mason wrote:
> On Tue, Dec 05, 2006 at 04:30:10PM -0500, Swaroop Sridhar wrote:

[...]
> Would naming space banks preclude having an arbitrary number of them?
> My naive interpretation of naming suggests this, but I don't know what
> you're thinking about them.

On an OS rather than programming language granularity, the number of
Space Banks a KeyKOS/CapROS process had to chose from while processing a
message is typically either one (which the process had from the
beginning) or two (for a multi-client server process, one which to
server had from the beginning and another provided by the client being
served).  When more storage sources are available to chose from, it
becomes much harder to identify a single, correct party to charge for
an allocation.

That said, I see no reason why naming space banks would preclude having
an arbitrary number of them.  For example, represent space banks with an
opaque reference type (as they are in KeyKOS-derived designs) passed as
an extra argument to dup.

A more serious problem with to space bank analogy is that, in KeyKOS et
al, the party who provided a space bank is allowed to destroy the bank,
reclaiming all its storage.  Recovering from that event is a non-issue
if an entire process was allocated from the  destroyed bank, but
trickier in a multi-client server when a single client's bank
disappears.   I don't see how to model either case in a memory safe
language like BitC.

-Eric