Interesting post from the MC project to linux-kernel. :block while spinlock held...

Interesting post from the MC project to linux-kernel. :block while spinlock held...

[Ishikawa]

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 ---

Re: Interesting post from the MC project to linux-kernel. :block while spinlock held...

[David Woodhouse]

ishikawa@yk.rim.or.jp 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

Re: Interesting post from the MC project to linux-kernel. :block while spinlock held...

[Kurt Garloff]

[-- Attachment #1: Type: text/plain, Size: 1004 bytes --]

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  <garloff@suse.de>                          Eindhoven, NL
GPG key: See mail header, key servers         Linux kernel development
SuSE GmbH, Nuernberg, FRG                               SCSI, Security

[-- Attachment #2: Type: application/pgp-signature, Size: 232 bytes --]

Re: Interesting post from the MC project to linux-kernel. :block while spinlock held...

[Ishikawa]

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