[bitc-dev] Rationale for unboxed mutability in BitC?

[David Hopwood]

Sam Mason wrote:
> On Fri, Sep 15, 2006 at 03:38:19PM +0100, David Hopwood wrote:
> 
>>Or is there some other argument for unboxed mutability in the
>>semantics that I'm missing?
> 
> I see two main arguments leading to it:
> 
>  1. If BitC is going to be used in the kernel then you need to be able to
>     make guarantees about how things are organised in memory (i.e. the
>     page tables in an Intel processor need to structured correctly).

I agree that this is necessary *for some types* -- but only a very small
minority of types. It would be quite sufficient to require those types to
be annotated to say that the correctness of the program depends on their
having a standard representation.

This would have the following effects:

 - it would act as useful documentation of which types correspond to hardware
   or ABI abstractions (so that binary compatibility should be considered
   before changing them),

 - the semantics would impose whatever restrictions (e.g. on polymorphism)
   are necessary for those types to make a standard representation
   straightforward to implement,

 - conversely, non-annotated types would have no such restrictions, and no
   direct constraints on how they may be represented. I believe this would
   result in a better language expressiveness/complexity trade-off, require
   less type system invention, and permit more optimizations.

Note that C essentially does the same thing, but less portably. Standard
C89/99 does not guarantee anything about representations [*], so operating
systems written in C typically depend heavily on a particular C implementation
or small set of implementations (e.g. Linux on gcc), often using #pragmas for
certain types to select representation options, such as use of padding.


[*] except that the representation of a value is accessible and copyable
    as an array of 'unsigned char' -- but this is not very helpful on its
    own, and has some counterproductive consequences.

>     Making these guarantees when you have an unpredictable (to anyone
>     except the author of the optimiser) middle man is difficult.

What I was proposing would only depend on one specific optimization: ref cells
in specifically marked structure and array types must be inlined. Overall, the
constraints on optimization of BitC would be reduced.

Note that requiring certain optimizations is not without precedent in language
design; tail call optimization in Scheme is an obvious, and I think quite
successful, example.

>  2. Fancy optimisers make for lots of non-trivial code and lots code
>     means even more proof (which is going to be difficult enough even
>     for a small compiler).

The optimization I'm talking about is not particularly fancy. AFAICS, it
doesn't complicate the language implementation much more than supporting
unboxed mutables directly. Treating ref cell inlining as a required
optimization keeps the *specification* simpler than it would be for a
language with direct support for unboxed mutables, which is likely to have
at least as great an effect on the difficulty of verification as the
implementation complexity.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>