Imagine planning a wedding dinner where you had to consider every possible combination of guests at each table.

Even if you didn’t worry about the exact seating order, by the time you got to 40 guests on 10 tables, the number of combinations would be astronomical.

Software developers have to consider an even larger number of possibilities when anticipating the potential problems that can occur in programs designed to carry out multiple tasks at once.

These programs are capable of executing more than one set of instructions concurrently, and while they can complete tasks rapidly and be more responsive to users, they can also throw up a huge number of potential problems.

Because one set of instructions is being executed at the same time as another set, there is potential for these instructions to interact in ways that trigger undesirable behavior, referred to as a race condition. An example might be where one set of instructions alters the value of a piece of data just before that same data is utilized by another set of instructions.

These race conditions are particularly difficult to anticipate by examining code. Even in a program with just 40 lines of code, considering every possible interaction between instructions in that program, when that program was run concurrently with itself, would take a computer millions of years.

To help simplify the problem of evaluating concurrent code, Facebook has developed RacerD, an automated static race condition detection tool that massively reduces the time it takes to flag potential problems in concurrent software.

“Our tool RacerD finds errors in much bigger programs than 40 instructions–with hundreds of thousands of instructions–in 15 minutes rather than 3.4 million years,” said professor Peter O’Hearn, a research scientist working with the Static Analysis Tools team in the Facebook London Engineering office.

O’Hearn is a former university professor who created the theory of concurrent separation logic, for which he was awarded computer science’s prestigious Gödel Prize in 2016. The theory relates to the combinatorial explosion problem that leads to it taking millions of years to consider all the possible interactions by concurrent software, and it is that theory that is the basis of how RacerD works.

“There was one core insight in that tool, which was don’t explore all of the possibilities by brute force, rather compute an approximation of what’s needed, which applies a lot of the things you need to figure out,” said O’Hearn.

For the past 10 months, Facebook has been using RacerD to check the large and rapidly changing codebase that underpins Facebook’s News Feed for Android devices, during which time the tool has caught 1,000 multi-threading issues before code was pushed to production.

SEE: Hiring kit: Python developer (Tech Pro Research)

“RacerD takes a lot of the difficult manual work and a lot of the scariness out of the process of adding concurrency to the News Feed,” said Sam Blackshear, research scientist with Facebook’s Infer team, adding that the use of concurrency had sped up the Android News Feed by 5%.

Facebook has built RacerD into Infer, its open-source static analyzer that runs automatically on every code change, checking for bugs such as null pointer exceptions and resource leaks and, now, concurrency errors before the code hits production.

The RacerD tool is being open-sourced and made available online from today, as part of the Infer static analyzer platform.

RacerD currently checks Java code and Blackshear said: “One of the reasons we’re open-sourcing it is we think it’ll be useful for all Android engineers, and potentially Java programmers everywhere.”

O’Hearn says Facebook will extend RacerD to the C++ programming language in the coming months, and over the next year will look to extend RacerD to work alongside other tools that automatically suggest fixes, and then certify the amended code.

“We’re going to get the computer to help in not just finding the bug, but in fixing the bug. This will speed up our developers and free their mind to concentrate on things where more human creativity is needed.”

Also see