2001-03-21 17:26:05

by Chiaki

[permalink] [raw]
Subject: Interesting post from the MC project to linux-kernel. :block while spinlock held...

Hi,

I suppose that many SCSI maintainers do read the linux-kernel
mailing list. However, just in case, I am quoting one of the
very interesting postings that come from people at Stanford.
They seem to be doing mechanical verification / checking of
linux source code to hunt for potentical bugs. In the last week or so,
many potential bugs were identified and fixed.

Here is one that might be of interest to SCSI developers.
The checkers are known to produce false positives. So beware.

--- begin quote ---
> enclosed are 163 potential bugs in 2.4.1 where blocking functions are
> called with either interrupts disabled or a spin lock held. The
> checker works by:

Here's the file manifest. Apologies.

drivers/atm/idt77105.c
drivers/atm/iphase.c
drivers/atm/uPD98402.c
drivers/block/cciss.c
drivers/block/cpqarray.c
drivers/char/applicom.c
...
drivers/scsi/aha1542.c <--- some scsi files
drivers/scsi/atp870u.c <----
drivers/scsi/psi240i.c <----
drivers/scsi/sym53c416.c <----
drivers/scsi/tmscsim.c <----
...
[the rest omiitted]

--- end quote ---



2001-03-22 12:32:53

by David Woodhouse

[permalink] [raw]
Subject: Re: Interesting post from the MC project to linux-kernel. :block while spinlock held...


[email protected] said:
> drivers/char/applicom.c

There's a rewrite of this for the new PCI API. Doesn't yet support the ISA
cards because I didn't have one to test with. I'll try to get hold of one
and submit it.

--
dwmw2


2001-03-22 17:08:17

by Kurt Garloff

[permalink] [raw]
Subject: Re: Interesting post from the MC project to linux-kernel. :block while spinlock held...

On Thu, Mar 22, 2001 at 02:24:56AM +0900, Chiaki Ishikawa wrote:
> --- begin quote ---
> > enclosed are 163 potential bugs in 2.4.1 where blocking functions are
> > called with either interrupts disabled or a spin lock held. The
> > checker works by:
>
> Here's the file manifest. Apologies.
>
> drivers/atm/idt77105.c
> drivers/atm/iphase.c
> drivers/atm/uPD98402.c
> drivers/block/cciss.c
> drivers/block/cpqarray.c
> drivers/char/applicom.c
> ...
> drivers/scsi/aha1542.c <--- some scsi files
> drivers/scsi/atp870u.c <----
> drivers/scsi/psi240i.c <----
> drivers/scsi/sym53c416.c <----
> drivers/scsi/tmscsim.c <----
^^^^^^^^^^^^^^^^^^^^^^

How do I fond about about details?

Regards,
--
Kurt Garloff <[email protected]> Eindhoven, NL
GPG key: See mail header, key servers Linux kernel development
SuSE GmbH, Nuernberg, FRG SCSI, Security


Attachments:
(No filename) (975.00 B)
(No filename) (232.00 B)
Download all attachments

2001-03-24 00:01:07

by Chiaki

[permalink] [raw]
Subject: Re: Interesting post from the MC project to linux-kernel. :block while spinlock held...

Hello Garloff-san,

Actually, a good question.

I have been trying to find the details of the verification tool from stanford

but to no avail.
Maybe we should ask the posters from the Stanford directly.

(Oops. I thought I posted this to linux-scsi, but did I post
linux-kernel instead? Apologies.)

Kurt Garloff wrote:

> On Thu, Mar 22, 2001 at 02:24:56AM +0900, Chiaki Ishikawa wrote:
> > --- begin quote ---
> > > enclosed are 163 potential bugs in 2.4.1 where blocking functions are
> > > called with either interrupts disabled or a spin lock held. The
> > > checker works by:
> >
> > Here's the file manifest. Apologies.
> >
> > drivers/atm/idt77105.c
> > drivers/atm/iphase.c
> > drivers/atm/uPD98402.c
> > drivers/block/cciss.c
> > drivers/block/cpqarray.c
> > drivers/char/applicom.c
> > ...
> > drivers/scsi/aha1542.c <--- some scsi files
> > drivers/scsi/atp870u.c <----
> > drivers/scsi/psi240i.c <----
> > drivers/scsi/sym53c416.c <----
> > drivers/scsi/tmscsim.c <----
> ^^^^^^^^^^^^^^^^^^^^^^
>
> How do I fond about about details?
>
> R