Re: Efficient Sequential Access to Arrays

[Keean Schupke <keean.schupke@googlemail.com>]

On Thursday, 26 July 2012 01:15:25 UTC+1, Randy Brukardt  wrote:
> "Keean Schupke" wrote in message 
> > On Wednesday, 25 July 2012 08:09:09 UTC+1, Niklas Holsti  wrote:
> ...
> >> Sure, in general. But here the OP (Keean) is trying to beat the
> >> performance of C++ that uses pointers without index checks. Enabling
> >> index checks in the Ada code would probably (in this case, where the
> >> algorithm has scatterered indexing of the array) slow it by an amount
> >> that swamps the effect of the multiplication optimization.
> >
> > On the specific point of array index checking, if you can statically prove 
> > the algorithm
> > using the array will never use an out of range index, there is no need to 
> > run-time index check.
> >
> > If we generate a random number between one and N, and then lookup the Nth 
> > element, we do not
> > need to range check as the number is by definition in range. If the type 
> > system can carry such proofs
> > (for example using range types in Ada) so you have:
> >
> > subtype Idx is Integer range 1 .. 10;
> > type Arr is array (Idx) of Integer;
> > function Random returns Idx;
> > A : Arr;
> > A(Random); -- as the random number is already in the range there needs to 
> > be no
> >                         range checks on the array lookup.
> 
> This isn't necessarily true. The following is *very* Ada language-lawyer, so 
> skip if you don't want to know the details. (BTW, this is all Ada 95 
> thinking, refined somewhat since.)
> 
> Ada scalar objects can be in a state known as "invalid" (see 13.9.1 in your 
> Ada Reference Manual). For integer types, this corresponds to a value out of 
> range. Ada compilers are always allowed to return invalid results from 
> scalar operations, with a few exceptions. So in general, an Ada compiler 
> does not actually need to make range checks on scalar objects. The only time 
> that a check on a scalar object *has* to be performed is when using the 
> value could lead to erroneous execution (such as in indexing out of range).

This is an equivalent concept to nullable, so two questions:

What is the literal for 'invalid', IE:

X : Index := #INVALID -- we should be able to initialise to invalid.

if X = #INVALID -- I want to be able to test for invalid.


> 
> So, formally, writing a scalar subtype does not ensure that a compiler can 
> eliminate checks. Indeed, it doesn't necessarily mean anything at all, as 
> scalar objects can be uninitialized and the compiler has to assume that they 
> could be out of range unless it can prove that they are initialized on all 
> paths.

Like not null we therefore need:

type X_Type is new Integer not invalid range 0 .. 10;
X : X_Type; -- error
X : X_Type := 0; -- OK

> 
> Of course, us compiler implementers *want* to eliminate checks based in 
> subtypes. There are various strategies for doing so. The "usual" one is that 
> the compiler defines some subtest of scalar objects as "known to be valid". 
> Those are objects that the compiler can easily prove are initialized. (For 
> Janus/Ada, we use a fairly conservative definition: stand-alone objects that 
> are explicitly initialized, literals, loop parameters, and subprogram 
> parameters. I don't remember if function results are included or not.). 
> Checks have to be performed on assignments and other operations on "known to 
> be valid" objects (array indexing is also treated this way) unless subtypes 
> are the same or statically compatible AND all constituents of the source 
> expression are "known to be valid".

The above helps the compiler eliminate range checks, the other is type promotion: for example:

X : not invalid Integer := 99;
Y : array (10 .. 1000) of Integer;

if X <= 1000 then
   -- type of X is now : not invalid Integer range Integer'First .. 1000;
   if X >= 10 then
       -- type of X is now : not invalid Integer range 10 .. 1000;
       Y(X) -- No need for any range checks.
   end if;
end if;

> 
> Our optimizer can remove a few checks that have been generated because of 
> later flow analysis and the like, but what can be done then is quite 
> limited. Generally, the compiler has to not generate the checks in the first 
> place.

See above for language changes to facilitate better range check removal.

> 
> I&#39;m not sure precisely how GNAT handles this, but elimination of checks is 
> *much* harder than it appears on the surface, mainly because Ada allows 
> uninitialized objects (and still expects uses of them to be detected).

This is something I have looked at in a couple of different contexts, and using dependent types (a simple example of which is above) there are known techniques for removing all implicit range checks. Personally I dont like implicit stuff, so for me personally I would like the compiler to never insert implicit checks but instead issue a compile error if it ever had to insert an implicit range check. As above you may have to insert explicit range checks to satisfy the compiler, or you may used an unchecked conversion to tell the compiler, trust me, i know what I am doing and I have verified the code will not generate out of bounds values due to unit testing and formal verification methods.

> 
> &gt; I don&#39;t know how good the compiler is at doing this?
> 
> If the implementation model is &quot;wrong&quot;, it might not do it at all.
> 
> &gt; There are times when the programmer can guarantee that the output of a 
> &gt; function will be
> &gt; within range due to extensive unit testing and validation.
> 
> But that doesn&#39;t guarantee that the compiler can remove the checks.

The compiler should remove the range checks if the programmer is telling it that the value is definitely within range. With a 'not invalid' type modifier, this can be done with some kind of unchecked conversion.

> 
> &gt; I wonder, is there a way to get the compiler (GNAT) to issue a warning 
> &gt; when it has to insert a range check?
> 
> Can&#39;t say if there is a GNAT option, but it seems like a good idea. I added 
> such an &quot;information&quot; (it&#39;s not a warning in the sense that normally it 
> doesn&#39;t need to be corrected) to the (lengthy) to-do list for Janus/Ada.
> 
>                                         Randy.

Cheers,
Keean.