- Laowai Guide
Hardening Tools for C
The target audience for this tutorial is interested in increasing the quality of one or more tools that process C code. Csmith, our random program generator, is useful in this regard, having uncovered more than 400 previously unknown bugs in C compilers and more than 50 bugs in non-compiler tools (such as static analyzers) for C. The focus will be on pragmatic issues such as choosing appropriate invariants to test, selecting an appropriate C subset, narrowing down the circumstances leading to tool failure, and automating the testing workflow.
John Regehr is an associate professor in computer science at the University of Utah. His research focuses on improving software quality.
McLab, a Compiler and VM Framework for MATLAB
MATLAB is a popular dynamic programming language used for scientific and numerical programming. As a language, it has evolved from a small scripting language intended as an interactive interface to numerical libraries, to a very popular language supporting many language features and libraries. The overloaded syntax and dynamic nature of the language, plus the somewhat organic addition of language features over the years, makes static analysis of modern MATLAB quite challenging. The tutorial will introduce the MATLAB language, the importance of compiler research for MATLAB and similar dynamic scientific languages, and the particular challenges the language presents for compiler developers. The tutorial will then provide an overview of the McLAB infrastructure, with a more in-depth presentation of the static analysis framework.
Laurie Hendren leads the Sable Research Group. She has been a professor at McGill since 1990, was made an ACM Fellow in 2010, and was awarded a Canada Research Chair in Compiler Tools and Techniques in 2011. The Sable Research Group has previously designed and implemented Soot and associated tools for the analysis and transformation of Java.
Grace: an Open-Source OO Educational Programming Language
Grace aims to demonstrate the advantages of object-orientation, showing how a small number of underlying principles can be applied uniformly: programs built from nested objects, computation as requesting behaviour from objects, and the separation of types and classes. Grace makes it possible to write powerful libraries that extend the language, supporting first-class pattern matching, parser combinators, and flexible control structures. Grace also supports, but does not require, static type checking. This makes it possible to use Grace as a dynamically typed language, to start with dynamic types and add static types later, or to teach static types from the beginning. In this talk, I'll outline the principal features of Grace, discuss open issues, and listen to your reactions while some choices are still on the table. I'll give some examples from the design process so far, showing how conceptually orthogonal design decisions all too easily end up as tightly coupled gordian knots.
James Noble is a professor at Victoria University of Wellington, New Zealand. James's research centres around software design.
Data Parallel Programming in Haskell
The Glasgow Haskell Compiler comes with support for a range of concurrent and parallel programming models, which take advantage of Haskell's rigorous control of side effects. In this talk, we will specifically focus on data parallel programming for shared-memory hardware, covering both regular and nested data parallelism as well as targeting both CPUs and GPUs. We will have a detailed look at how to write data parallel code in Haskell by discussing the implementation of example applications, such as edge detection and particle systems. This talk will give an overview over the state of the art of data parallel programming in Haskell. It will outline the range of use of the existing technology and show you how to get started on writing your own data parallel programs.
Manuel Chakravarty is an Associate Professor at the University of New South Wales. He holds a doctoral degree from the Berlin Institute of Technology. He contributed to Haskell's foreign function interface, the theory and implementation of type families, and the design and realisation of Data Parallel Haskell, an implementation of nested data parallelism in the Glasgow Haskell Compiler.
SnuCL: An OpenCL Framework for Heterogeneous CPU+GPU Clusters
Open Computing Language (OpenCL) is a programming model for heterogeneous parallel computing systems. OpenCL provides a common abstraction layer across different multicore architectures, such as CPUs, GPUs, DSPs, and Cell BE processors. Programmers can write an OpenCL application once and run it on any OpenCL-compliant system. However, current OpenCL is restricted to a single operating system instance. To target heterogenous CPU/GPU clusters, programmers must use the OpenCL framework combining with a communication library, such as MPI. This tutorial will cover usages and internals of an OpenCL framework, called SnuCL. It naturally extends the original OpenCL semantics to the heterogeneous cluster environment. The target cluster contains multiple CPUs and GPUs in a node. The nodes in the cluster are connected by an interconnection network, such as Gigabit and InfiniBand switches. For such clusters, SnuCL provides an illusion of a single operating system image for the programmer. With SnuCL, OpenCL applications written for a single operating system instance with multiple OpenCL compute devices can run on the cluster without any modification. This tutorial will introduce you to OpenCL and how OpenCL applications are developed for heterogeneous computing systems.
Jaejin Lee is the director of the Center for Manycore Programming and a professor of Computer Science and Engineering at Seoul National University. He obtained a Ph.D. from UIUC in 1999 in the area of compilation techniques for explicitly parallel programs. His primary research focus in these days is on heterogeneous parallel programming models such as OpenCL.
Avik Chaudhuri is a programming language design expert at Adobe Systems, where his overall role is to shape the future of the language in which Flash-based games are developed. Prior to joining Adobe, he completed a PhD at UCSC in 2008 and a post-doc at UMD in 2010.
Abstractions & Languages for Wireless Sensor Networks
Wireless Sensor Networks (WSNs) are currently regarded as a key technology towards the vision of an “Internet of Things”. The current practice in programming WSNs largely revolves around low-level programming frameworks. Such an approach is not sustainable in the long term, and is certainly not applicable when WSNs become part of a larger computing infrastructure. In this tutorial, we begin with a characterization of WSN applications to identify the fundamental requirements at stake, and describe a taxonomy of high-level WSN programming solutions providing a foundation to classify, compare, and evaluate the various approaches. We intertwine the description with live demonstrations of the technology being discussed. The tutorial is aimed at fresh students looking for interesting problems, researchers willing to gain deeper insights into WSN programming, and practitioners in search of a systematic overview on the topic.
Luca Mottola is an assistant professor at Politecnico di Milano and a Senior Researcher at the Swedish Institute of Computer Science. His research interests include the design, implementation, and validation of modern distributed systems, with the current focus on Internet of Things. He was listed amongst Postscapes "Internet of Things Top 100 Thinkers" and has received the Cor Baayen Award for the most promising young researcher in computer science and applied mathematics.
The K Framework
K is an executable modular framework for programming language semantics, design and analysis. It is particularly suitable for defining truly concurrent languages/calculi, as well as for defining control-intensive language features such as abrupt termination, exceptions, or call/cc. K has been used to define real world languages like C. This tutorial will provide participants with a basic knowledge of the framework, showing how you can automatically generate an interpreter, debugger, state space searcher, and other formal analysis tools, all from an arbitrary language semantic definition using K. To exemplify the framework, prototypical languages covering the imperative, functional, object-oriented and logic programming paradigms will be defined.
Grigore Rosu is an Associate Professor at the University of Illinois at Urbana-Champaign. His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames.
Yogi: Property Checking via Static Analysis and Testing
Aditya Nori & Sriram Rajamani
Static analysis and testing are complementary approaches to the property checking problem. The goal of Yogi is to solve the property checking problem. One of the unique features of Yogi is that it simultaneously searches for both a test to establish that the program violates the property, and an abstraction to establish that the program satisfies the property. If the abstraction has a path that leads to the violation of the property, Yogi attempts to focus test case generation along that path. If such a test case cannot be generated, Yogi uses information from the unsatisfiable constraint from the test case generator to refine the abstraction. Thus, the construction of test cases and abstraction proceed hand-in-hand, using error traces in the abstraction to guide test case generation, and constraints from failed test-case generation attempts to guide refinement of the abstraction.
Aditya V. Nori is a researcher at Microsoft Research India. His research interests include program analysis and machine learning with special focus on tools for improving software reliability and programmer productivity. He received his PhD from the Indian Institute of Science.
Sriram K. Rajamani is the assistant managing director of Microsoft Research India. His research interests are in programming languages and tools. Several of his projects have influenced academia and industry, the most notable one being SLAM which is the basis for Microsoft's Static Driver Verifier. He holds a PhD from the University of California at Berkeley.
Developing and Using Pluggable Type Systems
A pluggable type system extends a language's built-in type system to confer additional compile-time guarantees. We will explain the theory and practice of pluggable types. The material is relevant for researchers who wish to apply type theory, and for anyone who wishes to increase confidence in their code. After this session, you will have the knowledge to: analyze a problem to determine whether pluggable type-checking is appropriate; design a domain-specific type system; implement a simple type-checker; scale a simple type-checker to more sophisticated properties; and better appreciate both object-oriented types and flexible verification techniques. While the theory is general, our hands-on exercises will use a state-of-the-art system, the Checker Framework, that works for the Java language, scales to millions of lines of code, and is being adopted in the research and industrial communities. Such a framework enables researchers to easily evaluate their type systems in the context of a widely-used industrial language, Java. It enables non-researchers to verify their code in a lightweight way and to create custom analyses. And it enables students to better appreciate type system concepts.
Werner M. Dietl is a research associate at the Computer Science & Engineering department, University of Washington. He holds a PhD from ETH Zurich.
The Sketching Approach to Program Synthesis
The Sketch synthesis system allows programmers to write complex routines while leaving fragments of the code unspecified; the contents of these "holes" in the program is derived automatically by a synthesis engine. Sketching allows programmers to focus the power of the synthesizer on those portions of the code that are menial but easy to get wrong, reducing programmer effort without overwhelming the synthesizer. This tutorial offers a hands-on introduction to sketching as implemented in the SKETCH language and its accompanying synthesizer and show how the synthesizer can be used to derive the low-level details in a complex algorithm from a sketch that expresses its high-level structure. Basic sketching techniques will be illustrated through examples involving manipulations of linked data-structures, low-level bit-manipulation algorithms such as ciphers and error correction codes, and stencil kernels from scientific computing.
Time: 13:30–16:30, June 16
Room: Conference 3
Armando Solar-Lezama is an assistant professor in the electrical engineering and computer science department at MIT. His research interests lay in the area of computer supported programming; in particular, he is interested in program synthesis and program analysis tools to support programmer productivity.