RE: [BULK] - Re: Verification of Device Drivers

Ouch!!. I should be the one to apoligize for the last sentence. I did not mean U at all. I’ve seen here people sometime throws question(s) w/o detail, and that makes lot of people upset. That last sentence is not context sensitive.

Sorry, sorry …

-prokash
----- Original Message -----
From: Xinyu Feng
To: Windows System Software Devs Interest List
Sent: Wednesday, November 05, 2003 6:00 PM
Subject: [ntdev] RE: [BULK] - Re: Verification of Device Drivers

Dear All:

Since I am not a native speaker of English, if there are anything make you feel offended, I appologize and please believe me that I do not mean to do so.

– Xinyu

Prokash Sinha wrote:

Let’s not start another round of b(f)lame war. Some time “The art of asking question” is really important though !!!

It’s an earnest request…

-prokash
----- Original Message -----
From: Mesdaq, Ali
To: Windows System Software Devs Interest List
Sent: Wednesday, November 05, 2003 2:00 PM
Subject: [ntdev] RE: [BULK] - Re: Verification of Device Drivers

Get off your high horse he wasn’t trying to sell you anything. I think he was just asking for his own research. I see nothing wrong with the advice that everyone else gave him. Maybe since you have so much experience you can also give him some useful advice instead of attacking him personally.

-----Original Message-----
From: Gary G. Little [mailto:xxxxx@seagate.com]
Sent: Wednesday, November 05, 2003 1:52 PM
To: Windows System Software Devs Interest List
Subject: [BULK] - [ntdev] Re: Verification of Device Drivers

Prokash,

Driver Verifier is part of the OS, and does NOT require the DDK.

Xinyu,

My first question is what qualifies you for the task? The fact that you are
a Ph.D. student at Yale or the Computer Science Department at Yale? My
apologies, but some of the worst code I have ever seen was developed by
graduates with such academic credentials.

How many commercial drivers for Windows NT and above have you and your
department produced and sold to commercial enterprises? How many lines of
functional driver code, in daily use, have you or your department produced?
Do I have any of those commercially released drivers or lines of code in any
of the systems that I work on? In other words, what credentials do you bring
to the task of producing a tool that a 30 year veteran of kernel mode and
driver writing MIGHT want to use? Sorry … but a Ph.D. from Yale doesn’t
mean you even know how to parse a doubly linked list, let alone assist me in
debugging a multiplex problem in synchronization of a multilayered driver
stack running on 4 hyper-threaded processes with a required data throughput
of 2 gigabits per second.

You need practical experience to produce any kind of a tool that would even
be remotely useful, and surveying experienced programmers will not give you
what you, or we, need.


Gary G. Little
Seagate Technologies, LLC

“Prokash Sinha” wrote in message news:xxxxx@ntdev…
>
> Hi Xinyu,
>
> There are some tools already out there do the verifications you mentioned
> already, so in my opinion it would be wise to take a look at those tools
> first to comeup with a list of types of errors you would like to cover

> As an example, though might not be exhaustive -
>
> There is a driver verifier that comes with DDK, it does lot of
> checking/verifying.
>
> There are krnl debugger extension, that does deadlock analysis, and that
too
> comes with windbg, but it does not do prevention analysis if I’m correct
!!!
>
> There are tools from Compuware(Numega) that does code coverage, memory
leak
> analysis…
>
> There is no automatic garbage collector, so there is no analysis there as
of
> now, but in the future it seems like a logical direction.
>
> So in essence, my recommendation is to study those tools first to get an
> idea of what is/are already provided. Finally there are lots of stuff up
in
> MS’s that are being cooked and not quite in the market for their
primetime,
> so it might be a good idea to get connected with them, so that you dont
come
> with something that is well researched and bitten to death by MS
> research/dev people…
>
> -prokash
> ----- Original Message -----
> From: “Xinyu Feng”
> To: “Windows System Software Devs Interest List”
> Sent: Tuesday, November 04, 2003 11:43 PM
> Subject: [ntdev] Verification of Device Drivers
>
>
> > Dear All:
> >
> > I’m a Ph.D. student at the Department of Computer Science, Yale
> > Univ. One of our ongoing project is to use formal methods to verify the
> > correctness of the Device drivers/System BIOS. My question is, as device
> > driver developers/programmers, what kind of properties do you interested
> > in your program? In other words, what kind of problems/bugs do you
> > encounter most frequently? If I have an ideal tool that can verify any
> > properties you want (e.g. memory safety, type safety, deadlock free,
> > etc), what kind of properties do you want to verify?
> >
> > You response would be highly appreciated!
> >
> > Best,
> >
> > – Xinyu
> >
> >
> > —
> > Questions? First check the Kernel Driver FAQ at
> http://www.osronline.com/article.cfm?id=256
> >
> > You are currently subscribed to ntdev as: xxxxx@garlic.com
> > To unsubscribe send a blank email to xxxxx@lists.osr.com
> >
> >
>
>
>
>


Questions? First check the Kernel Driver FAQ at http://www.osronline.com/article.cfm?id=256

You are currently subscribed to ntdev as: xxxxx@websense.com
To unsubscribe send a blank email to xxxxx@lists.osr.com


Questions? First check the Kernel Driver FAQ at http://www.osronline.com/article.cfm?id=256

You are currently subscribed to ntdev as: xxxxx@garlic.com
To unsubscribe send a blank email to xxxxx@lists.osr.com

Questions? First check the Kernel Driver FAQ at http://www.osronline.com/article.cfm?id=256

You are currently subscribed to ntdev as: xxxxx@yale.edu
To unsubscribe send a blank email to xxxxx@lists.osr.com


Questions? First check the Kernel Driver FAQ at http://www.osronline.com/article.cfm?id=256

You are currently subscribed to ntdev as: xxxxx@garlic.com
To unsubscribe send a blank email to xxxxx@lists.osr.com