Program for the fall quarter of 2018.
9/27: Organizational Lunch
Time: Thursday, September 27, 2018, 12 noon - 1pm
Location: Gates 415
Organizational lunch. Come sign up to give a talk during the quarter.
Food: Todd
10/4: A First Step Towards Understanding Stochastic Synthesis
Time: Thursday, October 4, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Jason Koenig
Abstract: Abstract: We consider the problem of understanding the behavior of program synthesis from input-output examples via stochastic search. We show the distribution of synthesis times is defined by the log-normal and gamma distributions, show why these distributions arise and give an algorithm that exploits this behavior to speed up synthesis by a factor of up to 27x. Our experimental results are obtained using a new program synthesis benchmark distilled from widely used production code.
Food: Todd
10/11: Optimizing DNN Computation with Automatically Generated Graph Substitutions
Time: Thursday, October 11, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Zhihao Jia
Abstract: Existing deep learning frameworks generally optimize computation in a DNN model by performing rule-based transformations on its computation graph. This approach depends on human experts to manually design graph transformations and has two limitations. First, existing systems only consider a limited set of commonly used graph transformations and may miss subtle optimizations for particular graphs. Second, this approach can hardly scale when today's DNN models continuously introduce new DNN operators, as optimizing new DNNs requires exploring various combinations of new operators with existing operators.
To address both limitations, I will talk about MetaFlow, an ongoing research project that aims at optimizing DNN computation with automatically generated graph substitutions. I will first show that it is possible to translate an arbitrary graph substitution to a set of SMT (satisfiability modulo theories) problems and uses a SMT solver to verify the correctness of the substitution. I will also present an efficient backtracking search algorithm to explore a large space of potential computation graphs and find optimized candidates. Our initial results show that MetaFlow improves DNN inference and training performance by up to 1.6x and 1.2x respectively over existing deep learning frameworks.
Food: Oded
10/18: Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Time: Thursday, October 18, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Oded Padon
Abstract: Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call *temporal prophecy*, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.
Practice talk for a paper to be presented in FMCAD 2018. Joint work with: Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelsk, Mooly Sagiv, and Sharon Shoham.
Food: Zhihao
10/25: AI-driven software quality assurance
Time: Thursday, October 25, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Roni Stern
Abstract: In this talk I will present our recent successful integration of various techniques from the Artificial Intelligence (AI) literature into the software debugging and testing process.
First, we show how data that is already stored by industry standard software engineering tools can be used to learn a fault prediction model able to predict accurate the software components that are likely to contain bugs. This allows focusing testing efforts on such error-prone components.
Then, we show how this learned fault prediction model can be used to augment existing software diagnosis algorithms, providing a better understanding of which software components need to be replaced to correct an observed bug. Moreover, for the case where further tests are needed to identify the faulty software component, we present a test-planning algorithm based on Markov Decision Processes (MDP). Importantly, the presented approach for considering both a fault prediction model, learned from past failures, and a diagnosis algorithm that is model-based, is general, and can be applied to other fields, beyond software troubleshooting. If time permits, I will also show more recent work in which we extended our software diagnosis approach to diagnose system exploits and vulnerabilities.
Food: Jason
11/1: Aroma – Code Recommendation via Structural Code Search
Time: Thursday, November 1, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Frank Luan
Abstract: Programmers often write code that is similar to existing code written somewhere. A tool that could help programmers to search such similar code would be immensely useful. Such a tool could enable programmers to find idiomatic code patterns, cross-check against similar code, and discover extensions to partially written code that would avoid common mistakes and errors. We describe Aroma, a tool and technique for creating code recommendation via structural code search. Aroma indexes a huge code corpus, takes a partial code snippet as input, and returns a set of “code recommendations” – succinct code snippets created from a cluster of similar code fragments containing the query code snippet. This is joint work with Di Yang, Koushik Sen and Satish Chandra carried out at Facebook.
Food: Sierra
11/8: Dynamic Tracing: Memoization of Task Graphs for Dynamic Task-Based Runtimes
Time: Thursday, November 8, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Wonchan Lee
Abstract: Many recent programming systems for both supercomputing and data center workloads generate task graphs to express computations that run on parallel and distributed machines. Due to the overhead associated with constructing these graphs the dependence analysis that generates them is often statically computed and memoized, and the resulting graph executed repeatedly at runtime. However, many applications require a dynamic dependence analysis due to data dependent behavior, but there are new challenges in capturing and re- executing task graphs at runtime. In this work, we introduce dynamic tracing, a technique to capture a dynamic dependence analysis of a trace that generates a task graph, and replay it. We show that an implementation of dynamic tracing improves strong scaling by an average of 4.9X and up to 7.0X on a suite of already optimized benchmarks.
Food: Karthik
11/15: None
Time: Thursday, November 15, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: N/A
Abstract: No lunch this week.
11/22: Thanksgiving - No Lunch
Time: Thursday, November 22, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: N/A
11/29: Semantic Program Alignment for Equivalence Checking
Time: Thursday, November 29, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Berkeley Churchill
Abstract: We introduce a robust semantics-driven technique for program equivalence checking. Given two functions we find a trace alignment over a set of concrete executions of both programs and construct a product program particularly amenable to checking equivalence.
We demonstrate that our algorithm is applicable to challenging equivalence problems beyond the scope of existing techniques. For example, we verify the correctness of the hand-optimized vector implementation of strlen that ships as part of the GNU C Library, as well as the correctness of vectorization optimizations for 56 benchmarks derived from the Test Suite for Vectorizing Compilers.
Food: Oded
12/6: Algorithmic Improvisation
Time: Thursday, December 6, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Daniel Fremont
Abstract: Algorithmic Improvisation is a framework for automatically synthesizing systems with random but controllable behavior. It can be used in a wide variety of applications where randomness can provide variety, robustness, or unpredictability but safety guarantees or other properties must be ensured. These include software fuzz testing, robotic surveillance, machine music improvisation, randomized control of systems mimicking human behavior, and generation of synthetic data sets to train and test machine learning algorithms. In this talk, I will discuss both the theory of algorithmic improvisation and its practical applications. I will define the underlying formal language-theoretic problem, “control improvisation”, analyze its complexity and give efficient algorithms to solve it. I will describe in detail two applications: planning randomized patrol routes for surveillance robots, and generating random scenes of traffic to improve the reliability of neural networks used for autonomous driving. The latter application involves the design of a domain-specific probabilistic programming language to specify traffic and other scenarios.
Food: Sumith
12/13: Deploying Reboot-able Dynamic Task Graphs
Time: Thursday, December 13, 2018, 12 noon - 1pm
Location: Gates 415
Speaker: Karthik Murthy
Abstract: Dynamic task graphs are used by language runtimes to achieve high parallel performance efficiency. In this talk, we highlight the need for these runtimes to deploy reboot-able dynamic task graphs. We propose a design to achieve reboot-ability, and we present preliminary performance results for an implementation of the same design in the Legion parallel programming model. Additionally, we discuss several applications of this design in achieving resilience, supporting speculation, varying the mapping decisions for tasks, and achieving task variability using LLVM-Polly.
Food: Todd