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, MSGID_RANDY autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,6405eefbf080daa6 X-Google-Attributes: gid103376,public From: Robert Dewar Subject: Re: Is an RTOS Required for Ada? Date: 1999/05/28 Message-ID: <7il48k$qkf$1@nnrp1.deja.com>#1/1 X-Deja-AN: 482960373 References: <373B2927.7B22F898@pop.safetran.com> <19990514155120.03860.00000396@ng-cr1.aol.com> <7hmc18$jr6$1@nnrp1.deja.com> <7i1b7p$3nb$1@nnrp1.deja.com> <7ifapi$lf1$1@nnrp1.deja.com> X-Http-Proxy: 1.0 x28.deja.com:80 (Squid/1.1.22) for client 205.232.38.14 Organization: Deja.com - Share what you know. Learn what you don't. X-Article-Creation-Date: Fri May 28 03:58:13 1999 GMT Newsgroups: comp.lang.ada X-Http-User-Agent: Mozilla/4.04 [en] (OS/2; I) Date: 1999-05-28T00:00:00+00:00 List-Id: In article , "George Romanski" wrote: > My personal view (there is majority, but no concensus on this > at present) is that inserted code which includes decisions > must be identified and verified, for level B. That seems a reasonable working approximation. Certainly GNAT does not begin to come close to this line (really it does not do much insertion in this sense at all, and certainly nothing that involves complex decisions, I agree with George that this would usually cross the line). But the line is still murky. After all, what if the decision was not generated by inserting code, but directly by the compiler's code generator. In this case there *is* no source code to identify in this case, but certainly you have to check all paths if your certification discipline involves this. A lot of directly generated code involves such decisions. As an example, consider: A,B,C : Integer; A := B / C; on the 8086. You cannot simply generate a DIV instruction since there is a bug which causes 16#8000# (largest negative number) / 1 to divide trap. So either this has to be fixed up in the divide trap handler, or you have to check this case specially, generating a decision point in the code. Second, especially in modern predicated architectures, conditional jumps tend to disappear anyway as a result of if conversions. Should there be a principle that every predicated instruction must be executed with and without the predicate being True. Sounds reasonable, but I don't know if testing standards have caught up with this. Third, there are lots of cases that involve no predication, and no explicit testing, but they do strange things to avoid jumps. For example, consider the following computation of MAX (EAX, EBX) on a 386: -- EAX < EBX EAX >= EBX CMP EAX. EBX -- CF = 1 CF = 0 SBB EDX, EDX -- all 1 bits all 0 bits MOV ECX, EDX NOT ECX -- all 0 bits all 1 bits AND EDX, EBX -- EBX 0 AND ECX, EAX -- 0 EAX OR EDX, ECX -- MAX (EAX, EBX) No predication, no jumps, but one would sure like to check this code in "both directions", yet this is not easy to codify either in terms of directly generated code or in terms of inlined inserted code. Note that a clever compiler might generate the above sequence from code that looked like: if A >= B then C := A; else C := B; end if; so a decision point in the source has disappeared in the generated code. Of course if the source code had written MAX, then we don't have an obvious decision point in the source, but depending on the machine we might see: 1. A single MAX instruction (Power) 2. The above hairy sequence (x86) 3. A converted if, using predication, with no jumps (Merced) 4. An explicit test and jumps (Sparc) So decision points in the source may not correspond to decision points in the object in any obvious way. I give this example just to remind us that, unlike the formalists view of precise mathematical verification, the real world of safety-critical verification is a more pragmatic one. The FAA rules (and other similar verification protocols) do not guarantee 100% correctness in a formal sense, but they have been found to be effective in practice, and we refine the practice based on experience as we go along. That there is not yet a consensus on some of these issues is not surprising, this is a very tricky area, and one in which common sense is not necesarily the best guide :-) Sent via Deja.com http://www.deja.com/ Share what you know. Learn what you don't.