[bitc-dev] Capture problem with by-ref

[David-Sarah Hopwood]

Jonathan S. Shapiro wrote:
> On Wed, 2008-03-12 at 18:03 +0000, Sam Mason wrote:
>> OK, I didn't realise it was doing this.  It'll be fun/awkward writing
>> code that doesn't do any heapification then :) 
> 
> We have in mind to build an audit tool for this, so that code can be
> annotated as "should not allocate" and a checker can test this.
> 
>> I've also just thought of
>> another issue with mutable by-refs, I think it's going to make auditing
>> harder?  Take the following function:
>>
>>   (defun (f x : (mutable int32))
>>     (g x)
>>     x)
> 
> Yes, there is definitely an auditing issue here. That is a real concern,
> and an important one.
> 
> So let's look at that, and look at the alternatives.
> 
> First, note that the issue only arises for (by-ref (mutable T)). If the
> reference type is immutable, no audit issue arises.
> 
> The problem with *removing* BY-REF is that we have many cases in
> practice where we have some very large structure and we need to
> initialize or update some part of it. For example, in the Coyotos kernel
> we have lots of structures that contain capabilities, and we "prepare"
> these frequently. Our options are:
> 
>    capSlot := prepare(capSlot)	; pass by copy
> or
>    prepare(capSlot);  pass by mutable reference
> 
> Unfortunately, the performance advantages of the second are quite
> overwhelming. This seems to be a case where there is an unavoidable
> tradeoff between performance and audit, and in this case I think the
> argument in favor of performance is quite strong.

A linear type system is potentially capable of ensuring that a mutable
reference can be passed into prepare(...), but that no aliases derived
from that reference remain after prepare has returned.

Of course this could be considered a rather complicated sledgehammer,
but I'm trying to get a handle on precisely which problem(s) you are
concerned about with respect to auditability -- is it the potential
for aliasing of a reference after the procedure to which it was passed
has returned?

-- 
David-Sarah Hopwood