Linux Driver Revisions
for Regression Verification
— ESEC/FSE Evaluated Artifact Collection —
Abstract
This collection of verification tasks was used for experimental evaluation in our ESEC/FSE 2013 paper on "Precision Reuse for Efficient Regression Verification". The tool implementation and the full benchmark results are available on the supplementary web page.
Verification Tasks
The verification tasks have been extracted from the Linux kernel repository (Git repository) using the infrastructure of the Linux Driver Verification (LDV) project. Only commits to the mainline branch were considered. Merge commits that reintegrated branches were considered, and thus no changes are lost. The oldest revisions date back to the year 2007, and the most recent revisions to the end of 2012. The verification tasks are given in GNU C; the files were post-processed using CIL (C Intermediate Language).
Availability
The verification tasks are publicly available in a Git repository at GitLab. The complete set is provided
The verification tasks are released under GPL v2.Structure of Repository
The verification tasks (in directory 'regression-verification-tasks') are organized in one directory for each device driver. The file name of each verification task has the following format: RevisionOrder.AbbreviatedCommitHash.Specification.cil_Verdict.i
| RevisionOrder: | Total order of the revisions; describes in which order the revisions should be verified |
| AbbreviatedCommitHash: | Unique identifier of the revision (see documentation [1] [2] for git log --abbrev-commit) |
| Specification: | Specification that has been encoded into the verification task as reachability problem |
| Verdict: | Reference verdict that states whether the specification is violated (unsafe) or not (safe) |
The repository contains a total of 4521 verification tasks, of which CPAchecker found 103 to be unsafe and 4276 to be safe (for the remaining 142 verification tasks, the verifier could not determine a verification result).
Specifications
The safety properties to check have been encoded as reachability problems into the verification tasks. If the program location labeled with LDV_ERROR is reachable, then the property is violated (a counterexample is found). Table 1 describes all the specifications that have been encoded into the verification tasks. A detailed description of the rules can be found on the website of the Linux Driver Verification project.| Name | Description |
|---|---|
| 08_1a | For each successful call to try_module_get(), a corresponding call to module_put() that unblocks the module must exist. |
| 32_1 | A less accurate implementation of specification 32_7a. |
| 32_7a | A mutex must not be acquired or released twice. A mutex must not be released without prior acquiring. Finally, all mutexes must be released. |
| 39_7a | A spin lock must not be acquired or released twice. A spin lock must not be released without prior acquiring. Finally, all spin locks must be released. |
| 43_1a | The flag for atomic allocation operations must be used whenever a memory-allocation function is called while a spin lock is held. |
| 68_1 | For each allocation of an USB Request Block (URB) using usb_alloc_urb(), a corresponding call to usb_free_urb() must exist. |
Entry Function
The name of the entry (main) function of the verification task is either ldv_main0_sequence_infinite_withcheck_stateful or ldv_main1_sequence_infinite_withcheck_stateful.Drivers
Table 2 gives a short overview of all drivers for which verification tasks are included. Each directory in the repository corresponds to one driver. Slashes (/) were replaced by double-dashes (--) in names of the directories in the repository.
| Driver | Revisions | Covered Driver Source Files |
|---|---|---|
| auxdisplay/cfag12864b.ko | 4 | auxdisplay/cfag12864b.c |
| block/drbd/drbd.ko | 158 | block/drbd/{ drbd_bitmap.c, drbd_proc.c, drbd_worker.c, drbd_receiver.c, drbd_req.c, drbd_actlog.c, drbd_main.c, drbd_strings.c, drbd_nl.c } |
| block/paride/pt.ko | 12 | block/paride/pt.c |
| cpufreq/pcc-cpufreq.ko | 3 | cpufreq/pcc-cpufreq.c |
| gpu/drm/i2c/sil164.ko | 3 | gpu/drm/i2c/sil164_drv.c |
| gpu/drm/i915/i915.ko | 79 | gpu/drm/i915/{ i915_drv.c, i915_dma.c, i915_irq.c, i915_debugfs.c, i915_suspend.c, i915_gem.c, i915_gem_debug.c, i915_gem_evict.c, i915_gem_execbuffer.c, i915_gem_gtt.c, i915_gem_stolen.c, i915_gem_tiling.c, i915_sysfs.c, i915_trace_points.c, intel_display.c, intel_crt.c, intel_lvds.c, intel_bios.c, intel_ddi.c, intel_dp.c, intel_hdmi.c, intel_sdvo.c, intel_modes.c, intel_panel.c, intel_pm.c, intel_i2c.c, intel_fb.c, intel_tv.c, intel_dvo.c, intel_ringbuffer.c, intel_overlay.c, intel_sprite.c, intel_opregion.c, dvo_ch7xxx.c, dvo_ch7017.c, dvo_ivch.c, dvo_tfp410.c, dvo_sil164.c, i915_gem_dmabuf.c, i915_ioc32.c, intel_acpi.c } |
| hwmon/ads7871.ko | 10 | hwmon/ads7871.c |
| hwmon/it87.ko | 59 | hwmon/it87.c |
| i2c/algos/i2c-algo-pca.ko | 14 | i2c/algos/i2c-algo-pca.c |
| input/joystick/magellan.ko | 2 | input/joystick/magellan.c |
| input/joystick/spaceorb.ko | 2 | input/joystick/spaceorb.c |
| input/joystick/twidjoy.ko | 2 | input/joystick/twidjoy.c |
| input/misc/keyspan_remote.ko | 9 | input/misc/keyspan_remote.c |
| input/mouse/vsxxxaa.ko | 4 | input/mouse/vsxxxaa.c |
| isdn/mISDN/mISDN_core.ko | 59 | isdn/mISDN/{ core.c, fsm.c, socket.c, clock.c, hwchannel.c, stack.c, layer1.c, layer2.c, tei.c, timerdev.c } |
| leds/leds-bd2802.ko | 14 | leds/leds-bd2802.c |
| media/common/tuners/mt2266.ko | 5 | media/common/tuners/mt2266.c |
| media/dvb/dvb-usb/dvb-usb-az6007.ko | 5 | media/dvb/dvb-usb/az6007.c |
| media/dvb/dvb-usb/dvb-usb-rtl28xxu.ko | 10 | media/dvb/dvb-usb/rtl28xxu.c |
| media/dvb/dvb-usb/dvb-usb-vp7045.ko | 12 | media/dvb/dvb-usb/{ vp7045.c, vp7045-fe.c } |
| media/dvb/frontends/cxd2820r.ko | 23 | media/dvb/frontends/{ cxd2820r_core.c, cxd2820r_c.c, cxd2820r_t.c, cxd2820r_t2.c } |
| media/dvb/ttpci/budget-patch.ko | 9 | media/dvb/ttpci/budget-patch.c |
| media/video/cx231xx/cx231xx-dvb.ko | 13 | media/video/cx231xx/cx231xx-dvb.c |
| media/video/videobuf-vmalloc.ko | 31 | media/video/videobuf-vmalloc.c |
| message/i2o/i2o_scsi.ko | 7 | message/i2o/i2o_scsi.c |
| mfd/janz-cmodio.ko | 11 | mfd/janz-cmodio.c |
| mtd/ar7part.ko | 6 | mtd/ar7part.c |
| mtd/devices/slram.ko | 9 | mtd/devices/slram.c |
| mtd/maps/intel_vr_nor.ko | 10 | mtd/maps/intel_vr_nor.c |
| mtd/mtdoops.ko | 41 | mtd/mtdoops.c |
| net/arcnet/com20020_cs.ko | 2 | net/arcnet/com20020_cs.c |
| net/can/usb/ems_usb.ko | 21 | net/can/usb/ems_usb.c |
| net/phy/dp83640.ko | 16 | net/phy/dp83640.c |
| net/phy/spi_ks8995.ko | 4 | net/phy/spi_ks8995.c |
| net/tokenring/abyss.ko | 4 | net/tokenring/abyss.c |
| net/usb/catc.ko | 22 | net/usb/catc.c |
| net/wan/farsync.ko | 22 | net/wan/farsync.c |
| net/wireless/wl12xx/wl12xx_sdio.ko | 38 | net/wireless/wl12xx/sdio.c |
| platform/x86/panasonic-laptop.ko | 16 | platform/x86/panasonic-laptop.c |
| regulator/gpio-regulator.ko | 20 | regulator/gpio-regulator.c |
| regulator/wm831x-dcdc.ko | 34 | regulator/wm831x-dcdc.c |
| rtc/rtc-m41t93.ko | 6 | rtc/rtc-m41t93.c |
| rtc/rtc-max6902.ko | 9 | rtc/rtc-max6902.c |
| rtc/rtc-pcf2123.ko | 9 | rtc/rtc-pcf2123.c |
| scsi/dmx3191d.ko | 2 | scsi/dmx3191d.c |
| scsi/pcmcia/sym53c500_cs.ko | 20 | scsi/pcmcia/sym53c500_cs.c |
| staging/comedi/drivers/adl_pci7432.ko | 13 | staging/comedi/adl_pci7432.c |
| staging/comedi/drivers/comedi_bond.ko | 13 | staging/comedi/comedi_bond.c |
| target/loopback/tcm_loop.ko | 41 | target/loopback/tcm_loop.c |
| tty/serial/uartlite.ko | 9 | tty/serial/uartlite.c |
| tty/serial/xilinx_uartps.ko | 3 | tty/serial/xilinx_uartps.c |
| uio/uio_sercos3.ko | 5 | uio/uio_sercos3.c |
| usb/otg/ab8500-usb.ko | 6 | usb/otg/ab8500-usb.c |
| usb/serial/cp210x.ko | 71 | usb/serial/cp210x.c |
| usb/serial/metro-usb.ko | 25 | usb/serial/metro-usb.c |
| usb/serial/mos7840.ko | 60 | usb/serial/mos7840.c |
| usb/serial/spcp8x5.ko | 37 | usb/serial/spcp8x5.c |
| usb/serial/ssu100.ko | 28 | usb/serial/ssu100.c |
| video/arkfb.ko | 22 | video/arkfb.c |
| video/backlight/lms283gf05.ko | 13 | video/backlight/lms283gf05.c |
| video/backlight/tdo24m.ko | 12 | video/backlight/tdo24m.c |
| video/matrox/i2c-matroxfb.ko | 7 | video/matrox/i2c-matroxfb.c |
Original Source Code
To obtain the original source code, one needs to clone the Git repository of the Linux kernel (or open it via browser), checkout the desired revision using the "AbbreviatedCommitHash" (or open in browser by means of setting "AbbreviatedCommitHash" in a link, e.g., http://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/commit/?id=30b743a), and choose one of C source file he/she is interested in. The verification tasks contain #line preprocessor directives that reference the files and line numbers from the original source code.