BLASTing Linux Code

Jan Tobias Mühlberg and Gerald Lüttgen
Department of Computer Science, University of York, York YO10 5DD, U.K.

main page | next example

Commit Overview | Files | Comments

Checking Locking Properties: Example 1

Commit Overview

Commit Key d7283d61302798c0c57118e53d7732bec94f8d42
Subject [PATCH] libata: locking rewrite (== fix)
Description [libata] locking rewrite (== fix)
A lot of power packed into a little patch.
This change eliminates the sharing between our controller-wide spinlock and the SCSI core's Scsi_Host lock. As the locking in libata was already highly compartmentalized, always referencing our own lock, and never scsi_host::host_lock.
As a side effect, this change eliminates a deadlock from calling scsi_finish_command() while inside our spinlock.
Requires Linux 2.6.14 kernel source as from git://

--- a/drivers/scsi/libata-core.c
+++ b/drivers/scsi/libata-core.c
@@ -3916,8 +3916,6 @@ static void ata_host_init(struct ata_por
host->unique_id = ata_unique_id++;
host->max_cmd_len = 12;
- scsi_assign_lock(host, &host_set->lock);
ap->id = host->unique_id;
ap->host = host;

--- a/drivers/scsi/libata-scsi.c
+++ b/drivers/scsi/libata-scsi.c
@@ -39,6 +39,7 @@
#include <scsi/scsi.h>
#include "scsi.h"
#include <scsi/scsi_host.h>
+#include <scsi/scsi_device.h>
#include <linux/libata.h>
#include <asm/uaccess.h>
@@ -1565,8 +1566,12 @@ int ata_scsi_queuecmd(struct scsi_cmnd *
struct ata_port *ap;
struct ata_device *dev;
struct scsi_device *scsidev = cmd->device;
+ struct Scsi_Host *shost = scsidev->host;
- ap = (struct ata_port *) &scsidev->host->hostdata[0];
+ ap = (struct ata_port *) &shost->hostdata[0];
+ spin_unlock(shost->host_lock);
+ spin_lock(&ap->host_set->lock);
ata_scsi_dump_cdb(ap, cmd);
@@ -1589,6 +1594,8 @@ int ata_scsi_queuecmd(struct scsi_cmnd *
ata_scsi_translate(ap, dev, cmd, done, atapi_xlat);
+ spin_unlock(&ap->host_set->lock);
+ spin_lock(shost->host_lock);
return 0;

(purple: line numbers and function names; red: line removed; green: line added)


Unmodified sources

Related files


This is the running example for Section 4, "Checking Locking Properties". The example code contains a deadlock caused by a API rule violation: The functions spin_lock() and spin_unlock() must be called alternating on a specific lock. However, the problem is not obvious. Firstly, one has to know that whenever the program execution enters the function ata_scsi_queuecmd(), a lock on shost->host_lock is held. In an unlikely case the if-statement in line 1574 of libata-scsi.c will evaluate to true and line 1576:done(cmd); will be executed. This done() is a function pointer pointing to scsi_finish_command() (drivers/scsi/scsi.c), which will call 876:scsi_device_unbusy(). In line 447 of drivers/scsi/scsi_lib.c we see that this function will again lock shost->host_lock. Deadlock.

In order to find this bug using BLAST, simplifications needed to be applied to libata-scsi.c. We simplified several data structures, removed the use of function pointers and put all functions required into one C source file. The verification was then done using the temporal safety specification as given in the paper.

However, it was much more difficult to prove the patched version of the code to be free of this deadlock. Since it involves pointers to two different spinlocks; and pointers are not reasonably tracked by BLAST, we had to rewrite parts of the spinlock-API and used two global integer variables to represent the state of each lock.


Jan Tobias Mühlberg, $Date$