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.
Nominal Typing for Data Languages in QCert
Jerome Simeon (IBM Research)
Most data languages (e.g., SQL) are small functional languages with rich record operations and structural types. Using those in an object-oriented context can result in complex typing issues. We describe an approach to support nominal typing in data languages through a notion of brands. The resulting type system is simple enough for reasoning and flexible enough to capture many object- oriented idioms including classes and methods, object creation, casting, multiple inheritance and interfaces. We illustrate its use on miniOQL, a SQL- like language for objects and on NRA, a database algebra suitable for optimization. The type system has been formalized in Coq as part of QCert, a certified query compiler.
Joint work with Joshua Auerbach, Martin Hirzel, Louis Mandel, and Avraham Shinnar.
Accepting Blame for Safe Tunneled Exceptions
Yizhou Zhang (Cornell University)
Unhandled exceptions crash programs, so a compile-time check that exceptions are handled should in principle make software more reliable. But designers of some recent languages have argued that the benefits of statically checked exceptions are not worth the costs. We introduce a new statically checked exception mechanism that addresses the problems with existing checked-exception mechanisms. In particular, it interacts well with higher-order functions and other design patterns. The key insight is that whether an exception should be treated as exception is not a property of its type but rather of the context in which the exception propagates. Statically checked exceptions through code that is oblivious to their presence, but the type system nevertheless checks that these exceptions are handled. Further, exceptions can be tunneled without being accidentally caught, by expanding the space of exception identifiers to identify the exception-handling context. The resulting mechanism is expressive and syntactically light, and can be implemented efficiently. We demonstrate the expressiveness of the mechanism using significant codebases and evaluate its performance. We have implemented this new exception mechanism as part of the new Genus programming language, but the mechanism could equally well be applied to other programming languages.
Joint work with Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers.
Garbology: A Study of How Java Objects Die
Raoul L. Veroy (Tufts University)
How do objects die? In this paper, we present an analysis framework that can precisely characterize the ways in which Java programs dispose of objects. Our goal is to provide data that complements the existing object demographics literature, which is mostly focused on object allocation and lifetime characteristics. A more complete picture of object lifecycles is crucial to developing new garbage collection algorithms that can take advantage of application-specific information. We present a novel technique that uses trace-based simulation augmented with reference counting. Our analysis is able to identify groups of objects that die simultaneously and can compute the precise program point where these events occur. Furthermore, it can determine the specific program actions that cause objects to become unreachable. We classify object deaths in several different ways, and we present empirical results from running our analysis on the Dacapo, SPECjbb2005, and SPECjvm98 benchmarks using traces from the Elephant Tracks tracing tool.
Joint work with Samuel Z. Guyer.
Assessing the Limits of Program-Specific Garbage Collection Performance
Eliot Moss (University of Massachusetts Amherst)
We consider the ultimate limits of program-specific garbage collector performance for real programs. We first characterize the GC schedule optimization problem using Markov Decision Processes (MDPs). Based on this characterization, we develop a method of determining, for a given program run and heap size, an *optimal* schedule of collections for a non-generational collector. We further explore the limits of performance of a *generational* collector, where it is not feasible to search the space of schedules to prove optimality. Still, we show significant improvements with Least Squares Policy Iteration, a reinforcement learning technique for solving MDPs. We demonstrate that there is considerable promise to reduce garbage collection costs by developing program-specific collection policies.
Foundations of type-directed code inference: which types have a unique inhabitant?
Gabriel Scherer (Northeastern University)
Type information can be useful to guess some parts of the program that the users does not wish to write explicitly. This is the basic idea supporting coercions, Haskell's type classes, and Scala's implicits. I study a foundational question underlying this problem: when is it the case that a type has a unique inhabitant? In other words, when is the program fragment to guess *fully determined* from the type information? To answer this question, we take ideas from proof search and logic (in particular the notion of 'focusing'), and combine them with ideas about program equivalence in (pure) functional programming. In this talk, I would like to explain the motivation, and give an accessible introduction to 'focusing', a technique from logic used to answer questions from programming.
Multirole Logic as a Foundation for Global Coordination
Hanwen Wu (Boston University)
Session types are protocols describing valid communications among parties. Two- party sessions enjoy duality, in which one party's action is always the dual of the other party (e.g. send/receive, choose/offer). Correspondence to logics is being actively studied in which cut reduction is communication and the duality in classical linear logic captures duality in two-party sessions. However in multiparty sessions, duality no longer holds, and the two-premiss cut rule is insufficient to express multiparty communication. Several prior studies proposed multi-cut/coherent-cut as a generalization, with coherence as a side condition guarding cuts. Instead of resorting to classical logic, we propose a new form of logic, Multirole Logic, where propositions are not limited to only two interpretations (itself and its negation), but multiple interpretations annotated by a set of roles. Such generalization naturally gives rise to a (complete) cut rule for multiple propositions and a (partial) cut rule that leaves a residual proposition. And we proved the admissibility of cut rule, thus generalizing the celebrated results of Gentzen. We report that our Multirole Logic is much more general and it provides a foundation for global coordination, including but not limited to multiparty session types.
Joint work with Hongwei Xi.
PLANALYZER: Automatic Analysis of Online Field Experiments
Emma Tosch (University of Massachusetts Amherst)
Online experiments are widely used to evaluate changes to Internet services and inform design and engineering decisions. To manage the complexity of performing experiments at scale, large companies employ frameworks for designing, managing, and logging experimental data. While such systems can help prevent many pitfalls, the design, analysis, and verification of all but the most basic experiments require substantial domain expertise. This paper presents PLANALYZER, a static analysis tool that aids in the verification and analysis of online experiments. PLANALYZER incorporates the rules of causal inference to devise proper estimators for advanced experimental designs. PLANALYZER targets the PlanOut language, though its techniques would be applicable to similar experimental design languages. s static analyses identify whether a PlanOut program implements any valid experimental contrasts, and aids ana- lysts by enumerating these contrasts.
Steffen Smolka (Cornell University)
NetKAT is a language for modeling, programming, and reasoning about software-defined networks. It comes with a rich theory and automated tools including a sound and complete axiomatic system, a compiler, and a decision procedure for checking qualitative network properties automatically. A recent probabilistic extension of NetKAT holds great promise: it enables programming randomized routing algorithms, modeling probabilistc features such as link-failures, and reasoning about quantiative properties such as expected link congestion, probability of packet delivery, etc. While the denotational semantics of probabilistic NetKAT has been worked out, little is known about how to compute in this model algorithmically. There is no decision procedure or compiler. This work aims to develop the theoretic foundations to enable such tools: a theory of approximation and a coalgebraic (automata) theory for probabilistc NetKAT.
This is ongoing work with Nate Foster and Dexter Kozen at Cornell and with Alexandra Silva at University College London.
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Newman Wu (Yale University)
An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified general-purpose kernels, but it is unclear how to extend their work to verify the functional correctness of device drivers, due to the non-local effects of interrupts. In this paper, we present a novel compositional framework for building certified interruptible OS kernels with device drivers. We provide a general device model that can be instantiated with various hardware devices, and a realistic formal model of interrupts, which can be used to reason about interruptible code. We have realized this framework in the Coq proof assistant. To demonstrate the effectiveness of our new approach, we have successfully extended an existing verified non-interruptible kernel with our framework and turned it into an interruptible kernel with verified device drivers. To the best of our knowledge, this is the first verified interruptible operating system with device drivers.
Joint work with Hao Chen, Zhong Shao, Joshua Lockerman, and Ronghui Gu.
Using Anomaly Detection to Find Bugs in Control Software
Hu Huang (Tufts University)
Modern commercial aircraft are heavily dependent on large software systems for many of their essential functions. However, bugs may cause software failure and endanger the lives of passengers and crew. Software development processes in aviation emphasize near exhaustive testing but not all bugs can be found. Additionally, current bug detection methods are not suitable for bugs that appear during run-time as there exist complex relationships between program variables that are not detectable by assertions or simple invariants. In our work, we make use of a machine learning approach for detecting bugs at run-time. However, we depart from previous work by leveraging program slicing to obtain a set of variables for monitoring. This talk will be on preliminary work that we have done so far on this idea.
Adel: A New Way to Program Microcontrollers
Sam Guyer (Tufts University)
Cheap microcontrollers, such as the Arduino, have become wildly popular for embedded applications ranging from "smart homes" to wearable devices to electronic art. Unfortunately, programming these tiny microprocessors is surprisingly difficult. The central problem is that the applications often consist of logically asynchronous tasks -- for example, blink a light until a button is pushed -- but there is no support for concurrency (e.g., threads). Many of these microprocessors do not have the resources necessary to support an operating system of any kind, so composing multiple tasks requires programmers to implement a kind of ad hoc scheduler that greatly complicates the code. In this talk I will present a new "programming language", called Adel, for programming microcontrollers. Adel provides a limited form of concurrency based on coroutines and is cheap enough for use in even the most bare-bones systems. Adel is not a full programming language -- it is implemented entirely as a set of C macros and requires no changes to the existing Arduino tool chain. Most importantly, it provides compositionality: asynchronous tasks can be composed in a simple and intuitive way without compromising modularity and clarity.
|Last modified Friday, May 27th, 2016 7:37:53am|