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 http://people.csail.mit.edu/shachari/
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 

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.