How tracking Byzantine bugs in the Linux kernel led
to a new way of thinking about complex software.

1. Background

Our goal is to transform software engineering from its currently manual, highly labor-intensive form to something highly automated, yet human directed. We seek to relieve engineers of tedious tasks by implementing automation and thereby allowing a person to focus on what is really relevant and inspiring: human insight and creativity.

Human ingenuity has carried us a long way from the days of punch cards, and today we appreciate tools like Eclipse that greatly streamline our ability to write software. But how do we make the next jump? How do we fast forward to the mass production of software? Some say we are already there, but we disagree—the journey is just beginning. Currently, there are vast volumes of software, but they are constructed in the same painstaking way the Egyptians built the pyramids, stone by stone. The Egyptians were equipped with the proper technology that made such large structures possible, but like us, the scale with which they could build was limited by sheer human labor.

Our first glimpse into the future came in the year 2000 when we created ParAgent, a tool that vastly sped-up the process of porting of a half-million line weather modeling code from a single processor to a cluster super-computer. By reducing the manual labor component of the task, the original effort which took 3-man years to complete was replicated by a single person in only 2-weeks - a speed-up of over 75 times [1].

ParAgent should be viewed not as a singular success, but as the first step in our journey to realizing the future potential of software automation. We asked ourselves: what principles can we learn from this accomplishment? In what other areas can this be applied? These are the questions we have been working to answer at the Knowledge-Centric Software Laboratory at Iowa State University.

In this paper we present our work with the Linux kernel as a unique expedition that seeks to transform software engineering. Our journey starts with an engineer trying to track down a Byzantine Linux kernel bug, and then we move on to the ambitious goal of verifying synchronization in the Linux kernel. Both stories give us simple yet profound insight into how we may approach software in the not-too-distant future.

2. Tracking a Byzantine Linux Kernel Bug

Our journey begins with Srinivas Neginhal, an engineer at a major network equipment manufacturer who is trying to track down a Byzantine Linux kernel bug through network-stack code, past pointer dereferences, and between threads - a hard job indeed. Even though Srinivas was used to tracking bugs, his frustration was ever-present as most of the bugs were discovered only after the equipment was deployed to the customer. The word Byzantine is the most appropriate term as it describes the complex interactions that characterize these bugs—interactions that are not easily reproduced and a challenge to untangle.

Convinced there was a more efficient way to track these bugs, Srinivas used his dissatisfaction with traditional methodologies as motivation to discover a better way. He felt like an expert navigator with merely a compass and a map, picking through the code one path at a time, when what he desperately wanted was a GPS - a way to consider many routes at once. The first step was to understand how these bugs were tracked manually, and then attempt to speed up the process through automation.

To illustrate the process, Srinivas chose to track the trajectory of a packet through the Intel PRO/1000 gigabit ethernet driver. In the Linux kernel this driver is named e1000 and consists of 284 functions in 21,032 lines of code. It quickly became evident that tracking a packet in the code involves primarily reading code, not writing it. This meant that speeding up the process would entail automating the reading of code, as opposed to writing.

Arthur and Pigoski tell us that up to 90% of time in maintaining software is spent reading (i.e. comprehending) software [2, 3]. Now, imagine building a pyramid: the first stones are easily maneuvered to form the base, but as it gains height, more and more time and effort go into lifting the heavy stones to the top of the emerging structure. Likewise, a large mature software system requires more and more time devoted to the reading of code.

You can think of tracking a packet from one end of the e1000 driver to the other like traveling from New York to Los Angeles. Although we cannot memorize every possible route between New York and Los Angeles, general knowledge of geography allows us to make educated predictions: a route from New York to Los Angeles must exist, and weʼll probably picture a map with highways running East to West; however, we cannot possibly conceive every possible route. Similarly, our process of reading of code is informed by a mental model and constrained by the limited amount of information our brains can juggle. Letʼs begin by refreshing our memory with a mental model of how a network driver works.

1. Mental Model for a Network Driver

Typically, a network device interrupts the processor upon receiving a packet. The device interrupt handler receives the packet and puts it into a receive queue. Subsequently, in a different thread of execution, the kernel dequeues the packet and processes it. Based on the packet type, the kernel directs the packet to the appropriate protocol handler. Runtime bindings, achieved through function pointers, provide for efficient and modular implementation of the protocol stack. [4]

2. How the e1000 driver processes an incoming packet

