Program for the fall quarter of 2017.

9/28: Organizational Lunch

Time: Thursday, September 28, 2017, 12 noon - 1pm
Location: Gates 415

Organizational lunch. Come sign up to give a talk during the quarter.

Food: Stefan

10/5: PriMagic: Component-Based Synthesis with Control Structures

Time: Thursday, October 5, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Kensen Shi

Abstract: Previous works in component-based program synthesis have struggled to synthesize loops and other control structures. We present PriMagic, a new approach to component-based synthesis that can synthesize programs from input-output examples using control structures and arbitrary libraries. Our approach combines two main ideas. We mine primitives, obtaining code fragments from partial-successes that are likely to be useful for synthesis. We also use angelic conditions to optimistically evaluate partial programs with unspecified control structure conditions. Empirically, PriMagic can synthesize interesting programs with combinations of control structures within several minutes.

Food: Zhihao

10/12: Seam: Provably Safe Local Edits on Graphs

Time: Thursday, October 12, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Manolis Papadakis

Abstract: In this talk I will present Seam, a domain-specific language for describing graph-like data structures and programming local modification operations over them. Based on our preliminary results, programs written in Seam are competitive with hand-written implementations in terms of performance, while being an order of magnitude shorter, easier to maintain and extend, and amenable to static verification. I will focus on the design of our verification method for Seam operations: We leverage an SMT solver to verify that operations are memory-safe and maintain referential integrity and user-specified invariants. Our verification method is sound and precise (complete modulo termination of the SMT solver).

Food: Manolis

10/19: Control Replication: Compiling Implicit Parallelism to Efficient SPMD with Logical Regions

Time: Thursday, October 19, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Elliott Slaughter

Abstract: We present control replication, a technique for generating high-performance and scalable SPMD code from implicitly parallel programs. In contrast to traditional parallel programming models that require the programmer to explicitly manage threads and the communication and synchronization between them, implicitly parallel programs have sequential execution semantics and by their nature avoid the pitfalls of explicitly parallel programming. However, without optimizations to distribute control overhead, scalability is often poor.
Performance on distributed-memory machines is especially sensitive to communication and synchronization in the program, and thus optimizations for these machines require an intimate understanding of a program’s memory accesses. Control replication achieves particularly effective and predictable results by leveraging language support for first-class data partitioning in the source programming model. We evaluate an implementation of control replication for Regent and show that it achieves up to 99% parallel efficiency at 1024 nodes with absolute performance comparable to hand-written MPI(+X) codes.

Food: Giovanni

10/26: AI Complete: Smarter code assistant

Time: Thursday, October 26, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Maxim Sokolov

Abstract: Given large amount of code available at Facebook, we started looking into ways to use it to improve developers’ productivity.
AI Complete is an autocomplete provider which learns on our Hack codebase and is able to suggests whole statements using surrounding code context.
In the talk, we will present technology behind it. Although the AI Complete’s model is relatively simple it achieves exact accuracies of 30% and is able to
suggest a statement that it has never seen. AI Complete is deployed at Facebook and used by thousands of engineers.

Food: Todd

11/2: In situ visualization with task-based parallelism

Time: Thursday, November 2, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Alan Heirich

Abstract: This short paper describes an experimental prototype of in situ visualization in a task-based parallel programming framework. A set of reusable visualization tasks were composed with an existing simulation. The visualization tasks include a local OpenGL renderer, a parallel image compositor, and a display task. These tasks were added to an existing fluid-particle-radiation simulation and weak scaling tests were run on up to 512 nodes of the Piz Daint supercomputer. Benchmarks showed that the visualization components scaled and did not reduce the simulation throughput. The compositor latency increased logarithmically with increasing node count.

Food: Andres

11/9: User-Programmable Access Control via Communicating Virtual Asssitants

Time: Thursday, November 9, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Giovanni Campagna

Abstract: Today, individuals’ information and capabilities are siloed across many web accounts and IoT devices. Users wishing to share information are limited by what the service provider supports, or resort to giving out their account credentials.
We propose a novel, general, and secure method of sharing data and devices with the help of communicating virtual assistants. The owner of the data can specify, in natural language, what, when, how, where, and to whom the access is given, using a new policy language called Thing Access Control Language. A requester can ask the owner to execute any virtual assistant command. The command is locally translated to a program in the formal ThingTalk language and forwarded to the owner’s assistant, which adds run-time checks to the request if necessary and executes conforming requests on behalf of the requester.
We show that static and dynamic conformance of policies can be derived efficiently, with formal guarantees, using an algorithm based on Satisfiability Modulo Theories. We conducted a user study to collect use cases of access controls and found that, out of 220 use cases, 67% can be supported, provided the APIs are made available to the assistant.

11/16: Modular and Safe Event Driven Programming

Time: Thursday, November 16, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Ankush Desai

Abstract: Distributed systems are notoriously difficult to get right as they must deal with concurrency and failures. In the first part of my talk, I will present P[1], a communicating state machines based domain-specific language for building reliable distributed systems. For scalable analysis of distributed systems, P implements a module system based on the theory of compositional trace refinement for both compositional (assume-guarantee) and hierarchical (refinement) reasoning of dynamic distributed systems. P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows and Windows Phone.
Autonomous robots increasingly depend on third-party off-the-shelf components and complex machine-learning techniques. This trend makes it challenging to provide strong design-time certifications of correct operation. In the second half of my talk, I will present Drona[2], a framework for building safe robotics systems. Drona extends P with Runtime Assurance (RTA) capabilities to ensure end-to-end correctness of robotics systems. We recently did a successful DARPA demo where a team of drones was programmed using Drona to perform complex surveillance mission autonomously.
[1]https://github.com/p-org/P
[2]https://drona-org.github.io/Drona/

Food: Karthik

11/30: EMME: a formal tool for ECMAScript Memory Model Evaluation

Time: Thursday, November 30, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Cristian Mattarei

Abstract: Nearly all web-based interfaces are written in JavaScript. Given its prevalence, the support for high performance JavaScript code is crucial. The ECMA Technical Committee 39 (TC39) has recently extended the ECMAScript language (i.e., JavaScript) to support shared memory accesses between different threads. The extension is given in terms of a natural language memory model specification. In this work we describe a formal approach for validating both the memory model and its implementations in various JavaScript engines. We first introduce a formal version of the memory model and report results on checking the model for consistency and other properties. We then introduce our tool, EMME, built on top of the Alloy analyzer, which leverages the model to generate all possible valid executions of a given JavaScript program. Finally, we report results using EMME together with small test programs to analyze industrial JavaScript engines. We show that EMME is able to find bugs as well as missed opportunities for optimization.

12/7: Flow: Fast and Precise Type Checking for JavaScript

Time: Thursday, December 7, 2017, 12 noon - 1pm
Location: Gates 415

Speaker: Panagiotis Vekris

Abstract: In this talk we present the design and implementation of Flow, a fast and precise type checker for JavaScript that is used by thousands of developers on millions of lines of code at Facebook every day. Flow uses sophisticated type inference to understand common JavaScript idioms precisely. This helps it find non-trivial bugs in code and provide code intelligence to editors without requiring significant rewriting or annotations from the developer. We formalize an important fragment of Flow's analysis and prove its soundness. Furthermore, Flow uses aggressive parallelization and incrementalization to deliver near-instantaneous response times. This helps it avoid introducing any latency in the usual edit-refresh cycle of rapid JavaScript development. We describe the algorithms and systems infrastructure that we built to scale Flow's analysis.