On Wed, 23 Nov 2011, Willem Penninckx wrote: > > Interesting. Thanks for the fix. > > > > Out of curiosity -- how did you find this out? I would have hoped noone is > > using these drivers. > > I used this driver to perform formal software verification on a "real" (i.e. > not an artificial toy) kernel driver. The verified properties include absence > of illegal memory accesses, absence of race conditions, and some API rules > (e.g. the rule "do not access the URB status field before the URB is returned > to the completion handler" mentioned by the first patch). The verifier used > was VeriFast, which is a research prototype. > > usbkbd was chosen because it was considered small enough for trying out the > verification approach an a real driver for the first time. This did not take > the complexity of mainly the USB API into account, which made it a bit more > time-consuming than expected. > > The bugs fixed in the two patches are the ones found and fixed during the > verification process. Ah, I see. > > > Signed-off-by: Willem Penninckx<willem.penninckx@xxxxxxxxxxxxxx> > > > > > > --- linux-3.2-rc2/drivers/hid/usbhid/usbkbd.c 2011-11-15 > > > 18:02:59.000000000 +0100 > > > +++ linux-3.2-rc2/drivers/hid/usbhid/usbkbd-patch1.c 2011-11-17 > > > 10:21:18.099036158 +0100 > > > > Could you please resend the patch in a standardized kernel format so that > > I could apply it with patch -p1? (and the same holds for the second patch > > you have sent). > > I re-diffed using git this time, see next mail. Please ask me to do it again > if it is still not in standardized format. Yes, these were in proper format, and I have queued those. Thanks, -- Jiri Kosina SUSE Labs -- To unsubscribe from this list: send the line "unsubscribe linux-usb" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
