From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 23116 invoked by alias); 2 Mar 2008 16:08:18 -0000 Received: (qmail 23098 invoked by uid 22791); 2 Mar 2008 16:08:17 -0000 X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.31) with ESMTP; Sun, 02 Mar 2008 16:07:58 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 9602B2A9EC2; Sun, 2 Mar 2008 11:07:56 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id euxOzWQV8hKy; Sun, 2 Mar 2008 11:07:56 -0500 (EST) Received: from [127.0.0.1] (nile.gnat.com [205.232.38.5]) by rock.gnat.com (Postfix) with ESMTP id E73FE2A9EC1; Sun, 2 Mar 2008 11:07:55 -0500 (EST) Message-ID: <47CAD0CC.1010002@adacore.com> Date: Sun, 02 Mar 2008 16:08:00 -0000 From: Robert Dewar User-Agent: Thunderbird 2.0.0.12 (Windows/20080213) MIME-Version: 1.0 To: "Frank Ch. Eigler" CC: Mark Mitchell , "Joseph S. Myers" , Richard Kenner , gcc-patches@gcc.gnu.org, gcc@gcc.gnu.org, rguenther@suse.de Subject: Re: [PATCH][4.3] Deprecate -ftrapv References: <10803011408.AA02772@vlsi1.ultra.nyu.edu> <47CA750E.9080409@codesourcery.com> <47CABA01.3090700@adacore.com> <20080302150959.GF29013@redhat.com> <47CAC5BE.7030904@adacore.com> <20080302154432.GH29013@redhat.com> In-Reply-To: <20080302154432.GH29013@redhat.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org X-SW-Source: 2008-03/txt/msg00099.txt.bz2 Frank Ch. Eigler wrote: > Hi - > > On Sun, Mar 02, 2008 at 10:20:30AM -0500, Robert Dewar wrote: >> [...] >>> (Off topic, but I'd expect that avionics software is engineered with >>> enough layers of protection, including catching traps, so that a >>> -ftrapv hit would not cause a deep impact.) >> As I say, it is more usual in avionics software to rely on proving >> or demonstrating during the certification process that the code >> is correct. [... and exception trapping is sometimes disabled on >> deployed code ...] > > Wow. This gives one the impression of eschewing of defense in depth, > but I suppose the overall record (positive and negative) speaks for > itself. That's right, defense in depth is a concept that comes from dealing with code that you assume might fail. Safety-critical avionics code is code that you assume will never fail. There has been at least one incident of a software bug in certified code, but it is very rare, and the record is impressive (no life has been lost because of a software bug in the history of commercial aviation). And that's using an informal standard (DO-178B) and we think we can do much better than this (e.g. in the MILS contexts, where higher EAL levels require formal verification techniques to be used, DO-178B has no such requirement). > If you're saying that security-related software written by people > working in DO-178B workflows tends to be as well cared-for as > saftery-related software, OK. But most security-related software we > normal folks use is not written by such people / processes. Right, and security-related (a nice term, which distinguishes itself from security-critical) software can certainly benefit from defense in depth. Even formally proved security-critical software can benefit, because corrupting code or data by physical intrusion may still be limited in effect because of such defenses > > >> [...] Again, the issue is whether such things are for finding bugs >> during development, or defending against bugs that make it through >> the entire development process. > > Those decisions may be made by separate people or even organizations. > An OS distributor can decide to use different compiler flags than the > code author - whether that be for extra trustworthiness, speed, > portability, compatibility. Ideally, protective measures should be > usable for either subject. Yes indeed ... > > >> Even in the Ada world, it is normal to turn off exceptions in >> safety-critical code for the final delivered software that runs on >> planes. > > (Drifting farther off topic onto my personal curiosity: are exception > handling paths just not considered powerful & robust enough to design > in and rely on? Do these machines have e.g. watchdog timers? Run -O2 > vs. -O0 code?) Usually you avoid -O2 in these contexts, too hard to establish the required source-to-object traceability. We most typially use -O1 with a couple of optimizations suppressed (e.g. if-conversion). It is not that exception handling paths are not powerful or robust. It is that a) they should not be needed if the code is correct b) they create a testing hazard, you can't have untested code in an SC system, so you have to test the exception case, which is tricky if in fact it is not possible for the exception to occur. So you have to prove in any casea that the exception can't occur to justify not testing it, and if you can convince the certification authorities that testing is not required, you have convinced them that the exception cannot happen, so why leave in the code. There are those who prefer to leave checks on in safety-critical delivered code, the argument rages strongly on both sides :-)