From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,8a4455177648cb9e
X-Google-Attributes: gid103376,public
From: Peter Amey <pna@praxis-cs.co.uk>
Subject: Re: Idea: Array Boundary Checks on Write Access Only
Date: 1998/06/15
Message-ID: <35858FBC.4E5E@praxis-cs.co.uk>#1/1
X-Deja-AN: 362832169
Content-Transfer-Encoding: 7bit
References: <35851B64.5BF271C4@cl.cam.ac.uk>
Content-Type: text/plain; charset=us-ascii
Organization: Praxis Critical Systems
Mime-Version: 1.0
Newsgroups: comp.lang.ada
Date: 1998-06-15T00:00:00+00:00
List-Id: <comp.lang.ada>


Markus Kuhn wrote:
> 
> Here is a suggestion for Ada compiler developers:
> 
> Add a compiler configuration option that suppresses array index
> boundary checks only for *read* access to array elements.
> 
> Array boundary checks in Ada are a major advantage over C/C++
> and add a lot to the safety and debugability of the language.
> However the checks are also a significant performance loss
> unless they are deactivated. A useful compromise would be an
> option that causes the compiler to add boundary checks only
> when an array element is written, but not when it is read.
> Out-of-boundary array write accesses are dangerous because they can
> destroy other data structures and can cause failure inside completely
> unrelated objects. Therefore, in security critical applications,
> it is very desireable to deactivate for performance reasons
> only the checks for the less dangerous read accesses that if
> they go wrong should not cause malfunction within other objects.
> 
> Are there already Ada compilers around that do this?
> 
> Markus

Working in the safety-critical, real-time field I frequently encounter the 
tension between the need for checking and the desire for speed.  Another 
factor is the need to generate very high levels of object-code test coverage 
to satisfy some regulatory regimes; this is rather hard if the compiler has 
inserted run-time checks that in practice are unncessary and therefore 
cannot be externally stimulated.  In this environement I am not very happy 
with the idea that reading out of bounds is any less unsatisfactory than 
writing: both show that the code is broken and may misbehave.  

It was to square this particular circle that we invested so much effort in 
the proof of absence of run-time errors facility in SPARK (Markus, I know 
you are familiar with this...).   Having conducted a proof that code is 
exception free it is possible to turn compiler-generated checks off with a 
clear conscience and get the benefit of smaller, faster code as a bonus.

Peter

-- 
--------------------------------------------------------------------------- 
  
      __         Peter Amey, Product Manager
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/
 --------------------------------------------------------------------------