l4-hurd
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A Question to throw at you guys


From: Sam Mason
Subject: Re: A Question to throw at you guys
Date: Mon, 13 Nov 2006 19:31:39 +0000
User-agent: Mutt/1.5.13 (2006-08-11)

On Sun, Nov 12, 2006 at 10:57:32PM +0000, Justin Emmanuel wrote:
> I would also like to know your comments criticisms on
> the concept of what I like to call a Driver Description Language. If it has
> already been developed, then I have never heard of it, please let me know
> where I can go and pick up more information on it.

Sounds like a specific instance of proving the safety of code.  You're
going to be interacting with (potentially buggy) hardware as well, so
it's going to take much more work but could be fun.  I'm pretty sure you
wouldn't need a whole new implementation language though.

The main things you appear to need are models of the hardware, programming
language, and the target API.  Your code would fill in the gap allowing
you to check various safety properties of your driver.  Not sure if
anyone has attempted it and my limited search has come up with lots of
driver analysis tools for MS Windows, but not much else.  The Microsoft
stuff all seems to be checking that the driver conforms to their API,
rather than if the driver is actually driving the hardware correctly.

If people do go down this direction (I suppose) it would be possible to
have the hardware manufacturer produce the hardware model and provide
guarantees that their hardware actually does what they've said it does.
Not sure who would supply the other bits though.

Unfortunately I don't think it's a very easy set of problems to solve
though.  It would be amazing if it was solved though.


  Sam




reply via email to

[Prev in Thread] Current Thread [Next in Thread]