It is a hardly discussed problem, but Android is a tough platform to use with concurrent programming. As a result most apps don't use it to its full potential. Facebook has now gifted you a tool that makes it a lot easier and is using it to make its own app faster and more reliable.

The RacerD project was started because the Facebook team realized that concurrency on anything was hard and on Android especially so. The reason Android is difficult is partly because of the lifecycle model of an app - and partly the lack of clear guidance on what works and what is best practice. At the lowest levels you don't get any help from the tooling to find basic things like race hazards. A race hazard is what you have if there are two or more threads performing an update - which one gets there last determines what the update is. Race updates are difficult to find because the code involved in a race can be spread over the codebase. 

RacerD uses some very clever symbolic reasoning to find code that is subject to race hazards. 

"To get an idea of the scale of the challenge, say a program wanted to examine each of the different ways that two threads of 40 lines of code can interact concurrently (“interleavings,” in the jargon). Even considering those interactions at a blazing rate of 1 billion interactions per second, the computer would be working for more than 3.4 million years! On the other hand, RacerD does its work in less than 15 minutes, for much larger programs than 80 lines."

To brute-force analyze a real program isn't feasible and so the Facebook team looked into using the theory of concurrent separation logic and proofs that code was free of race conditions. The work became more practical and urgent when the team working on the News Feed Android app were planning to change it from a mostly sequential design to a full multi-threaded architecture.  This pressure resulted in a Minimum viable produce and RacerD was born. 

RacerD's goal is to find data races. Its design is based on the following ideas:

1. Don't do whole-program analysis; be compositional.

2. Don't explore interleavings; track lock and thread information.

3. Don't attempt a general, precise alias analysis; use an aggressive ownership analysis for anti-aliasing of allocated resources.

So does it work?

The answer seems to yes:

"RacerD has been running in production for 10 months on our Android codebase and has caught over 1000 multi-threading issues which have been fixed by Facebook developers before the code reaches production. "

RacerD looks easy enough to use and the annotations it applies to your code are easy enough to understand. It runs as part of Infer Facebook's static analysis tool for Java, C/C++ and Objective C.It would be nice if Infer for Android was part of Android Studio but ...

The project is on GitHub with a standard BSD licence.

More Information

Open-sourcing RacerD: Fast static race detection at scale

RacerD

Infer

RacerD On GitHub

Related Articles

Facebook Open Sources Two Technologies

RocksDB on Steroids

RocksDB - Facebook's Database Now Open Source 

Facebook Open Sources Litho Android UI Framework

CrashScope Gets Android Crash Data So You Can Reproduce It

To be informed about new articles on I Programmer, sign up for our weekly newsletter, subscribe to the RSS feed and follow us on Twitter, Facebook or Linkedin.

Comments

Make a Comment or View Existing Comments Using Disqus

or email your comment to: comments@i-programmer.info