In BitC, the type system is required to consistently preserve the
(im)mutability of every location across all aliases. However, I think
that there is a problem with this immutability guarantee due to the
interaction of unboxed composite types and by-ref aliasing.
If a location has type t, where t != (mutable t'), then we know that
the contents of l cannot change over the entire execution. All aliases
that refer to l also have type t.
In the case of unboxed structures, mutability can be specified
both on a per-field basis, as well as with respect to the entire
structure value.
For example, the following code declares an integer pair whose fist
field is declared mutable.
(defstruct iPair:val fst:(mutable int32) snd: int32)
Now, if p:iPair and q:(mutablle iPair),
(set! p.fst 25) ;; OK. fst is mutable
(set! p q) ;; WRONG, p is not mutable
(set! p.snd 25) ;; WRONG, snd field is not mutable.
(set! q p) ;; OK. q is mutable as a whole
(set! q.snd 25) ;; WRONG, snd field is not mutable.
The snd field cannot be set directly even though q can be mutated as a
whole. This is similar to const annotation of structure fields in C.
The point to note here is that contents of q.snd can change due to an
assignment through q, even though the field is not declared with a
mutable type. This is still consistent with the immutability per
location requirement that we have, since q.snd does not have independent
existence, but is dependent on the mutability of q.
In the programming language sense, q is what maps to a location
(possibly consisting of multiple cells for individual fields). As long
as we do not have unboxed aliases (ex: using the & operator), we must
always refer to the snd field of q through q (as q.snd) and the
mutability dependency is obvious to the compiler or other analysis
tools. However, by-ref breaks this since it permits unboxed aliasing.
For example, we can write:
(define qref:(ref (mutable iPair)) (dup (iPair 10 25)))
(define (f x:(byref int) y:(ref (mutable iPair)))
(== x 25) ;; suppose now true
(set! y^ (iPair -10 -25))
(== x 25) ;; not necessarily true !!!
)
(f qref^.snd qref)
The compiler cannot rely on the fact that x is a by-ref to an immutable
integer even though the type says so. This violates the immutability
guarantee of the type system.
The real issue here is that the mutability propagates inwards upto a
reference boundary. So, we need to interpret mutability in a pathwise
fashion, at least while creating aliases.
There are a couple of ways to fix this problem:
1) Handle it at by-ref: Declare that mutability propagates pathwise
while creating a by-ref. That is, the field qref^.snd can only be
passed as the actual parameter to a function that expects
(by-ref (mutable int32)). This will still forbid an assignment
like (set! qref^.snd 25).
2) Declare that mutability propagates pathwise: Same as (1) except that
assignment to qref^.snd is also permitted. Mutability propagates upto
the current level of unboxed-ness.
3) Declare that immutability propagates pathwise: The dual of (2) where
a field can be set (or passed as a (by-ref (mutable t)) parameter)
only if it is mutable as a whole as well as at the field
Given this, we can reconsider whether mutability must be specifiable at
the field level at all. First, mutability must be specifiable within
references. For example, in
(defstruct S1 a:(mutable int32) b:(ref (mutable int32)) c:int32)
the use of mutable annotation for a is contentious, but the mutable
annotation within a reference for b is necessary. The immutable int32
annotation for c may be useful if we want to ensure that we never set
the c field directly.
Second, even if we forbid unboxed mutability annotation of fields, a
similar effect can be achieved using parametrized structures:
(defstruct (S1 'a) a:'a b:(ref 'a))
(S1 (mutable int32))
So, I think it might be better to allow mutable annotations of fields
but change their interpretation?
Swaroop.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
