News, tips, partners, and perspectives for the Oracle Linux operating system and upstream Linux kernel work

Writing the Ultimate Locking Check

Scott Michael
Director, Software Development

In this blog post, Oracle Linux kernel developer Dan Carpenter discusses a recent improvement that he made to his static analyzer Smatch to look for locking errors.


One common type of bug is when programmers forget to unlock on an error path and it leads to a system hang later when the kernel tries to re-take the lock. These kinds of bugs hard to catch in testing because they happen on the failure paths but they're ideally suited for static analysis. Static analysis tools look at the source code to find bugs instead of doing it through testing. I wrote a static analysis tool called Smatch and the website for it is here: https://github.com/error27/smatch

In theory a clever programmer could discover all the bugs in a piece of software just by examining it carefully, but in reality humans can't keep track of everything and they get distracted easily. A computer could use the same logic and find the bugs through static analysis. There are two main limitations for static analysis. The first is that it is hard to know the difference between a bug and feature. Here we're going to specify that holding a lock for certain returns is a bug. This rule is generally is true but occasionally the kernel programmers hold a lock deliberately. The second limitation is that to understand the code, sometimes you need to understand how the variables are related to each other. It's difficult to know in advance which variables are related and it's impossible to track all the relationships without running out of memory. This will become more clear later. Nevertheless, static analysis can find many bugs so it is a useful tool.

Many static analysis tools have a check for locking bugs. Smatch has had one since 2002 but it wasn't exceptional. My first ten patches in the Linux kernel git history fixed locking bugs and I have written hundreds of these fixes in the years since. When Smatch gained the ability to do cross function analysis in 2010, I knew that I had to re-write the locking check to take advantage of the new cross function analysis feature. When you combine cross function analysis with top of the line flow analysis available and in depth knowledge of kernel locks then the result is the Ultimate Locking Check! Unfortunately, I have a tendency towards procrastination and it took me a decade to get around to it, but it is done now. This blog will step through how the locking analysis works.

Locking Functions

The kernel uses the __acquires() and __releases() annotations to mark the locking functions. Smatch ignores these. Partly it is for legacy reasons but it's also because the locking annotations are a bit clumsy. Not all locks are annotated so it was never going to be a complete solution. The annotations serve as a sort of cross function markup, but since Smatch can do cross function analysis directly they aren't required. Instead Smatch has a table which describes the locking functions.

The locking table has around 300 entries which look like this:

    {"down_write_trylock",        LOCK,   write_lock, 0, ret_one},
    {"down_write_killable",       LOCK,   write_lock, 0, ret_zero},
    {"write_unlock",              UNLOCK, write_lock, 0, ret_any},

The fields are mostly self explanatory. The type was originally supposed to be used to warn about places that call schedule() while holding a spin_lock. Currently, it's only used to warn about nesting calls where some type of locks are allow to be nested, like bottom half locks, and some like spin_lock_irq() are not. The "0" means that the first (zeroeth) argument to down_write_trylock(&my_lock) is the lock variable. The "ret_one" means if down_write_trylock(&my_lock) returns one the lock is acquired but "ret_zero" for down_write_killable(&my_lock) a zero return means the lock is acquired.

Loading the Locking Table Information

