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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!fx27.iad.POSTED!not-for-mail
From: Shark8 <OneWingedShark@gmail.com>
User-Agent: Mozilla/5.0 (Windows NT 6.1; Win64; x64;
 rv:30.0) Gecko/20100101 Thunderbird/30.0a1
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
 <NcaCv.85303$qR1.74779@fx02.iad> <HNidnc9nh6n76UTORVn_vwA@giganews.com>
In-Reply-To: <HNidnc9nh6n76UTORVn_vwA@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <DHeCv.125595$pu5.24045@fx27.iad>
X-Complaints-To: abuse@teranews.com
NNTP-Posting-Date: Wed, 30 Jul 2014 22:53:23 UTC
Organization: TeraNews.com
Date: Wed, 30 Jul 2014 16:53:21 -0600
X-Received-Bytes: 2060
X-Received-Body-CRC: 1321006822
Xref: news.eternal-september.org comp.lang.ada:21356
Date: 2014-07-30T16:53:21-06:00
List-Id: <comp.lang.ada>

On 30-Jul-14 16:40, Peter Chapin wrote:
> I'm not clear what they mean by "in-kernel hardware management" here.
> Are they talking about the hardware itself? If so, then SPARK would have
> to make that assumption as well. Similarly SPARK would have to assume
> any assembly language components are correct since they can't be
> analyzed. Of course one hopes the size of such components is minimal.

If it was the HW itself I wouldn't have thought they would add 
'management' -- therefore I think it must be concluded they are talking 
about things like properly using the cache or hw-paging.

> I'm going to guess the seL4 people regarded the boot loader as outside
> the scope of their project just as they might regard applications as
> outside their scope. Of course a verified boot loader would be great...
> but then so would be verified applications.

I'm the one who added 'loader' as the original text was "boot code is 
correct" -- I assume it means the loader and I could grant that should 
be out of the scope of an OS; /HOWEVER/, it could also be the code which 
starts/initializes the OS, in which case I would have to say it 
certainly falls into the the scope of verifying the OS "end-to-end".