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 _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
