Issue: ADJUST-ARRAY-NOT-ADJUSTABLE (Version 6)

[Guy Steele <gls@Think.COM>]

It is important at this stage to have specific code examples to look at,
and I am glad that Jonl has provided one.  Unfortunately, it does not
appear to back his claim.  (This is not to say that there cannot be some
other piece of code to back his claim, and I hope that he will produce
another example.)

   Date: Tue, 28 Feb 89 02:36:21 PST
   From: Jon L White <jonl@lucid.com>
   ...
   Here's a synopsis of the damage that can occur unless some such
   clarification is made.  Consider the following function:

	(defun fast-aref (x i)
	  (declare (optimize (safety 0) (speed 3)))
	  (check-type x (simple-array t 1))
	  (setf (aref (the (simple-array t 1) x) i)	;open-compiled
		:encountered)
	  t)

	(defparameter foo (make-array 5 :adjustable t))

   What happens when FOO is passed to FAST-AREF?

Let's look at this closely.  Consider two implementations (A) and (B).  In
(A) ["Symbolics"] an array may be both adjustable and simple; that is,
simpleness might depend on fill-pointerness and displacedness but is
independent of adjustability.  In (B) ["stock hardware"] an array can never
be both adjustable and simple.

 For each implementation I will consider compile-time actions and then
run-time actions.  Assume that both compilers open-code SETF, and for
simplicity assume that displacedness or fill-pointerness does not affect
the open-coding.

(1) The compiler for implementation (A), knowing that simple arrays may
nevertheless be adjustable, will generate code that handles arrays
regardless of adjustability.

The CHECK-TYPE form will determine that the array is simple, and execution
will continue.  Because the array is in fact simple, the declaration in the
THE form is correct.  The SETF will be executed.

(2)  The compiler for implementation (B) is justified in generating open code
for the SETF that does not handle adjustable arrays, because the array has
been declared via THE to be simple, and the compiler knows that in
implementation (B) simple arrays are not adjustable.  Moreover, the
compiler is justified in producing such code even at high safety, because
non-simple arrays will not get past the CHECK-TYPE form.

The CHECK-TYPE form will determine that the array is not simple, and an
error will be signalled.


Now, the two implementations behave differently on the example, and that is
a cause for concern.

Let us now examine the two behaviors described above under two different
interpretations of "simple-array" type specifiers.  One is the strict
interpretation that adjustable arrays may never be simple.  The other is
the more liberal interpretation that I proposed: namely that for
declaration "simple-array" means that you *tried* to make it simple (by
specifying :adjustable nil) or that you have checked that it is simple; and
for discrimination an adjustable array is considered non-simple only if the
implementation in fact relies on that distinction.

Before I proceed further I must reaffirm an important principle on which I
judge correctness and conformance.

	It is *not* required that two implementations have the same behavior
	when executing an erroneous program.

This has two consequences:

(i) It is permitted for an implementation to extend the language by defining
within that implementation a meaning for particular kinds of erroneous code.

(ii) A programmer may not rely on a valid implementation to identify every
error in a program.  In other words, successful execution of a program in
one implementation is not a guarantee that the program is free of errors,
and is not a guarantee that the program will execute successfully in
another implementation.  The only guarantee of equivalent execution in two
implmentations is that the program in fact be free of errors.

This principle is relevant to evaluating Jonl's claim:

   ... if the language permits SIMPLE-ARRAY to mean one thing in one
   implementation, and another thing in another implementation (under a
   false sense of permitting optional efficiency), then this little example
   will "break" in one implementation but will "work" in the other --
   in short, the type SIMPLE-ARRAY will not be portable.  

because his argument about nonportability is not sound unless the program
in question is correct (and I have seen this argument advanced in previous
discussions in cases where the example under discussion was not correct).

Therefore we must establish that the program is correct before comparing
the implementations.  (In preparing this analysis I considered a variant of
the given example in which the CHECK-TYPE form was omitted, and concluded
that this program was erroneous under either interpretation.)


I argue that the program is correct under both interpretations.  The
presence of the CHECK-TYPE form is crucial to correctness, for it is
guaranteed to filter out non-simple arrays before the AREF is encountered.
(From the point of view of code generation, it is guaranteed to filter out
arrays that the open code for SETF cannot handle.)

Under the strict interpretation implementation (A) is incorrect by
definition.  Under the liberal interpretation implementation (A) is
correct, and accomplishes a useful purpose.

Let us therefore examine the question of which interpretation is to
be preferred.

(a) The strict interpretation would seem to adhere more closely to the
definition of simple arrays given in CLtL, p. 28, and some weight must be
given to adhering to CLtL.  However, there is arguably some ambiguity in
the wording, as it refers to an array that "is not to be adjusted"; perhaps
adjustable arrays fall into this category if the program in fact never
makes any attempt to adjust them.

(b) A program might attempt to use adjustability as an explicit
information conduit, rather than simply as advice to the implementation
on speedy array implementations:

	(defun hairy-print (a)
	  (let ((*print-pretty* (typep a 'simple-array)))
	    (print wazoo)))

	(hairy-print (make-array 3 :adjustable nil))

In implementation (A) this would not have the (bizarrely) intended effect.


I conclude that the strict interpretation may be preferred, but not for the
reasons Jonl has advanced!  The liberal interpretation does *not* prevent
compilers for stock hardware from producing good code, and therefore the
code example does not support his claim to the contrary.

Moreover, an argument that code might behave differently in two
implementations and therefore impede debugging is rather a red herring,
because (I claim) such differing behaviors occur only when the program is
erroneous (in which case implementations are permitted to differ) or when
the program is using adjustability as an information conduit for reasons
unrelated to getting good array performance.

We may wish to regard the latter point as justification for preferring the
strict interpretation anyway, because implementations are required to
faithfully execute *all* correct programs, not just sensible ones.
Whichever interpretation is agreed upon, let it be for good and careful
reasons.  I don't believe that the arguments advanced so far based on a
desire for good open code on stock hardware have yet provided a clear
criterion for preferring one interpretation over the other.

--Guy