Verifying a toy driver with SATABS

Prior to Linux 2.2, Linux driver needed to maintain a usecount for the devices they manage. As soon as a device driver is loaded, the corresponding device can be accessed through a special file in the file system, typically located in the /dev directory. The device driver must not be unloaded (or unregistered, in kernel speak) unless nobody is accessing the device anymore.

Testing such a driver typically involves writing a test harness that simulates the behaviour of the program that calls the driver's open, read, write and release functions. However, if you develop a Linux device driver you have typically no control over how the API you provide will be used by clients. Therefore, as many combinations of calls to the driver as possible should be considered in your test cases.

SATABS provides a technique that is more powerful than traditional unit testing. By introducing non-determinism into your test harness, you can exhaustively test all combinations of calls to your driver. The family of nondet functions tells SATABS to consider all possible elements of a type. assume can be used to discard execution traces you are not interested in:

  do
    {
      random = nondet_uchar ();
      assume (0 <= random && random <= 3);

      switch (random)
	{
	case 1: 
	  rval = mydriver_open (&inode, &my_file);
	  if (rval == 0)
	    lock_held = TRUE;
	  break;
	case 2:
	  assume (lock_held);
	  count = mydriver_read (&my_file, buffer, BUF_SIZE); 
	  break;
	case 3:
	  mydriver_release (&inode, &my_file);
	  lock_held = FALSE;
	  break;
	default:
	  break;
	}
    }
  while (random || lock_held);
	

When SATABS analyzes the loop given in the code snipped above, it will consider all sequential combinations of calls to the driver API functions. In our example (see spec.c, this loop is followed by a call to unregisger_chrdev. This call contains an assertion that the usecount should be zero.

SATABS will automatically infer that there is a bug in mydriver_open. The reference count is increased upon entry of the function, but is not released if mydriver_open fails (because some other process has already locked the device). Note that this bug only emerges if the device is opened twice without being released in between.

	
  int mydriver_open (struct inode *inode, struct file *filp)
  {
    assert (MAJOR (inode->i_rdev) == dummy_major);
    MOD_INC_USE_COUNT;

    if (locked)
      return -1;
    locked = TRUE;
 
    return 0; /* success */
  }

This bug might have gone unnoticed by traditional unit testing (unless the test engineer, following his intuition, had specified a test-case that tests exactly this very sequence of calls to the driver API).

A more detailed description of this example is given in our SATABS user manual.

Example: Reference Counting in a Linux Driver

Requirements

Instructions