|Time+Place:||Thursday 24/11/2016 10:30 Room 337 Taub Bld.|
|Title:||From Programming Languages to Programming Systems - Software Development by Refinement|
|Speaker:|| Shachar Itzhaky - CS-Lecture - NOTE UNUSUAL HOUR
|| Affiliation: || MIT - Computer Science Lab.
Everyone wants to program with "high-level concepts", rather than meddle with the fine details of the implementation, such as pointers, network packets, and asynchronous callbacks. This is usually achieved by introducing layers of abstraction - but every layer incurs some overhead, and when they accumulate, this overhand becomes significant and sometimes prohibitive. Optimizing the program often requires to break abstractions, which leads to suboptimal design, higher maintenance costs, and subtle hard-to-trace bugs. I will present two recent projects that attempt to address this difficulty. STNG is an automated lifting compiler that can synthesize high-level graphics code for computing stencils over matrices, from low-level legacy code written in Fortran. Its output is expressed in Halide, a domain-specific language for image processing that can take advantage of modern GPUs. The result is therefore code that is both easier to understand and more efficient than the original code. Bellmania is a specialized tool for accelerating dynamic-programming algorithms by generating recursive divide-and-conquer implementations of them. Recursive divide-and-conquer is an algorithmic technique that was developed to obtain better memory locality properties. Bellmania includes a high-level language for specifying dynamic programming algorithms and a calculus that facilitates gradual transformation of these specifications into efficient implementations. These transformations formalize the divide-and-conquer technique; a visualization interface helps users to interactively guide the process, while an SMT-based back-end verifies each step and takes care of low-level reasoning required for parallelism. The lesson is that synthesis techniques are becoming mature enough to play a role in the design and implementation of realistic software systems, by combining the elegance of abstractions with the performance gained by optimizing and tuning the fine details. Short bio: ========== I am a post-doc at MIT's Computer Science lab, working in the Computer-Aided Programming group headed by Prof. Armando Solar-Lezama. I have an M.Sc. and a Ph.D. from Tel Aviv University, done under the supervision of Prof. Mooly Sagiv. Prior to that I was a proud alum of the Open University.