This mental model serves as a guide to determine which functions out of the 284 possibilities are relevant for the task at hand. We know from our mental model to start by looking for the place where packets are received from the network, and that the place is likely to be an interrupt. We can guess from the naming convention that e1000_intr() is the interrupt handler for the e1000 driver, so we start there. If we look at e1000_intr() we find that it calls __netif_rx_schedule(). __netif_rx_schedule() puts the net device structure on a per-CPU poll list in the softnet_data data structure and schedules the execution of the NET_RX_SOFTIRQ softirq. We are now at the second stage of our mental model.

The next step is to find where the packet is taken out of the poll list and processed. We specifically look for the code where the poll_list member variable of the softnet_data data structure is passed to list manipulation functions. After some searching and reading, we find that this happens in net_rx_action() which calls the function pointer dev->poll. We must figure out which function dev->poll points to. We find that e1000_probe() initializes dev->poll to e1000_clean().

e1000_clean() calls e1000_clean_rx_irq_ps(), which takes the packets that have been waiting in a buffer called the rx ring and constructs sk_buff objects - the third stage of our mental model. These sk_buff objects are passed to netif_receive_skb() which then routes it to the additional layers in the network stack.

3. Interactive Approach to Semi-automatic Reading of Code

As we read through the code we piece together clues, and we use these clues along with our mental model to ask questions about the code. Then we read further to answer these questions. Srinivas, working with Suraj Kothari, built CVision to automate part of this process. CVision is an interactive tool that allows the user to: quickly get to the relevant parts of the code, graphically visualize relationships between program elements, and interactively apply different graph reductions to eliminate irrelevant relationships [4]. Letʼs take a look at a few examples.

1. Example 1

We know from the mental model that e1000_intr() must place packets on a queue for later handling. If you have worked with the Linux kernel, you also know that queues and other lists are manipulated by functions declared in list.h. What if we could ask, “What relationship does e1000_intr() have to functions declared in list.h”? The graph below is the answer.

mod_timer() is suspicious since the name suggests it is not involved in moving packets, a quick inspection of the function confirms this. We can refine the answer by excluding relationships that are reached from mod_timer.

This is a strong suggestion we should look at __netif_rx_schedule() more closely.

As expected, we see in the highlighted text that the device poll_list is added to softnet_data.poll_list. A complete walkthrough of the e1000 driver is detailed in section 5.2 of [4]

2. Example 2

In the previous example the relationships of interest were very close to each other. Letʼs look at another example from the Linux kernel where relationships are far away and may be unexpected, this time outside of networking.

Does dynamic allocation of memory via kmalloc() have anything to do with the file system? Pause for a second — you should be able to guess the answer from your own domain knowledge of modern operating systems.

The answer is “Yes!” When there is no physical memory available, the kernel must use virtual memory, which may in turn reside in a file. In Figure 6, kmalloc() and the functions it can reach in the file system are highlighted.

3. Verifying Synchronization in the Linux Kernel

In section 2 we explored how to narrow down the code within the e1000 driver to only the functions and data structures necessary to understand the trajectory of a packet through the driver. We took an iterative approach, where a tool sped-up the reading of code by allowing the user to ask questions about functions and their relationships. In this section we explore our attempt to adapt the techniques developed with Srinivas to sift through the Linux kernel for interesting software artifacts en masse.

In other fields of science the progression from manual use of tools towards automatic processing and surveying of large volumes of data is commonplace. In 1609 Galileo Galilei pointed his telescope to the skies and for the next two centuries astronomers sketched their observations by hand. But when John William Draper took a photograph of the moon in 1840, it spurred a new era of astronomical discovery, and in 1958 the Palomar Observatory Sky Survey was completed, photographing the entire northern sky using almost 2000 photographic plates [hc17, hc21].

Today, design of the Large Synoptic Survey Telescope is underway. Scheduled to start operating in 2015, it will use a 3.2-gigapixel camera to photograph the entire night sky every week [16]. The project will generate 60 petabytes of data that must be sifted through by a computer to pinpoint interesting stellar events [17]. Like the Large Synoptic Survey Telescope, our approach is to bring the interesting portions of source code to the attention of engineers who will use their insight and other tools and techniques to probe these in more detail.

We chose matching pair properties as the first interesting software artifacts to survey. Specifically, we wanted to verify that the uses of mutex_lock()¹ and mutex_unlock() in the Linux kernel are correct. In the sections below we provide a formal definition of matching pair properties and describe our approach to sifting through the mammoth 1,081,090 lines of code and 39,973 functions in the Linux kernel (version 2.6.31).

¹ mutex_trylock() and mutex_lock_interruptible() may also be used acquire a lock and were considered. We focus on mutex_lock() and mutex_unlock() in the text to keep explanations concise.

