[cap-talk] Claim: correct generic wrapping is not possible in principle

[Jonathan S. Shapiro]

On Mon, 2007-01-01 at 08:18 -0800, David Wagner wrote:
> Thanks for your comments on embedded systems.  They're helpful.
> Let me follow up on one point, for my own understanding:
> 
> David Hopwood writes:
> >As it happens, the embedded system I'm working on at the moment (a printer)
> >uses linked structures within a statically allocated array.
> 
> How does it help to allocate those structures from a statically allocated
> array, instead of from the heap?  Isn't that statically allocated array
> just a heap in disguise, making your code just malloc() in disguise?

Not quite. First, it is a heap of pre-bounded size. Second, as you
pointed out, it can be indexed with cursors (indices) or pointers of
dependent type, which makes aliasing issues clearer in both human and
automated verification terms. Finally, it induces a change of mindset in
the programmer.

The last one is probably the most important one from a practical point
of view: knowing that the heap size is fixed promotes a more judicious
view of object allocation.

> Why would the resource exhaustion issues be significantly different for
> linked structures within a statically allocated array (which sounds
> to me like an open-coded malloc()), as compared to any other kind of
> dynamic allocation (e.g., an explicit call to malloc())?

Two reasons -- perhaps David will have others:

  1. You are forced, mentally, to accountability.
  2. You have non-interacting purpose-specific heaps. Allocations in one
     cannot exhaust storage in another.

> I'm sure you can specialize the behavior of your dynamic allocator for
> this particular use, since you know it will only be used in this one way,
> but it's still a dynamic allocator, so you still need to prove that
> no dynamic allocation attempt will ever exceed the amount of storage
> available in that statically allocated array.  I don't see why proving
> that no memory allocation attempt will ever fail is any easier to do
> when the program calls Hopwood_malloc() to allocate out of a statically
> allocated array, than it would be if you called malloc() for that one
> purpose.

>From a verification perspective, it isn't intrinsically easier, but the
change in programmer behavior leads to programs that are easier to
analyze in either model.


shap
-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100