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.

Probabalistic NetKAT

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