However, in the case of synchronization our ambitious goal is to find bugs before they happen in the field.

1. Synchronization and The Matching Pair Property

Synchronization in the Linux kernel is a special case of a matching pair property [6]. Examples of matching pair properties are:

• Synchronization: lock and unlock
• File access: open and close
• Memory management: allocate and free

What all matching pair properties have in common are two “opposite” events that operate on an instance of a token. We use the following general formulation of the MP property: on any execution path, the identifier used by a call to P(X) must flow into and be used by exactly one call to V(X), where P and V are problem-specific events in the software, and X is a token they share. Table 2 shows two examples of P, V, and X.

Synchronization in the Linux kernel is achieved by matching calls to mutex_lock() and mutex_unlock() for a given mutex.

In Figure 8 we see four call graphs with increasingly complex matching pair properties.

(a) A simple instance of where P(X) and V(X) are invoked within the same function a1.

(b) A more complex case with intermediate functions between b1 and P(X) and V(X).

(c) A given execution may result in P(X) and V(X) being called from different non-trivial paths through the code.

(d) Ordinarily, control flow is visible through control structures and call sequences. However the matching calls to P(X) and V(X) in this example are made in different threads.

The examples in Figure 8(b,c,d) illustrate that to verify correct behavior of a matching pair property it is not sufficient to just examine the functions that call P(X) and V(X). It is also important to understand how these functions are related to each other via other functions. For example in Figure 8(b), b1 is necessary to tie the token acquired in b2 via P(X) to its release in b3 via V(X). When a concern or behavior is distributed in different parts of code we refer to it as cross-cutting [12].

2. Past Efforts

Our goal is to verify that the uses of mutex_lock() and mutex_unlock() in the Linux kernel are correct in an effort to find synchronization bugs before they happen. Finding bugs before they happen is certainly not new, however, there are serious limitations to a computer-only approach to the problem.

Many tools [7, 8, 9, 10, 11] can perform fast intra-procedural static analysis. However, the algorithmic complexity of a context-sensitive static analysis solution grows exponentially [13, 14], making it unsuitable for large-scale inter-procedural analysis of cross-cutting instances of matching pair properties. A detailed discussion can be found in section 2 of [5].

3. Our Approach

So how do we verify behavior for synchronization and other similar cross-cutting aspects in software as large as the Linux kernel? The astronomers working on the Large Synoptic Survey Telescope are not interested in everything in the sky; rather, they will use computers to identify a subset of celestial events that are of interest. Likewise, only a small subset of the code needs to be examined to verify synchronization and other cross-cutting behaviors. However, as we said in section 3.1 it is not enough to focus only on the functions that call mutex_lock() and mutex_unlock(), it is also necessary to examine the functions that connect them.

Like Srinivas, we want to identify what portions of code are relevant to the problem at hand. However, instead of having a human use a tool interactively for each bug, we wanted to narrow down the code significantly en masse. The result should be the code relevant to each instance of a matching pair property. Then, like astronomers looking at individual star clusters, we can use human insight and other techniques to understand the relevant subsets of code.

Astronomers use mathematics to understand the heavens. We also use mathematics to understand software. Specifically, we use graphs to create formulas and algorithms to filter out code. The particular formula we present here is called MPG(X) and is described below [5]. Like other products of mathematics, MPG(X) has broad applicability. It can be applied to any matching pair property on many different pieces of software, not just synchronization in the Linux kernel. In the following sections we describe the MPG(X) in more detail and present our results so far.

4. Matching Pair Graph of a token X

MPG(X) is the set of functions that must be examined to verify an instance of a matching pair property [5]. In the case of synchronization in the Linux kernel P(X) corresponds to mutex_lock(), P(V) corresponds to mutex_unlock(), and X is a pointer to a mutex.

The four criteria below give us a good intuitive understanding of MPG(X) (a formal definition is found in [5]). A function is in the MPG(X) for a given token X if any of these is true:

• A function is in MPG(X) if only P(X) or V(X) can be reached from it, but not both P(X) and V(X). This function is said to be unbalanced.
• A function that calls one or more unbalanced functions directly.
• If a functional calls both P(X) and V(X) directly.
• For functions a and b which are members of the MPG(X), where a reaches b through the call graph. Functions in the path from a to b are also in the MPG(X)

A function is said to be balanced if both P(X) and V(X) can be reached from it. Not all balanced functions are part of an MPG(X), but we will refer to this idea later.

