Don't hardwire OS features

[Alaric B. Williams]

On  5 Dec 96 at 9:10, Francois-Rene Rideau wrote:

A BIG message!

> > Eiffel was designed so it is possible to prove things, just no 
> > compilers do much proving beyond type inference. So Far.
>
> Surely I should re-read more in detail the Eiffel specs.
> But from what I know of Eiffel practice,
> only computable checks are used as pre/post-conditions,
> which severely limits the expressiveness of the specification system.

Hmmm. I'm not sure which restrictions apply. But surely they can be 
relaxed...

> Also, building a specification system with the belief
> that automated proofs are possible independently of specifications
> is illusory.

Specifications of what? Many things are 'specified' in Eiffel.

> > That can be done quite easily, IMHO. Enumerate the things that cause 
> > crashes, and mask them off.
>
> No, that can't be. Because there are infinitely
> many things that may cause crash,
> and masking them off is not computable.

I'm not considering going into infinite loops as crashes here; they 
only affect the affected application. I'm talking about 
corrupting/hogging system resources. If we can prevent that, 
applications are welcome to nosedive as long as they don't take 
anything else down!
 
> Not if we use the exception-recovery technique I've described
> at length in the tunes-lll list before (see LLL/ page).
> Currently, even Linux now uses a (restricted version) of this technique:
> the exception handler uses code recovery technique
> to replace software test for validity of user-memory access in the kernel.

I'll go look at that someday...
 
> Oops. This is a mistranslated french word: "place" in french means space.

That must be confusing when you have to think of them seperately in 
other languages!

> Typical example of a syntax-preserving, semantic-modifying transformation,
> whereas what we mean is to preserve semantics (==meaning), not syntax!
> So you see that even for an experienced programmer,
> a few seconds being careless will introduce dreadful bugs,
> that can only be detected by semantic-checking, not syntax-checking.

Perfect example :-)

> > Anyway, back to the thread. The most minimal trap handling code would
> > print an apologetic message to some kind of output system, then kill
> > that task/process/address space/module/whatever...
>
> That's already too little/too much.
> In a development system,
> In a compiled system, unless in debugging mode,
> traps would not be needed as error behavior,
> but only, perhaps, as a way to optimize
> some tests that only seldom fail.

Okay then - a signal handling system like Unix takes little space, 
and allows us to take control of exception handling ourselves. QNX 
does it in 8k!

> Though by definition coprocessors should have specialized circuits
> for their special purpose, again, I'm confident that a MISC approach
> for the non-critical parts of the design will greatly benefit
> the overall performance/cost ratio of the machine.
> Well, if this discussion is to continue,
> let's do it on the MISC mailing-list.
> Ask MISC-request@pisa.rockefeller.edu to join in...

Cool, if I get time :-)

> > You could strip floating point off a C implementation, just it'd be
> > harder than removing stdio streams! The division between "in the
> > compiler" and "in the standard libraries" is quite arbitary; some
> > languages just make it more syntactically visible.
>
> Well, let's say that the problem is not as much
> "what is the status of standardized words?",
> as "how can new words be defined?".

Right. Ideally, a compiler should define basic constructs for 
specifying localised output semantics (machine code) and the best 
ways of joining them together... things like addition and all that 
are defined on top.

> > I mean, a mathematical system for converting from syntax A to syntax 
> > B, with the /maximum/ efficiency possible. As in, if syntax A is a 
> > turing machine, and syntax B contains a simple instruction for most 
> > of what a neural net does, then a neural network implemented in A 
> > will use this instruction in B. IE, the ultimate compiler will be one 
> > application of a fundamental theory of computation!
>
> No need for a lot of fundamental theory to show that
> such thing is not computable.

Maybe not always computable, but if we place reasonable restrictions 
(like, all of our semantic contructs can be represented by a finite 
piece of code in another syntax) then it looks easier. But only 
/relatively/ easier :-)
  
> > Yes, but if we write code for Linux and try to compile it on my DOS 
> > machine with DJGPP, it won't find asm/*.h and I'll have to figure out 
> > exactly what they did from gcc's error messages and write them 
> > myself!
>
> That's why you can copy the asm/*.h from Linux,
> assuming, of course, you're writing GPLed software,
> or rewrite them, if you're not.
> [Followup to another place, too]

