Don't hardwire OS features

[Alexander Bostrom]

Rideau wrote:

>   In Tunes, the interrupted task would be basically be told
>"now do your best to yield execution ASAP,
>after putting the system in a rightful state".
>The task would exit the current loop/iteration,
>restore invariants needed for concurrent GC/whatever to take place,
>then call the scheduler for next task.

But what if it doesn't? Do you mean the proof system have ruled out such a
situation already, perhaps by having a prerequisite saying that for example
the objects/processes handling the network, floppy (input, but also output)
or .MOD player must always get control quickly enough not to allow lack of
preemption to slow them down?

Maybe that could be made (or automatically becomes?) an implementetion
issue that you (the user/programmer) don't have to care about as long as
you stick to HLL (as opposed to LLL).


>Yes yes yes. Object code should be irreversibly produced for a particular
>target, while a *high-level* language or maximal possible expressivity
>should be used to represent user-level and/or portable objects.

What about people (companies) who wants to keep their source code secret?
Should they be shot? :-) Are they not GNU-ish enough? As long as every
object is small enough and has enough information/documentation about it's
behaviour (a proof maybe?), it can always be rewritten by people who would
like to modify it, so the problem is one of making the docs fine-grained
enough. Maybe not something Macrosoft would agree to do...


---
Alex                                           e96_abo@e.kth.se
                                   http://www.e.kth.se/~e96_abo/
                                         (really)