Reagents: expressing and composing fine-grained concurrency
Aaron Turon
Draft, to appear in PLDI 2012.
[ abstract
| pdf ]
Abstract:
Efficient communication and synchronization is crucial for fine-grained
parallelism. Libraries providing such features, while indispensable, are
difficult to write, and often cannot be tailored or composed to meet the needs
of specific users. We introduce reagents, a set of combinators for
concisely expressing concurrency algorithms. Reagents scale as well as their
hand-coded counterparts, while providing the composability existing libraries
lack.
Scalable Join Patterns
Aaron Turon, Claudio Russo
in OOPSLA 2011.
[ abstract
| pdf | Keynote slides | pdf slides ]
Abstract:
Coordination can destroy scalability in parallel programming. A
comprehensive library of synchronization primitives is therefore an
essential tool for exploiting parallelism. Unfortunately, such
primitives do not easily combine to yield scalable solutions to more
complex problems. We demonstrate that a concurrency library based on
Fournet and Gonthier's join calculus can provide declarative and
scalable coordination. By declarative, we mean that the
programmer needs only to write down the constraints of a coordination
problem, and the library will automatically derive a correct solution.
By scalable, we mean that the derived solutions deliver robust
performance both as the number of processors increases, and as the
complexity of the coordination problem grows. We validate our claims
empirically on seven coordination problems, comparing our generic
solution to specialized algorithms from the literature.
Modular rollback through free monads
Conor McBride, Olin Shivers, Aaron Turon
Continuation Workshop 2011.
[ Keynote slides | pdf slides ]
Modular rollback through control logging
A pair of twin functional pearls
Olin Shivers, Aaron Turon
in ICFP 2011.
[ abstract
| pdf | Keynote slides | pdf slides ]
Abstract:
We present a technique, based on the use of first-class control
operators, permitting programs to maintain and invoke rollback
logs for sequences of reversible effects. Our technique is modular,
in that it provides for complete separation between some library of
effectful operations, and a client, "driver" program which invokes
and rolls back sequences of these operations. In particular, the
checkpoint mechanism, which is entirely encapsulated within the
effect library, logs not only the library's effects, but also the client's
control state. Thus, logging and rollback can be almost completely
transparent to the client code.
This separation of concerns manifests itself nicely when we
must implement software with sophisticated error handling. We
illustrate with two examples that both exploit the architecture to
disentangle some core parsing task from its error management. The
parser code is completely separate from the error-correction code,
although the two components are deeply intertwined at run time.
A resource analysis of the pi-calculus
Aaron Turon, Mitchell Wand
In MFPS 2011.
[ abstract
| pdf | slides ]
Abstract:
We give a new treatment of the pi-calculus based on the semantic
theory of separation logic, continuing a research program begun by
Hoare and O'Hearn. Using a novel resource model that distinguishes
between public and private ownership, we refactor the operational
semantics so that sending, receiving, and allocating are commands that
influence owned resources. These ideas lead naturally to two
denotational models: one for safety and one for liveness. Both models
are fully abstract for the corresponding observables, but more
importantly both are very simple. The close connections with the
model theory of separation logic (in particular, with Brookes's action
trace model) give rise to a logic of processes and resources.
A separation logic for refining concurrent objects
Aaron Turon, Mitchell Wand
In POPL 2011.
[ abstract
| pdf ]
Abstract:
Fine-grained concurrent data structures are crucial for gaining performance from multiprocessing, but their design is a subtle art. Recent literature has made large strides in verifying these data structures, using either atomicity refinement or separation logic with rely-guarantee reasoning. In this paper we show how the ownership discipline of separation logic can be used to enable atomicity refinement, and we develop a new rely-guarantee method that is localized to the definition of a data structure. We present the first semantics of separation logic that is sensitive to atomicity, and show how to control this sensitivity through ownership. The result is a logic that enables compositional reasoning about atomicity and interference, even for programs that use fine-grained synchronization and dynamic memory allocation.
All-Termination(T)
Panagiotis Manolios, Aaron Turon
In TACAS, March 2009.
[ abstract
| pdf | slides ]
Abstract: We introduce the
All-Termination(T) problem: given a termination
solver T and a collection of functions F, find
every subset of the formal parameters to F whose
consideration is sufficient to show, using T,
that F terminates. An important and motivating
application is enhancing theorem proving systems by constructing
the set of strongest induction schemes for F,
modulo T. These schemes can be derived from the set of
termination cores, the minimal sets returned by
All-Termination(T), without any reference to an explicit
measure function. We study the All-Termination(T) problem
as applied to the size-change termination analysis (SCT), a
PSpace-complete problem that underlies many termination
solvers. Surprisingly, we show that All-Termination(SCT) is also
PSpace-complete, even though it substantially generalizes SCT
. We develop a practical algorithm for All- Termination(SCT),
and show experimentally that on the ACL2 regression suite (whose
size is over 100MB) our algorithm generates stronger induction
schemes on 90% of multiargument functions.
Regular expression derivatives reexamined
Scott Owens, John Reppy, Aaron Turon
In JFP, March 2009, vol 19, issue 02, pp. 173-190
[ abstract
| pdf ]
Abstract:
The derivative of a set of strings
S with respect to a
symbol
a is the set of strings generated by stripping the
leading
a from the strings in
S that start
with
a. For regular sets of strings, i.e., sets defined by
regular expressions (REs), the derivative is also a regular set. In a
1964 paper, Janusz Brzozowski presented an elegant method for directly
constructing a recognizer from a regular expression based on
regular-expression derivatives (Brzozowski, 1964). His approach is
elegant and easily supports extended regular expressions; i.e., REs
extended with Boolean operations such as complement. Unfortunately, RE
derivatives have been lost in the sands of time, and few computer
scientists are aware of them. Recently, we independently developed two
scanner generators, one for PLT Scheme and one for Standard ML, using
RE derivatives. Our experiences with this approach have been quite
positive: the implementation techniques are simple, the generated
scanners are usually optimal in size, and the extended RE language
allows for more compact scanner specifications. Of special interest
is that the implementation techniques are well-suited to functional
languages that provide good support for symbolic term manipulation
(e.g., inductive datatypes and pattern matching).
The purpose of this paper is largely educational. Our positive
experience with RE derivatives leads us to believe that they deserve
the attention of the current generation of functional programmers,
especially those implementing RE recognizers. We begin with a review
of background material in Section 2, introducing the notation and
definitions of regular expressions and their recognizers. Section 3
gives a fresh presentation of Brzozowski's work, including DFA
construction with RE derivatives. In addition to reexamining
Brzozowski's work, we also report on the key implementation challenges
we faced in Section 4, including new techniques for handling large
character sets such as Unicode (Unicode Consortium, 2003). Section 5
reports our experience in general and includes an empirical comparison
of the derivative-based scanner generator for SML/NJ with the more
traditional tool it replaces. We conclude with a review of related
work and a summary.
Metaprogramming with Traits
Aaron Turon
Honors thesis
[ abstract
| pdf ]
Abstract:
In many domains, classes have highly regular internal structure. For
example, so-called business objects often contain boilerplate code for
mapping database fields to class members. The boilerplate code must be
repeated per-field for every class, because existing mechanisms for
constructing classes do not provide a way to capture and reuse such
member-level structure. As a result, programmers often resort to ad
hoc code generation. This paper presents a lightweight mechanism for
specifying and reusing member-level structure in Java programs. The
proposal is based on a modest extension to traits that we have termed
trait-based metaprogramming. Although the semantics of the mechanism
are straightforward, its type theory is difficult to reconcile with
nominal subtyping. We achieve reconciliation by introducing a hybrid
structural/nominal type system that extends Java's type system. The
thesis includes a formal calculus defined by translation to
Featherweight Generic Java.
Metaprogramming with Traits
John Reppy, Aaron Turon
In ECOOP, July 2007.
[ abstract
| pdf ]
Abstract:
In many domains, classes have highly regular internal structure. For
example, so-called business objects often contain boilerplate code for
mapping database fields to class members. The boilerplate code must be
repeated per-field for every class, because existing mechanisms for
constructing classes do not provide a way to capture and reuse such
member-level structure. As a result, programmers often resort to ad
hoc code generation. This paper presents a lightweight mechanism for
specifying and reusing member-level structure in Java programs. The
proposal is based on a modest extension to traits that we have termed
trait-based metaprogramming. Although the semantics of the mechanism
are straightforward, its type theory is difficult to reconcile with
nominal subtyping. We achieve reconciliation by introducing a hybrid
structural/nominal type system that extends Java's type system. The
paper includes a formal calculus defined by translation to
Featherweight Generic Java.
A foundation for trait-based metaprogramming
John Reppy, Aaron Turon
In FOOL/WOOD, January 2006.
[ abstract
| pdf
| slides
| tech report ]
Abstract:
Schaerli et al. introduced traits as reusable units of behavior
independent of the inheritance hierarchy. Despite their relative
simplicity, traits offer a surprisingly rich calculus. Trait calculi
typically include operations for resolving conflicts when composing
two traits. In the existing work on traits, these operations (method
exclusion and aliasing) are shallow, i.e., they have no effect on the
body of the other methods in the trait. In this paper, we present a
new trait system, based on the Fisher-Reppy trait calculus, that adds
deep operations (method hiding and renaming) to support conflict
resolution. The proposed operations are deep in the sense that they
preserve any existing connections between the affected method and the
other methods of the trait. Our system uses Riecke-Stone dictionaries
to support these features. In addition, we define a more fine-grained
mechanism for tracking trait types than in previous systems. The
resulting calculus is more flexible and expressive, and can serve as
the foundation for trait-based metaprogramming, an idiom we introduce.
