These abstracts are for talks at this event.
NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.
Symmetric Multimodal Intelligent IDEs, Framework Adoption
Under two DARPA-funded seedlings, we are studying (1) Symmetric Multimodal Interactive Intelligent Development Environments, and (2) Community-Based Framework Adoption Support. Together, these two research efforts aim to produce software design and development environments where the computer-based agent is a collaborator rather than just a glorified text editor. These efforts bring together research in multimodal (specifically sketch + speech) user interfaces, mixed initiative (aka symmetric) HCI, software repository mining, and domain specific modeling. In this brief talk, I will give an overview of how the various research fields combine, and give a few storyboards demonstrating the envisioned (class of) systems.
The OO/XML mismatch: Is there a logic-based solution?
The open problem of the mismatch between object-oriented languages and XML has not been resolved. The sources of this problem are believed to be caused by the mismatch of the underlying type systems. But if fact, virtually all object-oriented interfaces to XML, as well as typed XML oriented languages, suffer from the inability to express constraints such as those available in XML Schema. These constraints include specification of the ranges of the number of occurrences, keys and referential integrity. The rules for type derivation by restriction in XML Schema are based on constraints and hence cannot be expressed in any of the well-known object-oriented interfaces to XML. Semantics of XML Schema groups also represent a major issue for these interfaces. Specification of those features is beyond the expressiveness of type systems of mainstream programming languages. Rather than relying on those type systems, we make a major shift by using constraint (assertion) languages, to specify features of XML Schema. This makes it possible to use a prover technology to verify constraints associated with XML Schema. More importantly, object-oriented programs processing XML data are now subject to these constraints expressed in an assertion language such as JML or Spec#. The underlying support of this object-oriented/XML technology is an extended virtual platform that manages object-oriented specifications of XML types and structures via reflection and allows a variety of static and dynamic verification techniques. The prover technology is based on PVS. Joint work with Mark Royer and David Briggs.
Resolving and Exploiting the k-CFA Paradox
David Van Horn
Low-level program analysis is a fundamental problem, taking the shape of ``flow analysis'' in functional languages and ``points-to'' analysis in imperative and object-oriented (OO) languages. Despite the similarities, the vocabulary and results in the two communities remain largely distinct, with limited cross-understanding. One of the few links is Shivers's kCFA work, which has advanced the concept of ``context-sensitive analysis'' and is widely known in both communities. Recent results, however, indicate that the relationship between the different incarnations of the analysis is not understood. Van Horn and Mairson proved kCFA for k >= 1 to be EXPTIME-complete, hence no polynomial algorithm exists. Yet there have been multiple polynomial formulations of context-sensitive points-to analyses in OO languages. Is functional kCFA a profoundly different analysis from OO kCFA? We resolve this paradox by showing that OO features conspire to make the exact same specification of kCFA be polynomial-time: objects and closures are subtly different, in a way that interacts crucially with context-sensitivity. This leads to a significant practical result: by emulating the OO approximation, we derive a polynomial hierarchy of context-sensitive CFAs for functional programs, simultaneously achieving high precision and efficiency. Joint work with Matt Might and Yannis Smaragdakis.
Traditional transactional memory systems suffer from overly conservative conflict detection, yielding so-called false conflicts, because they are based on fine-grained, low-level read/write conflicts. In response, the recent trend has been toward integrating various abstract data-type libraries using ad-hoc methods of high-level conflict detection. These proposals have led to improved performance but a lack of a unified theory has led to confusion in the literature. We clarify these recent proposals by defining a generalization of transactional memory in which a transaction consists of coarse-grained (abstract data-type) operations rather than simple memory read/write operations. We provide semantics for both pessimistic (e.g. transactional boosting) and optimistic (e.g. traditional TMs and recent alternatives) execution. We show that both are included in the standard atomic semantics, yet find that the choice imposes different requirements on the coarse-grained operations: pessimistic requires operations be left-movers, optimistic requires right-movers. Finally, we discuss how the semantics applies to numerous TM implementation details discussed widely in the literature. Joint work with Eric Koskinen and Matthew Parkinson.
Co-action is a new form of synchronous reactive programming. From the programmer's point of view, all actions take place simultaneously, and all interdependencies between actions are resolved instantaneously. Eliminating execution order avoids many of the complexities and pitfalls of imperative programming. What is novel is that co-action also supports an imperative model of state, with a heap of dynamically allocated objects pointing to one another, and assignment through pointer variables. Other forms of declarative programming either eliminate pointers or fall back to explicitly ordering execution. Co-action attempts to combine the best of both declarative and imperative programming. Declarative languages avoid pointers for good reason: to determine a correct execution order, data flow dependencies must be known, but pointer aliasing makes that undecidable at compile time. Co-action instead finds a correct execution order at run time by monitoring program execution and doing rollbacks to backtrack. The undecidable problem at compile time is converted into a search problem at run time. Co-actions are in a sense the dual of transactions, combining synchronous actions instead of isolating asynchronous actions, and parallelizing instead of serializing. To better study and communicate these ideas, I have defined a small formal calculus. The correctness criterion of an execution order is Coherence: every field is written at most once, and prior to any reads. The completeness theorem states that if a coherent execution order exists, then the co-action execution algorithm will find it. As of this writing I have been unable to prove completeness, and am seeking advice.
For more information on this project, see coherence-lang.org.
Does This Guarantee of Termination Make My Program Look Fat?
For the past couple of years I have been working with sub-Turing-complete programming languages, and especially Datalog. Datalog (with a minor extra assumption) captures the PTIME complexity class, meaning that every Datalog program executes in polynomial time, and every polynomial program is expressible in Datalog. This would seem like a great property for most practical purposes. Yet people's reaction is often to question its desirability. One line of attack includes an appeal to the "succinctness theorem", which people remember from grad school (especially if their grad school was in upstate NY). This well-known result in complexity theory states that one can always find programs that are unboundedly shorter when expressed on a Turing machine than in a language with guaranteed termination. The purpose of this talk is to dispel the myth that the succinctness theorem tells us anything about programming languages and real programs. First, the theorem itself is based on the busy beaver function and includes constants that are unimaginably large. Second, the succinctness theorem can only apply to programs that not only cannot themselves be expressed concisely in a terminating language, but not even their running time bound can be expressed as an acceptably succinct terminating function. In fact, the directly opposite result is practically relevant: For programs whose running time can be bounded by a succinct terminating function, a language with guaranteed termination can always express the program with at most a constant additive overhead, relative to the Turing machine representation. For instance, in the case of Datalog, consider a practically "large" polynomial bound, such as n^100. Any program with running time below n^100 can be expressed in Datalog just as succinctly as on a Turing machine except for a small constant. (Such constants matter little in practice because they can be pre-processed away.) This is joint work with Neil Immerman.
Can FPGAs provide significant performance boosts to garbage collection?
With the growing prevalence of multi-core and non-standard processing units, we ask the question of whether FPGA's can be used to greatly accelerate the problem of garbage collection in a standard desktop or server environment. FPGA's have enjoyed success in traditional streaming applications like signal processing but the non-locality of memory traversal in memory management makes this choice seem like an uncomfortable fit. In this talk, I will argue why FPGA's (particularly with front-side-bus connectivity) may be an attractive option for GC because of performance and power. I will present two preliminary algorithms that show great potential (> 100% speedup).
Contracts Made Manifest
Since Findler and Felleisen introduced higher-order contracts, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied to each value. These two approaches are commonly assumed to be equivalent---different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding. Our work extends that of Gronski and Flanagan, who defined a latent calculus lambda_C and a manifest calculus lambda_H , gave a translation phi from lambda_C to lambda_H , and proved that, if a lambda_C term reduces to a constant, then so does its phi-image. We enrich their account with a translation psi from lambda_H to lambda_C and prove an analogous theorem. We then generalize the whole framework to dependent contracts, whose predicates can mention free variables. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of lambda_H and two dialects ("lax" and "picky") of lambda_C, establish type soundness---a substantial result in itself, for lambda_H---and extend phi and psi accordingly. Surprisingly, the intuition that the latent and manifest systems are equivalent now breaks down: the extended translations preserve behavior in one direction but, in the other, sometimes yield terms that blame more. Joint work with Benjamin C. Pierce, Stephanie Weirich.
An Ode to Arrows
We study a number of embedded DSLs for autonomous ordinary differential equations (autonomous ODEs) in Haskell. A naive implementation based on the lazy tower of derivatives is straightforward but has serious time and space leaks due to the loss of sharing when handling cyclic and infinite data structures. In seeking a solution to fix this problem, we explore a number of DSLs ranging from shallow to deep embeddings, and middle-grounds in between. We advocate a solution based on arrows, an abstract notion of computation that offers both a succinct representation and an effective implementation. Arrows are ubiquitous in their combinator style that happens to capture both sharing and recursion elegantly. We further relate our arrow-based DSL to a more constrained form of arrows called causal commutative arrows, the normalization of which leads to a staged compilation technique improving ODE performance by orders of magnitude. Joint work with Paul Hudak.
|Last modified Monday, November 30th, 2009 9:56:17pm|