Infer: Find Races and Deadlocks

In an almost evolutionary manner, programmers have learned to mostly avoid locks and shared mutable memory. Only when push comes to shove do we reach for these primitives. Unfortunately I found myself in need of some locks when writing a POPE Tree extension for Postgres. While building the prototype I wound up in lock hell. Lucky for me we have powerful tools that can help in these situations — this is my story of using Infer to get not-fired.

The POPE Tree (PDF) description is a tad academic; you don’t need to understand it to read on. This tree is populated lazily. Each node of the tree buffers data on insertion. Only the queries cause children nodes to be created and elements of the buffer to be binned into the nodes of the next layer. Want to allow high-throughput querying with parallel reads? Congratulations, the reads cause the tree to mutate and my prototype used locks… badly.

Fortunately that cryptographic structure was only half my day job. In the other half we were busy developing a way to make Facebook’s Infer static analyzer more accessible. Let’s look at what Infer is and how applying it played out.

Infer: What it is and what it is not

Facebook says:

Infer is a static analysis tool — if you give Infer some Java or C/C++/Objective-C code it produces a list of potential bugs.

What a great sentence. Infer finds bugs, or maybe bugs. You actually can’t just give it code — you have to tell it how to build the code. This is because Infer is no linter, it doesn’t just look at your code in a local context but considers how functions interact across compilation units (files, packages).

During analysis Infer assigns a sort of type signature to each function. The signatures describes the input/output impact the function has on the heap and acquired resources (allocation, locks, writes are all similar if you squint). If a caller doesn’t provide a suitably-shaped heap that the callee requires, well, that’s a bug.

On To Business: Using Infer on Toys

Enough banter, install infer and start doing things. First let’s download infer in a docker container.

docker run --rm -it tommd/infer bash

Second, let’s make a toy C file and tell infer how to build it.

cat <<EOF >toy.c
#include <stdlib.h>
int main() {
    int *ptr = malloc(sizeof(int));
    *ptr = 1;
    return *ptr;
}
EOF

Clearly correct. Now we let infer have a turn. No build system necessary, just a build instruction indicating gcc.

infer run -- gcc toy.c
Capturing in make/cc mode...
Found 1 source file to analyze in /infer-out

That simple. You tell infer the compilation commands and infer tells you the bugs it sees. What could be better? Well, a real project for starts. So let’s do that!

On to Business: Using Infer on Real Stuff

For this next step I’m going to dig up my old psql extension that hasn’t been open sourced. You can continue playing along at home using a C or Java project of your choosing. Consider zeromq or redis if you’re drawing a blank.

At this point I have a pretty typical Postgres extension. No surprises here, some files are included, a makefile exists, and with postgresql-server-dev-9.6 installed I can build the extension. Just… sometimes the query causes deadlock. I can run infer on the code too — it doesn’t find deadlocks yet but it does find bugs.

infer run -- make

Why doesn’t it find deadlocks? Well the English name of the functionReleaseBuffer doesn’t help Infer understand that it is a lock or allocation. We can teach it about new functions though — give it a model of what the function does in terms it understands.

For LockBuffer(), which is a function provided by psql, let’s teach infer some meaning by abusing allocation:

#if __INFER__
void LockBuffer(Buffer b, int lock)
{
    void *val = *(void**)b;
    switch (lock) {
        case BUFFER_LOCK_EXCLUSIVE:
            if(NULL != val) {
                __infer_fail("Locking a locked buffer...");
            } else {
                *((void**)b) = malloc(1);
            }
            break;
        case BUFFER_LOCK_UNLOCK:
            if(NULL == val) {
                __infer_fail("Unlocking an unlocked buffer...");
            } else {
                free(val);
                *(void**)b = NULL;
            }
            break;
        case BUFFER_LOCK_SHARE:
            if(NULL != val) {
                __infer_fail("Read Locking a locked buffer...");
            } else {
                *((void**)b) = malloc(2);
            }
            break;
        default:
            while(1);
    }
}
#endif /* __INFER__ */

Pretty simple once you get past the new function names. It’s just modeling locking a buffer as allocation and unlocking as freeing. I have made, but not shown, similar specifications for psql’s UnlockReleaseBuffer, ReadBuffer, and ReleaseBuffer . How does this change the reports?

make clean && infer run -- make

Pay dirt! It might not look like much, but that metaBuffer is pinned and needs to be unlock/released with a missing call to unlockReleaseBuffer. Knowing which resource was acquired is a huge step to knowing where to release it.

Closing Thoughts

Infer is pretty fast and gives amazing results. No configuration is necessary but can help in a pinch, as shown. Look around at what the world has produced in the last few years. Tools like full symbolic execution (an expensive and non-scalable process) are no longer the state of the industry. Look around at the tools available today, your coworkers will thank you.