Research Area
Year Published

132 Results

July 9, 2018

Continuous Reasoning: Scaling the Impact of Formal Methods

Logic in Computer Science

This paper describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that advances in continuous reasoning will allow formal reasoning to scale to more programs, and more programmers.

By: Peter O'Hearn

July 9, 2018

Experience developing and deploying concurrency analysis at Facebook

Static Analysis Symposium

This paper tells the story of the development of RacerD, a static program analysis for detecting data races that is in production at Facebook. The technical details of RacerD are described in a separate paper; we concentrate here on how the project unfolded from a human point of view.

By: Peter O'Hearn

July 1, 2018

We Need a Testability Transformation Semantics

16th International Conference on Software Engineering and Formal Methods

This paper briefly reviews Testability Transformation, its formal definition, and the open problem of constructing a set of formal test adequacy semantics to underpin the current practice of deploying transformations to help testing and verification activities.

By: Mark Harman

June 28, 2018

Hardware Remediation At Scale

International Conference on Dependable Systems and Networks (DSN)

Large scale services have automated hardware remediation to maintain the infrastructure availability at a healthy level. In this paper, we share the current remediation flow at Facebook, and how it is being monitored.

By: Fan (Fred) Lin, Matt Beadon, Harish Dattatraya Dixit, Gautham Vunnam, Amol Desai, Sriram Sankar

June 20, 2018

HHVM JIT: A Profile-Guided, Region-Based Compiler for PHP and Hack

Programming Language Design and Implementation (PLDI)

This paper describes the design of the second generation of the HHVM JIT and how it addresses the challenges to efficiently execute PHP and Hack programs. This new design uses profiling to build an aggressive region-based JIT compiler. We discuss the benefits of this approach compared to the more popular method-based and trace-based approaches to compile dynamic languages.

By: Guilherme Ottoni

May 16, 2018

Glow: Graph Lowering Compiler Techniques for Neural Networks

arXiv

This paper presents the design of Glow, a machine learning compiler for heterogeneous hardware. It is a pragmatic approach to compilation that enables the generation of highly optimized code for multiple targets. Glow lowers the traditional neural network dataflow graph into a two-phase strongly-typed intermediate representation.

By: Saleem Abdulrasool, Summer Deng, Roman Dzhabarov, Jordan Fix, James Hegeman, Roman Levenstein, Bert Maher, Satish Nadathur, Jakob Olesen, Jongsoo Park, Artem Rakhov, Nadav Rotem, Misha Smelyanskiy

April 23, 2018

Reducing DRAM Footprint with NVM in Facebook

EUROSYS 2018

In this work, we design a key-value store, MyNVM, which leverages an NVM block device to reduce DRAM usage, and to reduce the total cost of ownership, while providing comparable latency and queries-per-second (QPS) as MyRocks on a server with a much larger amount of DRAM. Replacing DRAM with NVM introduces several challenges. In particular, NVM has limited read bandwidth, and it wears out quickly under a high write bandwidth.

By: Assaf Eisenman, Darryl Gardner, Islam AbdelRahman, Jens Axboe, Siying Dong, Kim Hazelwood, Chris Petersen, Asaf Cidon, Sachin Katti

April 16, 2018

Rethinking Concurrency Control for In-Memory OLAP DBMSs

IEEE International Conference on Data Engineering (ICDE)

In this paper we describe a new concurrency control protocol specifically designed for analytical DBMSs that can provide Snapshot Isolation for distributed in-memory OLAP database systems, called Append-Only Snapshot Isolation (AOSI).

By: Pedro Pedreira, Yinghai Lu, Sergey Pershin, Amit Dutta, Chris Crosswhite

April 9, 2018

Semi-Oblivious Traffic Engineering: The Road Not Taken

USENIX Symposium on Networked Systems Design and Implementation (NSDI)

This paper presents a system that uses a set of paths computed using Räcke’s oblivious routing algorithm, as well as a centralized controller to dynamically adapt sending rates. Although oblivious routing and centralized TE have been studied previously in isolation, their combination is novel and powerful.

By: Praveen Kumar, Yang Yuan, Chris Yu, Nate Foster, Robert Kleinberg, Petr Lapukhov, Chiun Lin Lim, Robert Soule

March 28, 2018

SmoothOperator: Reducing Power Fragmentation and Improving Power Utilization in Large-scale Datacenters

ASPLOS 2018

With the ever growing popularity of cloud computing and web services, Internet companies are in need of increased computing capacity to serve the demand. However, power has become a major limiting factor prohibiting the growth in industry: it is often the case that no more servers can be added to datacenters without surpassing the capacity of the existing power infrastructure.

By: Chang-Hong Hsu, Qingyuan Deng, Jason Mars, Lingjia Tang