For example, in Figure 10(v), v1 and v2 are part of the MPG(X) since they only call P(X) and V(X) respectively, but not both. v1 and v2 are said to be unbalanced. v3 is part of MPG(X) because if calls v1 and v2, which are unbalanced. Finally, v4 is not part of the MPG(X) since v3 is not unbalanced.

5. Is an MPG(X) necessary or sufficient?

The MPG(X) contains only functions that must be examined to verify an instance of a matching pair property. Naturally the question arises, “Is this set of functions necessary, or sufficient?” The MPG(X) is always necessary since we must examine how the token X acquired by P(X) is eventually released by V(X). The functions in the MPG(X) contain the control path that ties these two events together.

However, the exact path taken may be influenced by conditions based on values set outside of the functions in the MPG(X). However not all conditions will affect a particular instance of a matching pair property. For example conditions related to sorting a list should not affect the lock on the list. The challenge is to efficiently examine the paths that do. Section 4 in [5] describes a method to minimize the number of paths to be examined and proposes an easy-to-examine table format which presents these paths.

For brevity and focus this method is not detailed here, but follows the same spirit: automate reading and focus human attention on as specific information as possible.

4. Results and Next Steps

Our experiment was conducted on the Linux kernel version 2.6.31. Our build of the kernel contains 1,081,090 lines of code and 39,973 functions. To date we have computed the MPG(X)ʼes for mutex_lock() and mutex_unlock(), detailed below. MPG(X) for a given mutex X is computed as a series of Atlas queries. A formal definition of MPG(X) and the algorithm to compute it with Atlas is found in [5].

1. Detailed Results

We computed MPG(X) for mutexes in global variables and in structures that were referenced via pointers. For mutexes in these structures we treated any access to a mutex from a structure of a given type as if it was the same mutex. This simplification works in most cases since a function or set of functions is generally called on one instance of the structure at a time.

This partitioning of uses of mutex_lock() and mutex_unlock() by global variables and structure types results in 249 MPG(X)ʼes that need to be computed. Table 3 summarizes the distribution of sizes of the MPG(X)ʼes computed. The size of MPG(X) is small in the majority of cases, less than five in nearly 75% them. The size is bigger than 50 in only three instances.

In addition, the structure of each MPG(X) tends to be simple. For example the MPG(block_device.bd_mutex) in Figure 11 is very shallow and most functions are like the simple case (a) in Figure 11.

Our process so far has drastically reduced the amount of code that will need to be reviewed in order to verify uses of mutex_lock() and mutex_unlock() in the Linux kernel. It has also made this work trivially parallelizable Each MPG(X) can be reviewed independently of the other without concern that they are missing some vital information.

2. Next Steps

The most significant next step is to verify each MPG(X) for mutex_lock() and mutex_unlock(). The method in Section 4 in [5] will be used for this task.

After the initial verification we plan to use the MPG(X) to intelligently perform an incremental verification. For example, a first pass can automatically check for which mutexes the MPG(X) has stayed the same. If the code for these has also stayed the same they need not be verified again.

A similar verification can be done for memory leaks in the Linux kernel. In this case P(X), V(X), and X would be kmalloc(), kfree(), and a pointers to memory.

MPG(X) can also be used for precise estimation of verification efforts since metrics can be developed around the subset of code that actually needs to examined.

5. Closing Thoughts

Whether one is trying to get from NY to LA or taking pictures of the universe or maintaining software code, the interpretation of large data sets is a constant struggle for the human mind. In this paper we have provided the first glimpse of a new software analysis methodology that focuses on reading code rather than writing it. Codifying how code is read into a machine-repeatable process through the use of graph representations of code is a powerful technique that vastly speeds up software engineering tasks. Furthermore, we demonstrated how general formulas and algorithms can be developed for software engineering tasks that pave the way for the automation of software engineering tasks at an unprecedented scale.

We believe in a future where reliable code is ubiquitous and engineers are able to use their time, energy and focus on being innovative. You can begin moving towards this future today. When you work on a piece of code ask yourself:

• How much time do I spend reading rather than writing?
• What relationships am I looking for when reading code?
• Do I take a similar approach to a class of problems?
• Could this approach be codified and applied to any problem of this type?

These are the questions that emerged from our journey. We believe answers to these questions will pave the way for future developments. We would love to hear your answers to these questions. Please contact Jeremias Sauceda with your insights at pi@ensoftcorp.com.

Acknowledgments

We thank Srinivas Neginhal and Kang Gui for their work related to the Linux kernel. We also thank Jon Mathews from EnSoft Corp., for his work on Atlas, the tool used to calculate the results in section 4.