As part of Meta’s commitment to innovation, members of the Developer Infrastructure (DevInfra) team are often involved in academic papers. Over the past six months, our research has broken new ground into the design of build systems, code optimizations for mobile apps, bug finding tools, and ML models for developer productivity. We’ve also worked with others outside Meta as we seek to build and share what we’ve learned. In this post, we’ve collected recent papers of interest to the engineering community.

Build systems

Meta is always looking at the theoretical foundations of build systems, and particularly in relation to our homegrown Buck build system, to provide more formal guarantees regarding its soundness and efficiency.

• Forward build systems, formally, by Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt, addresses the problem of formally verifying realistic build systems that automatically determine the dependency structure of the build.
• Implementing applicative build systems monadically, by Bob Yang and Neil Mitchell, revisits the distinction between monadic and applicative build systems and describes an incremental computation engine for Buck that improves code complexity and performance.

Code size optimization for mobile apps

The sheer size of some mobile apps can pose a challenge to users who don’t have access to high-end devices or broadband wireless networks. To ensure that our services are available to the largest possible audience, we have developed new optimization techniques to automatically reduce the binary size of mobile apps.

• Scalable size inliner for mobile applications, by Kyungwoo Lee, Manman Ren, and Shane Nay, describes a new approach to inlining driven by a global analysis that improves on the state of the art for binary size optimization of real-world mobile apps.
• Efficient profile-guided size optimization for native mobile applications, by Kyungwoo Lee, Ellis Hoag, and Nikolai Tillmann, introduces a new lightweight instrumentation that enables effective profile-guided optimization of real-world mobile apps.

Logic for bug finding and verification

Automatically surfacing important, hard-to-find bugs to developers early in the development cycle allows them to move faster and with more confidence. Similarly, building reliable software requires tooling that offers strong guarantees to developers that critical bugs will be either caught early or prevented entirely. We have leveraged formal verification techniques and developed new program logics to deliver high-quality signals to developers and raise confidence in critical software components.

• Finding real bugs in big programs with incorrectness logic, by Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn, describes an effective, fully automated analysis for catching memory errors in programs based on the formal framework of incorrectness logic.
• Concurrent incorrectness separation logic, by Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn, applies the framework of incorrectness logic to the design of static analyzers that can catch real bugs, like data races or deadlocks, in concurrent programs.
• Applying formal verification to microkernel IPC at meta, by Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O’Hearn, and Francesco Zappa Nardelli, demonstrates the use of proof assistants to formally verify two concurrent lock-free queue data structures for an industrial-scale operating system.

Machine learning for developer tools

The topic of neural networks and machine learning (ML) has been a great driver of recent innovations in computer science. We have been exploring the use of advanced ML models in developer tooling to provide better, more accurate information during code development and review.

• Detecting privacy-sensitive code changes with language modeling, by Gökalp Demirci, Vijayaraghavan Murali, Imad Ahmad, Rajeev Rao, and Gareth Ari Aye, leverages techniques from natural language processing to build an ML model that can detect privacy issues in code changes from developers.
• Improving code autocompletion with transfer learning, by Wen Zhou, Seohyun Kim, Vijayaraghavan Murali, and Gareth Ari Aye, investigates new approaches to the pretraining of ML models used for autocompletion in IDEs, resulting in significantly higher prediction accuracy.
• Counterfactual explanations for models of code, by Jürgen Cito, Isil Dillig, Vijayaraghavan Murali, and Satish Chandra, addresses the problem of explaining decisions made by opaque ML models in developer tools by constructing examples of code changes that fix the issues detected by the ML model.

About DevInfra

Developer Infrastructure (DevInfra) owns most of the coding life cycle at Meta, from the time code leaves an engineer’s mind until it reaches the people who use our products. Our goal is to increase developer efficiency so that we can continue to give people the power to build community and bring the world closer together. Meta is one of the leaders in the industry, building innovative developer tools and automation infrastructure that are reliable and fast, ensuring that every second of engineering time is spent on the things that matter most.