[r6rs-discuss] [Formal] eliminate library export immutability loophole

From: Abdulaziz Ghuloum <aghuloum>
Date: Mon Mar 12 19:03:05 2007

On Mar 12, 2007, at 6:05 PM, AndrevanTonder wrote:

> On Sun, 11 Mar 2007, R. Kent Dybvig wrote:
>
>> Okay, here's one example:
>>
>> (library (L1)
>> (export y get-y set-y!)
>> (import (r6rs))
>> (define x (call/cc (lambda (k) (list 0 k values))))
>> (define y (car x))
>> (define z ((caddr x)))
>> (define get-y (lambda () y))
>> (define set-y!
>> (lambda (v)
>> (call/cc (lambda (k) ((cadr x) (list v (cadr x) k)))))))
>
> I think there is an error. Here is a working version:
>
> (library (L1)
> (export y get-y set-y!)
> (import (r6rs))
> (define x (call/cc (lambda (k) (list 0 k values))))
> (define y (car x))
> (define z ((caddr x) #f)) ; modified line
> (define get-y (lambda () y))
> (define set-y!
> (lambda (v)
> (call/cc (lambda (k) ((cadr x) (list v (cadr x) k)))))))
>
>> By my reading of the current library description, the program:
>>
>> (import (r6rs) (L1))
>> (write (list y (get-y))) (newline)
>> (set-y! 3)
>> (write (list y (get-y))) (newline)
>>
>> prints
>>
>> (0 0)
>> (0 3)
>
> I get the following, which I think is also consistent with the
> current specification:
>
> (0 0)
> (3 3)
>
> This happens if exported variables are translated to shared r5rs
> toplevel globals, which is a possible implementation of the shared
> semantics.

I guess it depends on how you read the following (quoted from 6.1 of
R5.92RS):

   The variable-definition right-hand-side expressions are evaluated
from left
   to right, as if in an implicit letrec*, and the body expressions
are also
   evaluated from left to right after the variable-definition right-
hand-side
   expressions. A fresh location is created for each exported
variable and
   initialized to the value of its local counterpart. The effect of
returning
   twice to the continuation of the last body expression is unspecified.

The paragraph does not specify when the fresh locations for the
exported variables
are initialized. If every exported location is assigned immediately
after its
local counterpart is defined, then the values stored in both
locations will be
consistent (even when returning twice). This is also true if your
implementation
strategy is to skip local definitions altogether and just use one
global location
for each library definition.

If you read the above paragraph as saying that all variable's global
locations are
initialized together, in one go, after all the local variables are
defined, then
you'll get into the inconsistent state and invalid assignment to an
immutable
binding that Kent described.

Aziz,,,
Received on Mon Mar 12 2007 - 19:02:24 UTC