Computer Augmented Program Engineering
Rajeev Alur, University of Pennsylvania,
In classical synthesis, an optimizing compiler transforms a high-level specification
into a lower-level implementation. In the more recent view,
the synthesis tool assists the programmer in various programming tasks by
integrating a variety of specifications using a mix of computational tools.
In this talk, we will review the recent progress in this emerging methodology,
called "computer augmented program engineering".
As a specific example, we will show how synthesizing the inverse of canonicalization
routines for data structures can be effectively used in revealing representation
dependence bugs in open source image-formatting software.
Data paths are easy to program and hard to specify. Concurrency requirements are hard to program but often
simple to specify. Thus, synthesis should be expected to be most beneficial in providing a concurrency framework
for an existing data path, where the data path should be abstracted heavily. We show one example of such an
application by extending the Bucrch/Dill paradigm for pipeline verification to pipeline synthesis, using uninterpreted
functions to abstract the data path.
A fundamental challenge in the synthesis of reactive systems is the
size of the search space: the number of candidate implementations of a
temporal specification is typically superexponential or even, for
distributed system architectures, infinite. In this talk, I will
review the bounded synthesis approach, which makes it possible to
traverse this immense search space in a structured manner. We fix a
bound on a system parameter, such as the number of states, and limit
the search to those implementations that fall below the bound. By
incrementally expanding the search to larger bounds, we maintain
completeness, while orienting the search towards the simplest (and
often most useful) solutions. The approach is applicable to the
entire range of synthesis problems, from individual processes to
synchronous and asynchronous distributed systems, to systems with
additional design constraints, such as symmetry. The talk is based on
joint work with Sven Schewe.
We generate concurrent garbage collectors by an automated refinement
process in Kestrel's Specware system. Starting from a formal specification of
requirements, we apply a sequence of transformations that generate
correct-by-construction refinements, resulting in the generation of efficient
To handle the specification and refinement of stateful/concurrent processes, we
developed techniques for a mixed algebraic/coalgebraic-style of
specification within the higher-order logic of Specware's MetaSlang language.
In addition to generic techniques for algorithm design, we developed new
coalgebraically-oriented techniques for invariant maintenance and refining the
types of observers. We generate refinements using purely functional calculation
based on the axioms and theorems of the domain specification. As a final step,
we transform the coalgebraic operators to stateful form and encapsulate the
top-level processes as threads.
Constraint based synthesis from sketches to storyboards and beyond
Synthesis approaches based on constraint solving offer some unique opportunities to experiment with more natural and more interactive forms of collaboration between
programmers and synthesis engines. This talk will describe how constraint based synthesis technology can enable a multi-modal programming model, where programmers can
combine insights in different forms ranging from low-level insights about the structure of the desired program to high-level graphical intuitions about how the program modifies its
state. The talk will elaborate on some of the technical challenges involved in making new forms of interaction possible, as well as some of the open problems behind this
We consider the problem of specifying combinations of concurrent data
structures with complex sharing in a manner that is both declarative
and results in provably correct code. In our approach, abstract
concurrent data types are specified using relational algebra and
functional dependencies. We describe (1) a language of decompositions that
permit the user to specify different combinations of data
structures to represent a relation, and (2) a language of lock placements
that allow the user to specify a range of conservative and speculative
locking strategies at a variety of granularities. We show that given a
decomposition and a lock placement, a compiler can generate
serializable transactions that operate over decomposed relations.
Finally we describe an autotuner that can simultaneously explore the
space of decompositions and lock placements to synthesize an optimal
combination of data structures and locks.
We argue for a programming model where automated reasoning plays a key
role during (1) interactive program development, (2) program
compilation, and (3) program execution. I will focus on data
manipulation (as opposed to control). I outline our results in
complete functional synthesis for integer arithmetic, which is a form
of program compilation based on decision procedures. For program
development, I sketch our ongoing work on resolution theorem proving
for interactive synthesis. For program execution, I touch upon the
UDITA system based on Java Pathfinder, and argue that programming
models related to constraint logic programming should play a bigger
role in mainstream software.
For more information, please see: http://lara.epfl.ch/w/impro