All Research Areas
Research Areas
Year Published

100 Results

August 13, 2015

From Categorical Logic to Facebook Engineering

30th Annual ACM/IEEE Symposium on Logic in Computer Science

I chart a line of development from category-theoretic models of programs and logics to automatic program verification/analysis techniques that are in deployment at Facebook. Our journey takes in a number of concepts from the computer science logician’s toolkit – including categorical logic and model theory, denotational semantics, the Curry-Howard isomorphism, substructural logic, Hoare Logic and Separation Logic, abstract interpretation, compositional program analysis, the frame problem, and abductive inference.

By: Peter O'Hearn
June 22, 2015

Revisiting Memory Errors in Large-Scale Production Data Centers: Analysis and Modeling of New Trends from the Field

IEEE/IFIP International Conference on Dependable Systems and Networks

In this paper, we analyze the memory errors in the entire fleet of servers at Facebook over the course of fourteen months, representing billions of device days.

By: Justin Meza, Qiang Wu, Sanjeev Kumar, Onur Mutlu
June 15, 2015

A Large-Scale Study of Flash Memory Failures in the Field

ACM Sigmetrics 2015

This paper presents the first large-scale study of flash-based SSD reliability in the field.

By: Justin Meza, Qiang Wu, Sanjeev Kumar, Onur Mutlu
May 19, 2015

Challenges to Adopting Stronger Consistency at Scale

Workshop on Hot Topics in Operating Systems

There have been many recent advances in distributed systems that provide stronger semantics for geo-replicated data stores like those underlying Facebook. At Facebook we are excited by these lines of research, but fundamental and operational challenges currently make it infeasible to incorporate these advances into deployed systems. This paper describes some of these challenges with the hope that future advances will address them.

By: Philippe Ajoux, Nathan Bronson, Sanjeev Kumar, Wyatt Lloyd, Kaushik Veeraraghavan
May 6, 2015

Wormhole: Reliable Pub-Sub to Support Geo-replicated Internet Services

12th USENIX Symposium on Networked Systems Design and Implementation

Wormhole is a publish-subscribe (pub-sub) system developed for use within Facebook’s geographically replicated datacenters. It is used to reliably replicate changes among several Facebook services including TAO, Graph Search and Memcache. This paper describes the design and implementation of Wormhole as well as the operational challenges of scaling the system to support the multiple data storage systems deployed at Facebook.

By: Yogeshwer Sharma, Philippe Ajoux, Petchean Ang, David Callies, Abhishek Choudhary, Laurent Demailly, Thomas Fersch, Liat Atsmon, Andrzej Kotulski, Sachin Kulkarni, Sanjeev Kumar, Hu Li, Jun Li, Evgeniy Makeev, Kowshik Prakasam, Robbert van Renesse, Sabyasachi Roy, Pratyush Seth, Yee Jiun Song, Kaushik Veeraraghavan, Benjamin Wester, Peter Xie
February 10, 2015

Moving Fast with Software Verification

NASA Formal Method Symposium

For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error free software. Available tools are often lacking in helping programmers develop more reliable and secure applications.

By: Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Churchill
October 27, 2014

Characterizing Load Imbalance in Real-World Networked Caches

HotNets 2014: Thirteenth ACM Workshop on Hot Topics in Networks

Modern Web services rely extensively upon a tier of in-memory caches to reduce request latencies and alleviate load on backend servers. Within a given cache, items are typically partitioned across cache servers via consistent hashing, with the goal of balancing the number of items maintained by each cache server. Effects of consistent hashing vary by associated hashing function and partitioning ratio. Most real-world workloads are also skewed, with some items significantly more popular than others. Inefficiency in addressing both issues can create an imbalance in cache-server loads. We analyze the degree of observed load imbalance, focusing on read-only traffic against Facebook’s graph cache tier in Tao. We investigate the principal causes of load imbalance, including data co-location, non-ideal hashing scenarios, and hot-spot temporal effects. We also employ trace-drive analytics to study the benefits and limitations of current load-balancing methods, suggesting areas for future research.

By: Qi Huang, Helga Gudmundsdottir, Ymir Vigfusson, Daniel A. Freedman, Ken Birman, Robbert van Renesse
October 24, 2014

The HipHop Virtual Machine

ACM International Conference on Object Oriented Programming Systems, Languages, and Applications

The HipHop Virtual Machine (HHVM) is a JIT compiler and runtime for PHP. While PHP values are dynamically typed, real programs often have latent types that are useful for optimization once discovered….

By: Keith Adams, Jason Evans, Bertrand Maher, Guilherme Ottoni, Drew Paroski, Brett Simmers, Edwin Smith, Owen Yamauchi
October 7, 2014

f4: Facebook’s Warm BLOB Storage System

Operating Systems Design and Implementation

Facebook’s corpus of photos, videos, and other Binary Large OBjects (BLOBs) that need to be reliably stored and quickly accessible is massive and continues to grow.

By: Subramanian Muralidhar, Wyatt Lloyd, Sabyasachi Roy, Cory Hill, Ernest Lin, Weiwen Liu, Satadru Pan, Shiva Shankar, Viswanath Sivakumar, Linpeng Tang, Sanjeev Kumar
October 6, 2014

The Mystery Machine: End-to-end Performance Analysis of Large-scale Internet Services

Operating Systems Design and Implementation

Current debugging and optimization methods scale poorly to deal with the complexity of modern Internet services, in which a single request triggers parallel execution of numerous heterogeneous softwar…

By: Mike Chow, David Meisner, Jason Flinn, Daniel Peek, Thomas Wenisch