Final point: then the developer has all the horrid work of dragging
around possibly unnecessary (if it's compiled on Linux in the end)
utility code with his product! What if he'd used a real /big/ 
'optional' feature??? This problem still remains mostly unexamined as 
far as I see...

> >> C is architecture-dependent anyway (pointer sizes, etc).
> >
> > Yes, but our languages won't be!
>
> The standard portable languages shan't.
> But it might be expedient to use a semi-portable arch-dep layer
> for bootstrap purposes only
> (not in any case intended as a long-term user-wise standard).

Well, that's a special case... not a real worry...
 
> There are lots of books and articles on the net about functional
> programming. I don't know if there are good Tutorials, though.
> Try the docs for the OCAML language, to begin with;
> I believe there's a good tutorial, or at least a user guide.
> I you have plenty of RAM to waste,
> you might prefer to get the more standard SML/NJ.

Ok, thanx...
 
> > Yes, I agree, now I see what you're aiming at!
> >
> I'm glad my english is not completely ununderstandable, after all...

The grammar was perfect, it's just some concepts are hard to push 
through a syntax designed for telling each other were food is :-) 
 
> > I think "atomic"'s a nice word; it implies we don't have to deal with 
> > internal structure (meaning "indivisible")!
> I would oppose counter-arguments, but let's not argue about names.
> Follow-up to private e-mail if you want.

It's not important :-)
 
> Which means that the system should be able to consistently
> manage multiple versions of the "same" object...

Depending on the cost of conversion - if conversion is really slow, 
then by all means operate on RGB and Yu'v' bitmaps side by side, then 
select the one you need to send out, etc. This behaviour can be 
implemented, I think...
 
> > Oh, right. In set theory we define subsets like so:
> > 
> > {x epsilon super_set; x satisfies condition}
> >
> Nope. The "is element of" symbol is not an epsilon.
> Try looking in a dictionary of feeding TeX with \epsilon
> to see what it's like.

It's a little epsilon! Big epsilon is E, little epsilon is an E with 
curves instead of corners, the symbol I use for "is element of"!
 
> This means that "epsilon x.P" is any object fulfilling property "P",

Yup. "epsilon x.IsHungry" includes me, currently...

> which, if well defined, constitutes a proof for formula "exists x.P",

Right.

> while "lambda x.E" is a function that associates value of expression "E"
> to an object "x",

Uhuh. Such as the height of object x. It associates a value with this 
concept. I've heard of lambda before.

> and, if well defined, constitutes a proof for
> formula "forall x.(formula proven by E)".

Hmmm. I'll pass on that for a year or so.

> > Ahah. Have you heard of the Self system?
> Yeah. Tried it on a Sparc20 with "only" 32 megs or RAM.
> Just couldn't stand the slowness, so didn't explore it much.
> I like many things about it,
> but surely, a language for proofs is not what they tried to achieve...

Indeed...

> >>>[Security concept for ARGON]
> >> Ahem. And did you choose scoping as the basic protection paradigm,
> >> as in Tunes?
> > It's possibly semanticall equivelant to scoping. 
> Why not simply make it scoping, then???

Because I've never studied applying the phenomenon of scoping to this 
much. This arose independently.
 
> > Such that if you are "told about" an entity, you can access it. But you 
> > can only tell something about an entity to a certain level.

> Which is scoping with views on objects.

By any other name...

> That is, one has the green view on the object in scope,
> but not the indigo.

Right.

> This might be a simple way to standardize access to objects
> at some external level; it requires no special core system support;
> all the core system need implement is scoping.

Well my core system need implement nothing. This is a behaviour made 
available by the metaentity (call it a base class). Any entity can 
make use of it or not as the case may be. It may also use it 
internally, by creating lock objects (which are in charge of checking 
keys, objects which are given as proofs of knowledge. Typically large 
integers so they can't be bruteforced). These lock objects can be 
combined with keys to form colours as described above, which can then 
be used for less abstract security checks. But this probably won't be 
necessary very often. 
 
> You biggest security problem is likely to be with traitor commie mutants...

(puzzlement)
 
> > none = no access possible.
> > red = opaque visibility; you cannot use the entity, but you can ask 
> > it what it is, that kind of thing. Usually granted to container 
> > entities.
> > ...
> > violet = adminsitrative powers
> Shouldn't it be ultra-violet?
> Or perhaps that's reserved to single-user system debugging?

Well I didn't figure there'd be need for any extra colours. We could 
reserve the X-ray spectrum for the NSA... they can access them by 
having us escrow our keys :-)
 
> > It's simple and flexible...
> >  ...perhaps I should try and define a fundamental calculus of access 
> > control? There are so many schemes, but the field feels like there's 
> > a mathematical basis to be found...
>
> Let's keep it simple, and make it scoping plus standard naming.

Perhaps set theory is good enough, anyway :o)
 
ABW

--
Governments are merely protection rackets with good images.

Alaric B. Williams Internet : alaric@abwillms.demon.co.uk
<A HREF="http://www.abwillms.demon.co.uk/">http://www.abwillms.demon.co.uk/</A>