On 11/22/2011 11:37 PM, Jiri Kosina wrote:
On Thu, 17 Nov 2011, Willem Penninckx wrote:
usb_kbd_event() and usb_kbd_led() can be called concurrently, but they are not
synchronized. They both readwrite kbd->leds, and usb_kbd_event() originally just
checked the URB status field, while urb.h states that "It [status field] should
not be examined before the URB is returned to the completion handler."
To fix this unsynchronized behavior, this patch introduces a boolean
representing whether the URB is submitted, and a spinlock.
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.
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.
Thanks,
Kind regards,
Willem Penninckx
Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
--
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
