Mobile web browsers and data visualization tools require a performance boost. Parallelization poses an opportunity because commodity computers feature fast and energy-efficient multicore, subword-SIMD, and GPU hardware. However, layout engines in both browsers and visualizations have resisted parallelization thus far. This thesis introduces techniques for parallel computing over trees and applies them to generating layout engines.

Our solution is twofold. First, we show how to specify layout languages in the attribute grammar model of constraints over trees. Second, we address outstanding challenges in parallelizing attribute grammars and computations over trees. Our resulting attribute grammar compiler generates layout engines for various layout languages and parallel hardware.

We provide several individual contributions:

* We specify the functional and parallel behavior of common layout language primitives.

* We present a language for scheduling parallel tree traversals and a static verifier for ensuring a schedule will solve the attributes of an arbitrary layout in a safe order.

* We introduce a parallel programming model where programmers may partially specify the parallel schedule and call an optimizing synthesizer to complete the schedule.

* We design a scheduling algorithm that is fast and modular over scheduling constructs.

* We optimize tree traversals for SIMD hardware by automatically staging dynamic memory allocation and clustering diverging tasks.

* We optimize parallel tree traversals for MIMD architectures through a load-balancing heuristic that approximates work stealing.

To evaluate our approach, we present two case studies. First, we generated the first parallel webpage layout engine that can for the most part render complex sites such as Wikipedia. Second, we generated interactive data visualizations that support up to 1,000,000 data points in real-time. Both case studies have been further validated industrially.

Sparse matrix formats encode very large numerical matrices with relatively few nonzeros. They are typically implemented using imperative languages, with emphasis on low-level optimization. Such implementations are far removed from the conceptual organization of the sparse format, which obscures the representation invariants. They are further specialized by hand for particular applications, machines and workloads. Consequently, they are difficult to write, maintain, and verify.

In this dissertation we present LL, a small functional language suitable for implementing operations on sparse matrices. LL supports nested list and pair types, which naturally represent compressed matrices. It provides a few built-in operators and has a unique compositional dataflow model. As a result, LL programs are often direct analogs of high-level dataflow diagrams. This correspondence is useful when implementing sparse format construction and algebraic kernels such as sparse matrix-vector multiplication (SpMV). Despite its limited expressiveness, LL can specify interesting operations on real-world sparse formats.

Next, we present a full functional verifier for sparse codes written in LL. We use a higher-order logic theorem prover, deploying standard simplification and introduction techniques. We use novel parametric predicates for tracking relationships between mathematical objects and their concrete representation. A simple heuristic tactic is used for automating proofs of different sparse formats. A qualitative analysis shows that our rule base exhibits good reusability and that the system easily extends to hierarchical formats.

Finally, we describe a compiler for LL programs that generates efficient, parallel C code. We systematically map high-level nested datatypes onto compact and efficient low-level types. This facilitates a straightforward, syntax-directed translation of code. Local optimizations improve the performance of nested loops and eliminate redundant memory accesses. A coarse-grained heuristic loop parallelization scheme produces data-parallel code for execution on shared-memory multicore machines. Empirical evaluation shows that the sequential throughput of generated SpMV code is within 0.94--1.09 of a handwritten implementation. Parallel execution is 1.82--1.98 faster on two cores and 2.44--3.59 faster on four cores.

Creating layouts for documents, GUIs, or data visualizations is a time-consuming and error-prone process. Non-programmers would like the customization and fine-grained control currently only possible with handwritten layout engines. Today, such engines are written by proficient programmers. This thesis introduces new techniques for specifying layout and generating efficient layout engines.

First, we present a new programming methodology which addresses the two central sources of bugs in layouts: ambiguities and conflicts. Then, we introduce a language of constraints in which we capture layout specifications formally. Finally, we show how to generate efficient layout engines automatically. We provide the following individual contributions:

1) The Programming by Manipulation (PBM) paradigm targeted at non-programmers to establish specifications in visual domains such as layout. We introduce a new type of user demonstration---manipulation---which is resistant to users' imprecisions inherent in drawing. Instead of sketching the desired layout, users steer the exploration of potential layouts by pointing out what they would like to change.

2) L³, a declarative language for layout specifications. L³ is based on non-directional constraints in which the flow of computation is completely abstracted away.

