Re: [Chicken-hackers] [PATCH 4/6] * scrutinizer.scm: Infer more exact types after set!

[megane]

Peter Bex <address@hidden> writes:

> On Thu, Aug 22, 2019 at 02:51:26PM +0300, megane wrote:
>> Hi,
>>
>> I'm working on some inference improvements and I noticed the blist keeps
>> accumulating some bogus entries. Commit 0003 removes some of those.
>
> Hi Megane,
>
> I've pushed your cleanups because I believe they make the code and
> scrutinizer output much more readable.
>
>> There's also a small improvement (0004).
>
> This one I did not apply.  I'm not 100% sure this is safe to apply and
> Felix mentioned being a bit worried about the correctness of this change.
>
> I believe it has to do with continuations or perhaps different threads
> mutating the variable.  Since I don't know enough about the consequences,
> I'll leave this to Felix or Evan.

Thanks Peter!

Yeah, let's put this 0004 on hold.

I'm working on some refactorings on the scrutinizer that might help to
see the effects of this change more clearly.

That being said, I'd like to learn more about the unsafeness of this
change. How is this more unsafe compared to what the scrutinizer is
doing currently?

I consider continuations, threads and garbage collection (finalizers in
particular) all to be the same issue from the type safety perspective.
Finalizers being the most general of those. Finalizers may run at "any
time", and they can mutate things arbitrarily.

Here's two examples I think are equally safe things the scrutinizer
currently does:

   (lambda (x)
     (if (list? x)
         (begin                                 ; x : list
           (gc #t)                               ; <- x may be mutated here
           (compiler-typecase x ((not *) 1))))) ; x : list still

   (lambda (x)
     (length x)                         ; enforces x : list
     (gc #t)                             ; <- x may be mutated here
     (compiler-typecase x ((not *) 1))) ; x : list

If you replace the compiler-typecase with (length x), then that call
would get specialized. That is clearly theoretically not safe.

You could replace the (gc #t) with a call to any non-trivial #:pure or
#:clean function and the situation would still be the same. Those may
cause finalizers to run, which can mutate x.

Maybe there should be a flag or declaration that tells the scrutinizer
to assume there are no non-local mutation of local variables.

Also, please tell if this is not the issue you (anyone) had in mind.
Examples are helpful.