Events

We are developing methods to improve human learning and performance on challenging perceptual categorization tasks, e.g., bird species identification, diagnostic dermatology. Our approach involves inferring psychological embeddings -- internal representations that individuals use to reason about a domain. Using predictive cognitive models that operate on an embedding, we perform surrogate-based optimization to determine efficient and effective means of training domain novices as well as amplifying an individual's capabilities at any stage of training. Our cognitive models leverage psychological theories of: similarity judgement and generalization, contextual and sequential effects in choice, attention shifts among embedding dimensions.  Rather than searching over all possible training policies, we focus our search on policy spaces motivated by the training literature, including manipulation of exemplar difficulty and the sequencing of category labels. We show that our models predict human behavior not only in the aggregate but at the level of individual learners and individual exemplars, and preliminary experiments show the benefits of surrogate-based optimization on learning and perform ance.

This work was performed in close collaboration with Brett Roads at University College London.

The ongoing trend to more heterogeneity forces us to rethink the design of systems. In this talk, I will present a new system design that considers heterogeneous compute units (general-purpose cores with different instruction sets, DSPs, FPGAs, fixed-function accelerators, etc.) from the beginning instead of as an afterthought. The goal is to treat all compute units (CUs) as first-class citizens, enabling 1) isolation and secure communication between all types of CUs, 2) a direct interaction of all CUs to remove the conventional CPU from the critical path, and 3) access to OS services such as file systems and network stacks for all CUs. To study this system design, I am using a hardware/software co-design based on two key ideas: 1) introduce a new hardware component next to each CU used by the OS as the CUs' common interface and 2) let the OS kernel control applications remotely from a different CU. In my talk, I will show how this approach allows to support arbitrary CUs as aforementioned first-class citizens, ranging from fixed-function accelerators to complex general-purpose cores.

Sound static analysis over-approximates the set of all possible executions in a given program in order to prove the absence of errors in the program. Due to this over-approximation, sound static analysis may generate spurious warnings about executions that are not wrong or even possible in the program. To become more practical, many static analyzers give up soundness by design. This means that they do not check certain properties or that they check them under certain unsound assumptions, such as the absence of arithmetic overflow. At the other end of the soundness spectrum, we have automatic test-case generation, which typically under-approximates the set of possible program executions. The goal of test-case generation is not to prove the absence of errors in the program but, rather, their existence. In this talk, I will present an overview of my research on combining these program analysis techniques to improve their overall automation, performance, and accuracy on real programs.

Asynchronous concurrency is a wide-spread way of writing programs that deal with many short tasks. It is the programming model behind event-driven concurrency, as exemplified by GUI applications, where the tasks correspond to event handlers, web applications based around JavaScript, the implementation of web browsers, but also of server-side software or operating systems.

This model is widely used because it provides the performance benefits of concurrency together with easier programming than multi-threading. While there is ample work on how to implement asynchronous programs, and significant work on testing and model checking, little research has been done on handling asynchronous programs that involve heap manipulation, nor on how to automatically optimize code for asynchronous concurrency.

This thesis addresses the question of how we can reason about asynchronous programs while considering the heap, and how to use this to optimize programs. The work is organized along the main questions:

(i) How can we reason about asynchronous programs, without ignoring the heap? (ii) How can we use such reasoning techniques to optimize programs involving asynchronous behavior? (iii) How can we transfer these reasoning and optimization techniques to other settings?

The unifying idea behind all the results in the thesis is the use of an appropriate model encompassing global state and a promise-based model of asynchronous concurrency. For the first question, we start from refinement type systems for sequential programs and extend them to perform precise resource-based reasoning in terms of heap contents, known outstanding tasks and promises. This extended type system is known as Asynchronous Liquid Separation Types, or ALST for short. We implement ALST in for OCaml programs using the Lwt library.

For the second question, we consider a family of possible program optimizations, described by a set of rewriting rules, the DWFM rules. The rewriting rules are type-driven: We only guarantee soundness for programs that are well-typed under ALST. We give a soundness proof based on a semantic interpretation of ALST that allows us to show behavior inclusion of pairs of programs.

For the third question, we address an optimization problem from industrial practice: Normally, JavaScript files that are referenced in an HTML file are be loaded synchronously, i.e., when a script tag is encountered, the browser must suspend parsing, then load and execute the script, and only after will it continue parsing HTML. But in practice, there are numerous JavaScript files for which asynchronous loading would be perfectly sound. First, we sketch a hypothetical optimization using the DWFM rules and a static analysis.

To actually implement the analysis, we modify the approach to use a dynamic analysis. This analysis, known as JSDefer, enables us to analyze real-world web pages, and provide experimental evidence for the efficiency of this transformation.

Next to performance, early power and energy estimation is a key challenge in the design of computer systems. Traditional simulation-based methods are often too slow while existing analytical models are often not sufficiently accurate. In this talk, I will present our work on bridging this gap by providing fast yet accurate alternatives for power and performance modeling of software and hardware. In the past, we have pioneered so-called source-level and host-compiled simulation techniques that are based on back-annotation of source code with semi-analytically estimated target metrics. More recently, we have studied alternative approaches in which we employ advanced machine learning techniques to synthesize analytical proxy models that can extract latent correlations and accurately predict time-varying power and performance of an application running on a target platform purely from data obtained while executing the application natively on a completely different host machine. We have developed such learning-based approaches for both hardware and software. On the hardware side, learning-based models for white-box and black-box hardware accelerators reach simulation speeds of 1 Mcycles/s at 97% accuracy. On the software side, depending on the granularity at which prediction is performed, cross-platform prediction can achieve more than 95% accuracy at more than 3 GIPS ofequivalent simulation throughput.

Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different verified compilers, it is important to develop a compositional notion of compiler correctness that is modular (preserved under linking), transitive (supports multi-pass compilation), and flexible (applicable to compilers that use different intermediate languages or employ non-standard program transformations). In this thesis, we formalize such a notion of correctness based on parametric simulations, thus developing a novel approach to compositional compiler verification.