3) A synthesis procedure---grammar modular synthesis---capable of generating layout engines from L³ specifications. Our new algorithm scales to realistic layout specifications and produces generic engines supporting languages of documents.

To evaluate our work, we present two user studies showing not only that non-programmers can design interesting visualizations using PBM, but also that proficient programmers are more productive with PBM than with conventional constraint programming. We also compare the performance of our synthetized engines with state-of-the-art constraint solvers and show that our engines are up to two orders of magnitude faster.

We have promised social scientists a data revolution, but it has not arrived. What stands between practitioners and the data-driven insights they want? Acquiring the data. In particular, acquiring the social media, online forum, and other web data that was supposed to help them produce big, rich, ecologically valid datasets. Web automation programming is resistant to high-level abstractions, so end-user programmers end up stymied by the need to reverse engineer website internals—DOM, JavaScript, AJAX. Programming by Demonstration (PBD) offered one promising avenue towards democratizing web automation. Unfortunately, as the web matured, the programs became too complex for PBD tools to synthesize, and web PBD progress stalled.

This dissertation describes how I reformulated traditional web PBD around the insight that demonstrations are not always the easiest way for non-programmers to communicate their intent. By shifting from a purely Programming-By-Demonstration view to a Programming-By-X view that accepts a variety of user-friendly inputs, we can dramatically broaden the class of programs that come in reach for end-user programmers. Our Helena ecosystem combines (i) usable PBD-based program drafting tools, (ii) learnable programming languages, and (iii) novel programming environment interactions. The end result: non-coders write Helena programs in 10 minutes that can handle the complexity of modern webpages, while coders attempt the same task and time out in an hour. I conclude with a discussion of the abstraction-resistant domains that will fall next and how hybrid PL-HCI breakthroughs will vastly expand access to programming.

The usefulness of today's websites is limited by their form and ease of access. Even though the web contains an ever-expanding wealth of information, much of it exists in a form that is not directly useful. How can end-users access the web in a way that meets their needs?

We present record and replay (R+R) as a way to bridge the gap between a website's functionality and the end-user's goal. R+R leverages an interface the user knows and is stable --- that is, the webpage --- in order to automate repetitive tasks. A R+R system observes a user interacting with a website and produces a script which, when executed, repeats the original interaction. End-users can use R+R to automate a sequence of actions and programmers can use these recordings as an API to execute more complicated tasks. Unfortunately, as websites become more complex, R+R becomes increasingly difficult.

The challenge with modern websites is that a single demonstration of the interaction has limited information, making scripts fragile to changes in the website. For past R+R systems, this was less of an issue because of the static nature of websites. But as the web becomes more dynamic, it becomes difficult to produce a robust script that mimics the interactivity of the user and can adapt to changes on the page.

To solve this problem, we developed Ringer, a R+R system for the web. Ringer is built on three key abstractions --- actions, triggers, and elements. Ringer takes a user demonstration as input and synthesize a script that interacts with the page as a user would. To make Ringer scripts robust, we develop novel methods for web R+R. In particular, Ringer uses the following features:

Inferring triggers automatically which synchronize the script with the state of the webpage

Monitoring the replay execution to ensure actions faithfully mimic the user

Identifying elements on the replay-time page using a similarity metric

To evaluate our work, we run Ringer on a suite of real-world benchmarks by replaying interactions on Alexa-ranked websites. We compare Ringer against a current state-of-the-art replay tool and find that Ringer is able to replay all 29 benchmark interactions, compared to only 5 benchmarks for the previous approach. Additionally, our benchmarks show that a replayer needs to synchronize with the state of a webpage in order to replay correctly, motivating Ringer's use of triggers. We show that our trigger inference algorithm can synthesize sufficient synchronization, while also having the added benefit of speeding up the replay execution. Finally, we show that R+R is useful as a building block for end-user applications by building two such tools using Ringer. One allows end-users to scrape structured data from a website simply through demonstration. The other allows end-users to aggregate real-time data from various websites in the form of live tiles, by specifying the data they want on a website through demonstration.

Many code fragments are difficult to write. For example, using new and unfamiliar APIs can be a complex task with a steep learning curve. In addition, implementing a complex data structure requires discovering and understanding all of the corner cases. And more and more end users with little to no formal training are trying to write code, whether they be scientists writing simulations or kids writing mobile apps. For all of these reasons and more, programming is a difficult task, which leads to bugs and delays in software.

