Gary,
If you have a programming job today, you should thank those computer science
Ph.D. dudes.
Your C language was invented by computer science guys at an AT&T research
lab, based on a marvelously compact language called BCPL, which was invented
by a computer scientist at the University of Cambridge in the UK. Virtual
memory was invented by computer scientists at the University of Manchester
in England. Modern multithreading and multi-user operation was pioneered
among others by the CTSS system developed at MIT. Windowed interfaces were
created at the Xerox Park laboratory, again, by a bunch of bright computer
science types. Postscript was created by a Ph.D. The internet, together with
all its protocols, was also created by researchy Ph.D. dudes, and it took a
good many years before anyone outside the university and research lab
circuit had anything to do with it. Modern computer architectures were
created by such types as Dr. Flynn, who was one of the architects of the
IBM/360, or by Drs. Hennessy and Patterson who created RISC machines.
Computer graphics and 3D pipelines were created by computer scientists from
places such as the University of Utah, SGI, and others. Modern operating
systems evolved from things such as Multics, created, again, by computer
scientists.
I could go on. I don’t know about you, but I’m old enough to remember when
some of those were born, I was already programming. It’s this simple: no
academic dudes, no computers, no operating systems, no drivers, and no
programming languages.
Your synchronization of a multilayered driver stack in a Windows NT
environment would greatly benefit by the sound application of some computer
science concepts. Synchronization is a problem that’s been well studied, and
there are powerful tools to handle it: for example, try MPI or OpenMP,
again, both begotten in the computer sciency circuit. But hey, if you design
an OS like a ghost from christmases past, you deserve what you get ! But
back in the seventies Dr. Hoare put out his capital paper on CSP which is
the father of contemporary synchronization techniques. And what do you know,
big ticket MIMD machines such as the CM5 were created by academics too, and
their parallelism dwarfs that of a PC. Have you programmed a 16,384
processor machine ? I have, and few outside the academic and researchy
circles have ever had the privilege to play with that much parallelism and
that much power.
For your 2 gigabits per second, it’s this simple: get yourself good hardware
and it’ll happen. Maybe back in the fifties or sixties it was a good idea to
handicraft a piece of code to squeeze as much speed as possible, but today,
hey, get another computer, it’s way cheaper. With today’s hardware
development tools, it hardly makes sense to write something in C when it’s
possible to write it much better in HDL - but old habits die hard.
Computer science is upstream from what you and I do for a living. We
capitalize on their results, we live off the techniques they create. If they
didn’t exist, we wouldn’t have the jobs we have !
Alberto.
-----Original Message-----
From: Gary G. Little [mailto:xxxxx@seagate.com]
Sent: Wednesday, November 05, 2003 4:52 PM
To: Windows System Software Devs Interest List
Subject: [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@compuware.com
To unsubscribe send a blank email to xxxxx@lists.osr.com
The contents of this e-mail are intended for the named addressee only. It
contains information that may be confidential. Unless you are the named
addressee or an authorized designee, you may not copy or use it, or disclose
it to anyone else. If you received it in error please notify us immediately
and then destroy it.
