[coyotos-dev] Couple of potential-someday-user questions

[Jonathan S. Shapiro]

On Thu, 2005-01-27 at 21:05 -0500, lists at notatla.org.uk wrote:
> From: "Jonathan S. Shapiro" <shap at eros-os.org>
> 
> > I think it's a third phase. Phase one is to have a language and some
> > reason to believe that building a good proof environment is worth the
> 
> Can people suggest what good truly introductory stuff is there on s/w proofs ?
> 
> After a litle websearching I have the idea 
>     "Introduction to HOL", M.J.C. Gordon et al, Cambridge U Press 1993 ISBN 0-521-441897]
> might be a misleading title based on this review
>     http://www.cs.nott.ac.uk/~gmh/hol-review.pdf
> that I don't understand.    OTOH
>     http://www.amazon.co.uk/exec/obidos/ASIN/0521441897/202-6191561-7072608
> makes it sound more accessible.

Actually, we'ld be interested in an answer to this as well.

My sense is that there are many prover technologies out there, each
being worked on by a small group for self-defined objectives. There
isn't much in the way of writing targeted at users.

> Anther thing I've never managed to glean from the EROS site is what is the back-end
> structure representing/enacting a capability ?  If I'm holding an opaque blob that
> authorizes something is that an index to some kernel structure that can be viewed as
> a definition writen in some language ?

Yes. In EROS, a capability contains an object ID, a type, and some
permission bits. The type identifies both the kind of kernel resource
and the interface on it that this capability presents.

>   If it's not a language with arbitrary
> expressiveness doesn't that mean the designers have to envisage every possible
> capability that might be wanted ?

EROS is an "extensible" capability system. There is a capability type
that can be served by a user-written program, which allows users to
introduce new object types.

> Would adding some NVRAM make it easier to store all relevant capabilities
> (up to the recent split second) and simplify the process persistance issue
> that's being discussed on this list ?  Would it be acceptable to require an
> NVRAM component in PCs for running Coyotos ?

It would make some things more efficient, but it wouldn't let us beat
the snapshot phase, which is the real problem. Requiring PCs to have
NVRAM in order to run EROS/Coyotos is definitely not an option.

shap