There are many tools that help programmers find code fragments involving complex APIs, but many are somewhat inexpressive and rely on static information. We present a new technique, which we call CodeHint, that generates and evaluates code at runtime and hence can synthesize real-world Java code that involves I/O, reflection, native calls, and other advanced language features. Our approach is dynamic (giving accurate results and allowing programmers to reason about concrete executions), easy-to-use (supporting a wide range of correctness specifications), and interactive (allowing users to refine the candidate code snippets). We evaluate CodeHint and show that its algorithms are efficient and that in two user studies it improves programmer productivity by more than a factor of two.

As the second contribution, programmers and end users often find it easy to explain an algorithm on a whiteboard or with pictures in a textbook but struggle to write the code correctly. We propose a new methodology that allows users to program by demonstrating how an algorithm proceeds on concrete inputs. To reduce the burden of these demonstrations on the user, we have developed pruning algorithms to remove ambiguities in the demonstrations and control flow inference algorithms to infer missing conditionals in demonstrations. These two techniques take advantage of the knowledge encoded in the user's partial correctness condition. We show that this approach is effective in practice by analyzing its performance on several common algorithms.

Today's cutting-edge applications, ranging from wearable devices and embedded medical sensors to high-performance data centers, put new demands on computer architectures. Those demands include more computation capability, a tight power budget, low latency, high throughput, and many more. To meet these requirements, specialized architectures with low energy consumption are becoming more prevalent. Many of these architectures trade off programmability features for gains in energy efficiency and performance. Hence, programmability challenges are inevitable as applications continue to evolve and make new demands on computing architectures.

I propose key principles for improving programmability intended for application writers as well as compiler developers and language designers. First, I address programmability issues by providing a programming model that hides low-level details but sufficiently exposes essential details for application writers to control. Second, to compile and optimize programs, I apply a new compilation methodology based on synthesis. Unlike a classical compiler's transformation, synthesis obtains a correct and optimal solution by searching for an optimal candidate that is semantically equivalent to a specification program. This search helps compilers generate efficient code without deriving a program via a sequence of transformations, which are challenging for compiler developers to design for new unconventional architectures.

In this thesis, I demonstrate the key principles in three projects: Chlorophyll, a language and compiler for low-power spatial architectures; Floem, a programming system for NIC-accelerated data center applications; and GreenThumb, a framework for building a superoptimizer (an assembly program optimizer based on synthesis).

Cell signaling controls basic cellular activities and coordinates cell actions, such as cell differentiation, division and growth. Consequently, errors in cellular signaling are responsible for diseases such as cancer, autoimmunity, and diabetes.

Executable biology describes mechanistic models of biological processes in a formal language that is dynamic and executable by a computer. Models in executable biology are able to capture complex behaviors of biological systems, such as time and concurrency. In addition, discrete modeling enables efficient algorithms to exhaustively explore spaces of models.

This thesis introduces tools to automatically infer executable models at different levels of abstraction from varied types of experimental data. In each case, we investigate identifiability of models when the provided experimental evidence and prior knowledge are varied. We make the following individual contributions:

* TPS:A framework for the automated inference of signed directed graphs modeling protein signaling networks, using time series data.

* SBL: A modeling language embedded in Scala for the automated synthesis of concurrent programs modeling cell fate decision using mutation experiments.

* Karme: A framework for investigating identifiability of asynchronous Boolean network models from single-cell gene expression data.

To evaluate our work, we apply our tools to in vivo, in vitro, and in silico data sets on cellular differentiation and protein signaling. We show that, through explicit characterization of ambiguities in input specifications, our approaches make unambiguous predictions supported by experimental evidence, and suggest new experiments that help disambiguate alternative explanations. Applied to epidermal growth factor signaling response data, TPS exhaustively explores all models that are consistent with the input, and makes predictions that are unambiguous across the model space. These predictions are supported by further experimental validation. Using SBL, we synthesize valid models of cell fate decision in C. elegans vulval precursor cells, fixing a bug in previous modeling. We show the existence of internally different models that are behaviorally equivalent under all mutation experiments. One of the inferred models expresses a previously unknown biological hypothesis. Finally, we use Karme to synthesize models of myeloid cell differentiation from simulated noisy single-cell data, and demonstrate that experimental design can reveal key genes in the system.