The lock table is loaded into the function hooks:

    if (lock->return_type == ret_zero) {
        return_implies_state(lock->function, 0, 0, &match_lock_held, idx);
        return_implies_state(lock->function, -4095, -1, &match_lock_failed, idx);

In this code sample, "lock->function" is down_write_killable(). The next two parameters are a range of possible returns. The "0, 0" range means the lock is held. The "-4095, -1" represents the range of normal error codes in the kernel and these returns means that we weren't able to take the lock. This works for almost everything except for one caller which does this:

    if (mutex_lock_interruptible(&my_lock) == -EINTR)

Here only the -EINTR error code is handled. When we build the cross function database, Smatch thinks mutex_lock_interruptible() can return either -EINTR or -EALREADY. So when Smatch parses this code it prints a warning that the -EALREADY return wasn't handled correctly:

drivers/scsi/foo.c:1374 reset_fn() error: double unlocked '&my_lock' (orig line 1369)

The work around for this is to add a line in smatch_data/db/kernel.return_fixes

mutex_lock_interruptible (-35),(-4) (-4)

After the database is rebuilt, the .return_fixes file is used to update the database and changes the return from "(-35),(-4)" to "(-4)".

Going back to the function hooks code, the final two arguments are a pointer to the match_lock_held() function which takes "idx" as an argument. The simplified code for match_lock_held() looks like this:

static void do_lock(const char *name, struct symbol *sym)
    struct sm_state *sm;

    add_tracker(&locks, my_id, name, sym);
    sm = get_sm_state(my_id, name, sym);
    if (!sm)
        set_start_state(name, sym, &unlocked);
    warn_on_double(sm, &locked);
    set_state(my_id, name, sym, &locked);

static void match_lock_held(const char *fn, struct expression *call_expr,
                            struct expression *assign_expr, void *_index)
    int index = PTR_INT(_index);
    char *name;
    struct symbol *sym;

    name = get_full_name(call_expr, index, &sym);
    do_lock(name, sym);

The name is "my_lock". The add_tracker() function keeps a list of locks we have touched in this function. If this is the first time we have seen "my_lock" then we record that "my_lock" started as unlocked. The warn_on_double() function prints a warning if it was already locked. And finally, we set the state of "my_lock" to &locked.

States, SM States, and Strees

There are three important struct types to understand this code: smatch_state, sm_state and stree. The smatch_states in this function are &locked and &unlocked. The states are declared at the start of the check_locking.c file.


There are two additional global smatch_states that which are &undefined and &merged.

The sm_state struct links a variable to a smatch_state.

struct sm_state {
        const char *name;  // <<-- variable ("my_lock")
        struct symbol *sym;
        unsigned short owner;  // <-- check_locking.c
        unsigned short merged:1;
        unsigned int line;
        struct smatch_state *state;  // <<-- state ("&locked")
        struct stree *pool; // <-- where this state was created
        struct sm_state *left;
        struct sm_state *right;
        struct state_list *possible;  // <-- possible states ("&locked")

In this case, the variable is "my_lock" and the smatch_state is &locked. If the smatch_state is &merged then we could look at the list of sm->possible states to see if "my_lock" is ever &locked/&unlocked at this point. The sm_state struct also has a pointer to the stree where the sm_state was created. Finally, it has left and right pointers which point to previous sm_states and previous strees if smatch_state is &merged.

A stree is a group of sm_states. The name comes from "states" which are stored in a "tree". The "cur_stree" is the current set of all the sm_states that Smatch is tracking. The sm_state has the "owner" field so that we can identify the locking states out of the "cur_stree" and ignore the other checks.

In programming languages we have branches and merges:

    if (something) { // <-- branch
    } // <-- merge

When a merge happens, the strees from both side are frozen and preserved until the end of the function and a new merged stree is created. We saw earlier that each sm_state has links to previous strees. These links let us manipulate strees in useful ways. We can ask "assume mutex_lock_interruptible() returned -5", then Smatch looks through the history and returns the stree based on that assumption. The code for this is in smatch_implied.c. In that returned stree "my_lock" would be &unlocked. In this way, the stree represents connection between states and the relationship between the return value and the locked state.

Printing Warning Messages

To get back to the locking check, after a function has been parsed we look at all the locks from add_tracker(). For each lock, if it is held on some success paths but not others, or if it is held on an error path but not on the success path then print a warning message. We can ignore cases where the lock is always held on the success path because those will be always caught in testing.

The simplified code to implement that looks like:

static void check_lock(char *name, struct symbol *sym)
    int locked_buckets[NUM_RETURN_BUCKETS] = {};
    int unlocked_buckets[NUM_RETURN_BUCKETS] = {};
    struct smatch_state *state, *return_state;
    struct stree *stree, *orig;
    int bucket;

    FOR_EACH_PTR(get_all_return_strees(), stree) {
        orig = __swap_cur_stree(stree);

        return_state = get_state(RETURN_ID, "return_ranges", NULL);
        state = get_state(my_id, name, sym);
        if (!return_state || !state)
            goto swap_stree;
        if (state != &locked && state != &unlocked)
            goto swap_stree;

        bucket = success_fail_positive(estate_rl(return_state));
        if (state == &locked)
            locked_buckets[bucket] = true;
            unlocked_buckets[bucket] = true;
    } END_FOR_EACH_PTR(stree);

    if (locked_buckets[SUCCESS] && unlocked_buckets[SUCCESS])
        goto complain;
    if (locked_buckets[FAIL] && unlocked_buckets[SUCCESS]))
        goto complain;
    if (locked_buckets[ERR_PTR])
        goto complain;

    sm_msg("warn: inconsistent returns '%s'", name);

static void match_func_end(struct symbol *sym)
    struct tracker *tracker;

    FOR_EACH_PTR(locks, tracker) {
        check_lock(tracker->name, tracker->sym);
    } END_FOR_EACH_PTR(tracker);

One new feature introduced in these functions is "estate_rl(return_state)". An "estate" is a "smatch extra" state. The "extra" naming seems silly now because smatch_extra.c is the core feature of Smatch. The smatch_extra.c module tracks all the possible values of the variables used in a function. The "rl" in estate_rl() stands for struct range_list which is how Smatch represents a range of numbers like "(-35),(-4),0-1". This "estate_rl(return_state)" code is looking at the returned values to decide if it is an error path or a success path.

The Cross Function Database

When a function is called, we record information from the current stree in the caller_info table. Each call becomes a single stree in the called function. Unfortunately that means that the relationships between variables and links to previous strees are lost. For example, sometimes developers will write code like:

    if (pointer && !size_from_user_is_valid(size))
        return -EINVAL;

    some_function(pointer, size);

For the programmer, it's obvious that if "pointer" is NULL then we do not care about the size. But when Smatch records this in the database the relationship is lost and the call is flattened to a single stree. Smatch only knows that pointer can be NULL or non-NULL and that the size has not necessarily been checked. What I'm saying is don't write code like that. Always check the sizes from the user even when the pointer is not used. Do this:

    if (!size_from_user_is_valid(size))
        return -EINVAL;

    some_function(pointer, size);

Similarly, each return is represented in the cross function database as a stree. Actually, returns are more complicated because often we need to split a single return into multiple strees. For example, if we are parsing code like this:

    ret = 0;
    return ret;

The example code uses one return statement but Smatch would probably try split it up into success vs failure path. There are around ten different approaches or heuristics that Smatch uses to split returns into meaningful strees. Sometimes there are too many states and the return cannot be split. We need to parse the return information quickly so there are hard limits on how much data we can record in the database.

Storing Information in the Cross Function Database

The first step to store locking information in the cross function database is to add some new enum info_type types to smatch.h

    LOCKED      = 8020,
    UNLOCKED    = 8021,
    LOCK_RESTORED   = 9023,

The numbers are the type used in the database. They don't mean anything. They are out of order because I didn't realized until later that LOCK_RESTORED was required. LOCK_RESTORED is for irqrestore because restoring is not necessarily the same as enabling the IRQs.

The Smatch database has a number of different tables but the lock check only uses the return_states table. The code to insert data into return_states looks like this:

static void match_return_info(int return_id, char *return_ranges, struct expression *expr)
    struct sm_state *sm;
    const char *param_name;
    int param;

    FOR_EACH_MY_SM(my_id, __get_cur_stree(), sm) {
        if (sm->state != &locked &&
            sm->state != &unlocked &&
            sm->state != &restore)

        if (sm->state == get_start_state(sm)

        param = get_param_lock_name(sm, expr, ¶m_name);
        sql_insert_return_states(return_id, return_ranges,
                     param, param_name, "");
    } END_FOR_EACH_SM(sm);

The "return_id" is a unique ID and "return_ranges" is a string like "(-4095)-(-1)". The "expr" is returned value. This function iterates through all the locks and if they have changed then it records that in the return_states table. The get_db_type() function returns LOCKED or UNLOCKED that we added to info_type. If the function returns a struct holding the lock then param is -1, otherwise it's the parameter which holds the lock. The param_name is going to be something like "$->lock" where the dollar sign is a wild card because the callers might call the parameter different names.

Reading from the Database

That's how we insert locking information into return_states and the code to select it looks like this:

static void db_param_locked_unlocked(struct expression *expr, int param, char *key, char *value, enum action lock_unlock)
    struct expression *call, *arg;
    char *name;
    struct symbol *sym;

    call = expr;
    while (call->type == EXPR_ASSIGNMENT)
        call = strip_expr(call->right);
    if (call->type != EXPR_CALL)

    if (func_in_lock_table(call->fn))

    if (param == -1) {
        if (expr->type != EXPR_ASSIGNMENT)
        name = get_variable_from_key(expr->left, key, &sym);
    } else {
        arg = get_argument_from_call_expr(call->args, param);
        if (!arg)

        name = get_variable_from_key(arg, key, &sym);
    if (!name || !sym)
        goto free;

    if (lock_unlock == LOCK)
        do_lock(name, sym);
    else if (lock_unlock == UNLOCK)
        do_unlock(name, sym);
    else if (lock_unlock == RESTORE)
        do_restore(name, sym);

In this code "expr" can either be an assignment like "ret = spin_trylock(&my_lock);" or it can be a function call like "spin_lock(&my_lock);". The "param" variable is the parameter that is locked. If param is -1 that means the returned pointer is locked.

The other thing to note is the check:

    if (func_in_lock_table(call->fn))

Functions such as spin_lock_irq() are in both the database and the function table so they were counted as two locks in a row and triggered a double lock warning. This check means we ignore information from the database when we have the locking information in both places.

In an ideal world this would be the end of the story. But it is only the beginning.

Guess work

The first problem is that there are some functions where it's hard to tie the lock to a specific parameter. Perhaps the lock is a global variable, or the parameter might be a key and we have to look up the lock in a hash table. Or maybe we have two pointers which point to the same lock. The work around for this is that if the caller cannot tie a lock to a parameter, then it returns that the parameter is -2. In the caller, if the parameter is -2 or it otherwise fails to match an unlock to a lock then it uses the get_best_match() function to find the correct lock. The get_best_match() function looks takes a lock name such as "$->foo->bar->baz" and tries to find a known lock which ends with "->bar->baz".

Bugs in Smatch

Another early problem that I faced was parsing code like:

    18  void snd_gf1_mem_lock(struct snd_gf1_mem * alloc, int xup)
    19  {
    20          if (!xup) {
    21                  mutex_lock(&alloc->memory_mutex);
    22          } else {
    23                  mutex_unlock(&alloc->memory_mutex);
    24          }
    25  }

This function locks or unlocks depending on the "xup" parameter. These type of locking functions are normally small so Smatch parses them inline. This raised a problem because if you have a literal zero, Smatch treats it as known, but if you have a variable set to zero Smatch treats it as only "sort of known". The caller is passing literal values to this function but they are assigned to "xup" and downgraded to only sort of known. I made known inline parameters a special case where the "sort of known" values get promoted to "all the way known".

I ran into a number of other general bugs in Smatch. Here is an example of some code that was hard to parse. I have snipped away the irrelevant lines.

   108          for (i = 0; i < sas_ha->num_phys; i++) {
   109                  port = sas_ha->sas_port[i];
   110                  spin_lock(&port->phy_list_lock);
   111                  if (...) {

   116                          break;
   117                  }
   118                  spin_unlock(&port->phy_list_lock);
   119          }
   121          if (i == sas_ha->num_phys) {

   133          }
   135          if (i >= sas_ha->num_phys) {

   138                  return;
   139          }

The problem is that Smatch isn't sure if we are holding the "port->phy_list_lock" when we return on line 138. The Smatch subsystem to handle comparisons where the values of the variables are unknown is smatch_comparison.c. It was not preserving the links to previous strees correctly and the "i == sas_has->num_phys" comparison over wrote the links to the previous strees from the for loop.

I also discovered a bug in Smatch flow analysis where if we were in unreachable code and encountered a switch statement then the code was marked reachable again. That resulted in a bug where Smatch recorded that a return unlocked but really that return was unreachable.

A different bug was that Smatch did not handle conditional returns correctly when the conditional was a function.

    return foo() ?: ({ spin_lock(&my_lock; 0; });

This style of return worked where the condition was a variable but not when it was a function. I had to create an module called smatch_parsed_conditions.c to handle this.

Work Arounds

There were other inlines that were tricky to handle:

   228  static inline void rw_lock(bool w, struct btree *b, int level)
   229  {
   230          w ? down_write_nested(&b->lock, level + 1)
   231            : down_read_nested(&b->lock, level + 1);
   232          if (w)
   233                  b->seq++;
   234  }

In this case, I just added rw_lock() and rl_unlock() to the locking table (as mentioned earlier the locking table trumps the database). It is not perfect solution and there are still a couple false positives related to rw_lock().

One function that was especially difficult was the dma_resv_lock() function. It returns zero on success or -EINTR on failure, however if the second argument is NULL then it can't fail. The dma_resv_lock() is called over a hundred times and generated a lot of false positives. I wrote a special return_implies hook to handle it:

static void match_dma_resv_lock_NULL(const char *fn, struct expression *call_expr,
                                     struct expression *assign_expr, void *_index)
        struct expression *lock, *ctx;
        char *lock_name;
        struct symbol *sym;

        lock = get_argument_from_call_expr(call_expr->args, 0);
        ctx = get_argument_from_call_expr(call_expr->args, 1);
        if (!expr_is_zero(ctx))

        lock_name = lock_to_name_sym(lock, &sym);
        if (!lock_name || !sym)
                goto free;
        do_lock(lock_name, sym, NULL);

It just tests if the "ctx" parameter is NULL and sets the state to &locked if it is. What happens is the standard code sets this to a merged locked and unlocked state and then this function immediately over writes it to say that it's locked. I considered other fixes such as marking the -EINTR path as impossible. Those approaches are valid but this seemed easiest.

One place where Smatch struggles is if the function calls a callback in a different thread. My solution was to create a file with manual locking annotations in smatch_data/db/kernel.insert.return_states These entries are inserted into the cross function database after it is rebuilt.

# The format to insert is:
# file (optional), function, "return values" | type, param, "key", "value"
mlx5_cmd_comp_handler, "" | 8021, -2, "*sem", ""
smc_connect_abort, "1-s32max[==$1]"                | 8021, -2, "smc_client_lgr_pending", ""
smc_connect_abort, "s32min-(-12),(-10)-(-1)[==$1]" | 8021, -2, "smc_client_lgr_pending", ""
smc_connect_abort, "1-s32max[==$1]"                | 8021, -2, "smc_server_lgr_pending", ""
smc_connect_abort, "s32min-(-12),(-10)-(-1)[==$1]" | 8021, -2, "smc_server_lgr_pending", ""
dlfb_submit_urb, "0" | 8021, 0, "$->urbs.limit_sem", ""

There are a few locking functions which are just strange.

   314  static unsigned long *ipmi_ssif_lock_cond(struct ssif_info *ssif_info,
   315                                            unsigned long *flags)
   316  {
   317          spin_lock_irqsave(&ssif_info->lock, *flags);
   318          return flags;
   319  }

Both the "flags" parameter and the returned "ret_flags" represent the saved IRQ flags, but the callers always use the returned values. The database only records that the flags are set in the parameter. To work around this problem I added a line to smatch_data/db/fixup_kernel.sh to change it to the returned value.

update return_states set parameter = -1, key = '\$' where function = 'ipmi_ssif_lock_cond' and type = 8020 and parameter = 1;

I had to add the "ipmi_ssif_lock_cond" function to the smatch_data/kernel.no_inline_functions file so that Smatch would use the modified information from the disk instead of parsing it inline. Inline functions use the same code as the on-disk database, but they work using an in-memory database. Parsing inline functions is normally transparent, but sometimes the in-memory database will return different, hopefully more accurate information than the on-disk database. Changes from smatch_data/db/kernel.return_fixes will be applied to the in memory database, but raw SQL commands from the smatch_data/db/fixup_kernel.sh only affect the on-disk database.

Finally, when all else failed I decided to just silence some warnings so I created a false positive table.

static const char *false_positives[][2] = {
        {"fs/jffs2/", "->alloc_sem"},
        {"fs/xfs/", "->b_sema"},

The Debugging Process

Writing a Smatch check is an iterative process. I started with a basic heuristic that forgetting to unlock on an error path should generate a warning. Then I tested my code. Then I tried to fix the issues one at a time.

There three main debugging methods I used. The first is to use the --debug=check_locking option which prints all the locking state transitions. The second option is to add "#include "/path/to/smatch/check_debug.h" to the parsed file and __smatch_sates("check_locking"); at the appropriate lines. Like this:

   710  #include "/home/dcarpenter/smatch/check_debug.h"
   711  void __init poking_init(void)
   712  {
   713          spinlock_t *ptl;
   714          pte_t *ptep;
   716          poking_mm = copy_init_mm();

[ snip ]

   737          ptep = get_locked_pte(poking_mm, poking_addr, &ptl);
   738          __smatch_states("check_locking");
   739          BUG_ON(!ptep);
   740          __smatch_states("check_locking");
   741          pte_unmap_unlock(ptep, ptl);
   742          __smatch_states("check_locking");

When I run Smatch it displays:

arch/x86/mm/init.c:738 poking_init() [check_locking] *ptl = 'merged' [merged] (locked, merged, start_state)
arch/x86/mm/init.c:740 poking_init() [check_locking] *ptl = 'locked' [merged]
arch/x86/mm/init.c:742 poking_init() [check_locking] *ptl = 'unlocked'

This output represents the correct fixed output after I had finished debugging the issue. The other key debugging tool is the local_debug flag. Include the check_debug.h as in the previous example, then add:

   736      __smatch_local_debug_on();
   737          ptep = get_locked_pte(poking_mm, poking_addr, &ptl);
   738      __smatch_local_debug_off();

Then add the appropriate debug printfs to the Smatch check:

    if (local_debug)
        sm_msg("expr = '%s' key = '%s'", expr_to_str(expr), key);

There is a fourth option to use __smatch_debug_on/off() which prints every state change for every single module but if you have to resort to that then you should probably just give up.

Future Work

There were a few problems which I wasn't able to fix. One is that Smatch doesn't handle call backs correctly:

    if (kref_put(&zhdr->refcount, release_z3fold_page_locked)) {

In this code release_z3fold_page_locked() unlocks zhdr->page_lock but Smatch does not see it. It should be possible for Smatch to parse kref_put() correctly but I have not implemented that code yet.

Another problem is that Smatch doesn't parse bitwise logic correctly like:

    if (test_bit(PAGE_HEADLESS, &page->private))


    if (test_bit(PAGE_HEADLESS, &page->private))

In this code Smatch doesn't know that the lock is always unlocked at the end.

Handling bitwise logic is not necessarily difficult to do but it is a lot of code to write so I haven't gotten around to it. I knew that this was a problem before but as I wrote this code I was able to silence around 90% of the false positives. As the false positives got fewer the perceived seriousness went from "Bitwise logic only causes a few false positives" to "This a major cause of the remaining false positives".

A second idea to silence that warning would be to mark test_bit() as a pure function which doesn't have side effects. With pure functions, if the parameters are the same, then the result is the same so we can pair the two conditions nicely. I believe that GCC does this sort of analysis.

The kernel uses assertions such as spin_is_locked(). It would be nice to add a warning to say if these tests can fail. Another potential use would be to print a warning when data structures are accessed without holding a lock. We would need some annotation to tie the lock to the data it protects.


Looking back, the original Smatch locking check makes me cringe. It was the first check I wrote and I made some design errors. I'm very happy with the new check. It is still new so there is likely to be the occasional embarrassing bug, but overall the approach is sound and the bugs can now be fixed one at a time without doing a another rewrite.

The original Smatch locking check generated 98 warnings about inconsistent locking. Kernel developers have fixed all the real bugs so all 98 warnings are false positives. The new check has 28 warnings all together. Around half of the new warnings look like real bugs. They are mostly minor bugs in old code and don't likely have a noticeable real life impact. However, this check will be used for many years to come and I expect it will lead to hundreds of bug fixes.

Join the discussion

Comments ( 1 )
  • Noel Grandin Monday, June 8, 2020
    Nice! This pretty much parallels my own path writing checkers based on clang for the LibreOffice code base.

    In the beginning I thought that I would need to write really really clever code, but it turns out fairly dumb code actually can find a lot of bugs :-)
Please enter your name.Please provide a valid email address.Please enter a comment.CAPTCHA challenge response provided was incorrect. Please try again.