Add to Calendar
2019-05-17 15:00:00
2019-05-17 16:00:00
America/New_York
Relational Reasoning for Mergeable Replicated Data Types
Abstract: Programming geo-replicated distributed systems is challenging given the complexity of reasoning about different evolving states on different replicas. Existing approaches to this problem impose a significant burden on application developers to consider the effect of how operations performed on one replica are witnessed and applied on others. To alleviate these challenges, we present a fundamentally different approach to programming in the presence of replicated state. Our insight is based on the use of invertible relational specifications of an inductively-defined data type as a mechanism to capture salient aspects of the data type relevant to how its different instances can be safely merged in a replicated environment. Importantly, because these specifications only address a data type's (static) structural properties, their formulation does not require exposing low-level system-level details concerning asynchrony, replication, visibility, etc. As a consequence, our framework enables the correct-by-construction synthesis of rich merge functions over arbitrarily complex (i.e., composable) data types. In this talk, I'll show that the use of a rich relational specification language allows us to extract sufficient conditions to automatically derive merge functions that have meaningful non-trivial convergence properties.Bio: KC Sivaramakrishnan is an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras. He works on the intersection of Programming Languages and (Concurrent, Parallel, Distributed) Systems. He leads the Multicore OCaml project which extends the OCaml programming language with support for lightweight concurrency and shared memory parallelism. He led the development of MultiMLton, a multicore-aware runtime for MLton Standard ML compiler and Quelea, a language for programming over distributed databases. He has held research positions at University of Cambridge, Microsoft Research Cambridge, and Samsung Research. He obtained his PhD from Purdue University developing functional programming abstractions for weakly consistent systems.
32-G575
May 17
May 02
Differentiable Programming for Machine Learning
Martin Abadi and Dougal Maclaurin
Google
Add to Calendar
2019-05-02 16:00:00
2019-05-02 17:00:00
America/New_York
Differentiable Programming for Machine Learning
Abstract:The recent successes of machine learning are due in part to the invention of machine learning methods (especially for deep learning), to the collection of datasets for tackling problems in many fields, and to the availability of powerful hardware, including CPUs, GPUs, and custom-designed ASICs. Software systems, however, are central to this progress.This talk suggests that it is instructive and fruitful to think of these software systems from a programming-language perspective. A system such as TensorFlow owes its power and generality to its programmability. There, models for machine learning are assembled from primitive operations by function composition and other simple, familiar constructs, with in addition support for automatic differentiation, which is uncommon in mainstream programming languages but prominent in current machine learning methods.The design and the principles of the corresponding programming languages remain active research areas. This talk presents some recent results on the semantics of these languages, focusing on a tiny but expressive language for differentiable programming. It also includes an introduction to JAX, a new system for composable transformations of numerical Python programs, including automatic differentiation and compilation for hardware accelerators.The talk is based on joint work with many people, in particular Gordon Plotkin and the many contributors to the systems described.
March 13
Add to Calendar
2019-03-13 11:00:00
2019-03-13 12:00:00
America/New_York
Discover[i]: Component-based Parameterized Reasoning for Distributed Applications
Distributed systems are hard to get right. There have been many notable efforts in formal reasoning for distributed systems: these efforts have focused on language design, automated or semi-automated verification, and, more recently, on automated synthesis for systems with a fixed number of processes. Our Discover[i] project seeks to automate aspects of programming distributed applications by developing new foundations, algorithms and tools for synthesis/verification of distributed applications built using (verified) components and parameterized by the number of processes. In this talk, I will present an approach for parameterized synthesis of coordination for distributed systems that use consensus protocols, such as Paxos, as a building block to provide higher-level functionality. Our approach is based on (1) encapsulating the details of consensus into a simple atomic primitive, (2) a decidability result for parameterized verification of safety properties of systems with such consensus primitives, and (3) decision procedures for parameterized synthesis. We have used our tool to synthesize coordination for several examples of distributed applications, including a model of the Small Aircraft Tracking System.Bio: Roopsha Samanta is an Assistant Professor in the Department of Computer Science at Purdue University. Her research mission is to make it easier for people to build provably reliable programs. Her research focuses on developing algorithms and tools for automated program repair and synthesis, and targets diverse application domains such as concurrent and distributed systems, personalized education and machine learning.Roopsha completed her Ph.D. at The University of Texas at Austin in 2013 and was a postdoctoral researcher at the Institute of Science and Technology Austria (IST Austria) from 2014-2016.
Seminar Room G882 (Hewlett Room)
January 11
Sketch Internals Tutorial
Armando Solar-Lezama
Add to Calendar
2019-01-11 9:30:00
2019-01-11 15:00:00
America/New_York
Sketch Internals Tutorial
The Sketch synthesis system is an open source infrastructure for program synthesis that has been used in a variety of research projects in academia and industrial research labs. Sketch is based on a powerful symbolic search procedure that allows users to describe spaces of possible programs and then automatically search that space for a program that satisfies a given specification. In this hands-on tutorial, I will cover the internals of the Sketch synthesis system and some of the key algorithms behind it. The tutorial is aimed at students and researchers who wish to contribute to the Sketch synthesizer or simply gain a better understanding of how the system works in order to use it more effectively.
Seminar Room G449 (Patil/Kiva)
December 10
Humans Compose when Software Does
Alan Edelman, Jeff Bezanson
MIT, Julia Computing
Add to Calendar
2018-12-10 16:00:00
2018-12-10 17:00:00
America/New_York
Humans Compose when Software Does
Abstract:In the early days of 18.337/6.338, we gave a simple assignment. Part 1: Download any parallel program and run it. Part 2: Download two parallel programs and have them compose. Smart hard-working students failed miserably with Part 2. Fast forward to 2018, with the formation of MIT's College of Computing, and some of us dream that Part 1: Researchers at MIT will continue excellent research and Part 2: Researchers across disciplines can compose.We have found that the Julia language, through its composable abstractions, multiple dispatch, and expressive typing is accelerating the formation of bridges at MIT. As physical bridges may be made from steel and provide infrastructure for many to cross, it seems Julia's language elements are the medium that allow people to connect to solve hard problems.In this talk we will give a quick introduction to Julia, and then speak in depth about some of Julia's special features.Bio: Professor Alan Edelman (Math,CSAIL,CCE) loves to prove pure and applied theorems, program computers and everything in between. He has received many prizes including a Gordon Bell Prize, a Householder Prize, and a Charles Babbage Prize, is a fellow of IEEE, AMS, and SIAM, and is a founder and chief scientist of Interactive Supercomputing and Julia Computing, Inc. He passionately believes in more interactions between classical computer science and computational science. Edelman's research interests include Julia, machine learning, high-performance computing, numerical computation, linear algebra, random matrix theory and geometry. He has consulted for IBM, Pixar, Akamai, Intel, and Microsoft among other corporations.Jeff is one of the creators of Julia, co-founding the project at MIT in 2009 and eventually receiving a Ph.D. related to the language in 2015. He met Professor Edelman at Interactive Supercomputing, beginning a long collaboration. He continues to work on the Julia compiler and system internals, while also working to expand the language's commercial reach as a co-founder of Julia Computing, Inc.
32-D463 (Star)
December 03
Add to Calendar
2018-12-03 16:00:00
2018-12-03 17:00:00
America/New_York
The Dataflow Model of Computation
Abstract: The dataflow model formed the basis for a class of parallel programming languages and architectures in the nineteen seventies and eighties. We will describe Jack Dennis’ dataflow model of computation and its variants. Bio: Arvind is the Johnson Professor of Computer Science and Engineering at MIT. Arvind’s group, in collaboration with Motorola, built the Monsoon dataflow machines and its associated software in the late eighties. In 2000, Arvind started Sandburst which was sold to Broadcom in 2006. In 2003, Arvind co-founded Bluespec Inc., an EDA company to produce a set of tools for high-level synthesis. Arvind's current research focus is to enable rapid development of embedded systems. Arvind is a Fellow of IEEE and ACM, and a member of the National Academy of Engineering (USA) and the American Academy of Arts and Sciences.
November 01
P : Modular and Safe Event-Driven Programming
Ankush Desai
EECS Department - UC Berkeley
Add to Calendar
2018-11-01 14:00:00
2018-11-01 15:00:00
America/New_York
P : Modular and Safe Event-Driven Programming
CSAIL CONFERENCE ROOM, 32-D463Abstract:Asynchronous event-driven systems are ubiquitous across domains such as distributed systems, device drivers, and robotic systems. These systems are notoriously hard to get right as the programmer needs to reason numerous control paths resulting from the myriad interleaving of events (messages) and failures.In this talk, I will present the P language for modular and safe event-driven programming. P unifies modeling and programming into one activity for the programmer. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P also supports a module system that enables compositional (assume-guarantee) and hierarchical (refinement) reasoning of event-driven programs. Not only can a P program be compiled into executable code, but it can also be validated using state-of-the-art systematic testing (e.g., using search prioritization and symbolic execution). Using P's module system one can scale systematic testing to large, industrial-scale implementations by decomposing the system-level testing problem into a collection of simpler component-level testing problems.P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. More recently, we have used P for the design and implementation of fault-tolerant distributed systems and robotics systems with safety-assurance.P language: https://github.com/p-org/PBio:Ankush Desai is a Ph.D. student in the EECS department at UC Berkeley working with Prof. Sanjit Seshia and Dr. Shaz Qadeer. His research focuses on designing tools and techniques in the area of programming languages, formal methods, and software engineering, and applying them to build reliable systems across domains like device drivers, distributed systems, robotics, and cyber-physical systems.His research has had an impact both in Industry and Academia for which he was awarded the Sevin Rosen Funds Award for Innovation in 2018.Before joining the graduate school, Ankush spent 2+ years at Microsoft Research (India) working with Dr. Sriram Rajamani and Dr. Shaz Qadeer applying formal methods to build reliable device drivers. At IIT Kanpur, he was part of the team that built the first Indian Nano-Satellite JUGNU (launched on 12 October 2011). As a part of his Master's thesis, he designed and implemented the software stack for the on-board computer of the satellite.