It is my great pleasure to welcome you to the 43rd ACM Symposium on Principles of Programming Languages, POPL 2016. The conference is held in St. Petersburg, Florida, a location that follows the tradition of revisiting the east of the United States roughly every three years.
Computing has entered the era of uncertain data, in which hardware and software generate and reason about estimates. Applications use estimates from sensors, machine learning, big data, humans, and approximate hardware and software. Unfortunately, developers face pervasive correctness, programmability, and optimization problems due to estimates. Most programming languages unfortunately make these problems worse. We propose a new programming abstraction called Uncertain<T> embedded into languages, such as C#, C++, Java, Python, and JavaScript. Applications that consume estimates use familiar discrete operations for their estimates; overloaded conditional operators specify hypothesis tests and applications use them control false positives and negatives; and new compositional operators express domain knowledge. By carefully restricting the expressiveness, the runtime automatically implements correct statistical reasoning at conditionals, relieving developers of the need to implement or deeply understand statistics. We demonstrate substantial programmability, correctness, and efficiency benefits of this programming model for GPS sensor navigation, approximate computing, machine learning, and xBox.
@InProceedings{POPL16p1,
author = {Kathryn S. McKinley},
title = {Programming the World of Uncertain Things (Keynote)},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {1--2},
doi = {10.1145/2837614.2843895},
year = {2016},
}
Publisher's Version Article Search
Decision-making logic in hybrid systems is responsible for selecting
modes of operation for the underlying (continuous) control system,
reacting to external events and failures in the system, and insuring
that the overall control system is satisfying safety and performance
specifications. Tools from computer science, such as model-checking
and logic synthesis, combined with design patterns from feedback
control theory provide new approaches to solving these problems. A
major shift is the move from ``design then verify'' to ``specify then
synthesize'' approaches to controller design that allow simultaneous
synthesis of high-performance, robust control laws and
correct-by-construction decision-making logic.
@InProceedings{POPL16p3,
author = {Richard M. Murray},
title = {Synthesis of Reactive Controllers for Hybrid Systems (Keynote)},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {3--3},
doi = {10.1145/2837614.2843894},
year = {2016},
}
Publisher's Version Article Search
A confluence occurs when two rivers flow together; downstream the combined forces gather strength and propel their waters forward with increased vigor. In academic research, according to Varghese, a confluence occurs after some trigger, perhaps a discovery or a change in technology, and brings two previously separate branches of research together. In this talk, I will discuss confluences in programming languages research. Here, confluences often occur when basic research finds application in some important new domain. Two prime examples from my own career involve the confluence of research in type theory and systems security, triggered by new theoretical tools for reasoning about programming language safety, and the confluence of formal methods and networking, triggered by the rise of data centers. These experiences may shed light on what to teach our students and what is next for programming languages research.
@InProceedings{POPL16p4,
author = {David Walker},
title = {Confluences in Programming Languages Research (Keynote)},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {4--4},
doi = {10.1145/2837614.2843896},
year = {2016},
}
Publisher's Version Article Search
According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System F_omega, a strongly normalizing lambda-calculus. After a careful analysis of the classical theorem, we show that static type checking in F_omega can exclude the proof's diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F_omega, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.
@InProceedings{POPL16p5,
author = {Matt Brown and Jens Palsberg},
title = {Breaking through the Normalization Barrier: A Self-Interpreter for F-omega},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {5--17},
doi = {10.1145/2837614.2837623},
year = {2016},
}
Publisher's Version Article Search
We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.
@InProceedings{POPL16p18,
author = {Thorsten Altenkirch and Ambrus Kaposi},
title = {Type Theory in Type Theory using Quotient Inductive Types},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {18--29},
doi = {10.1145/2837614.2837638},
year = {2016},
}
Publisher's Version Article Search Info
Traversing an algebraic datatype by hand requires boilerplate code which duplicates the structure of the datatype. Datatype-generic programming (DGP) aims to eliminate such boilerplate code by decomposing algebraic datatypes into type constructor applications from which generic traversals can be synthesized. However, different traversals require different decompositions, which yield isomorphic but unequal types. This hinders the interoperability of different DGP techniques. In this paper, we propose Fωμ, an extension of the higher-order polymorphic lambda calculus Fω with records, variants, and equirecursive types. We prove the soundness of the type system, and show that type checking for first-order recursive types is decidable with a practical type checking algorithm. In our soundness proof we define type equality by interpreting types as infinitary λ-terms (in particular, Berarducci-trees). To decide type equality we β-normalize types, and then use an extension of equivalence checking for usual equirecursive types. Thanks to equirecursive types, new decompositions for a datatype can be added modularly and still interoperate with each other, allowing multiple DGP techniques to work together. We sketch how generic traversals can be synthesized, and apply these components to some examples. Since the set of datatype decomposition becomes extensible, System Fωμ enables using DGP techniques incrementally, instead of planning for them upfront or doing invasive refactoring.
@InProceedings{POPL16p30,
author = {Yufei Cai and Paolo G. Giarrusso and Klaus Ostermann},
title = {System F-omega with Equirecursive Types for Datatype-Generic Programming},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {30--43},
doi = {10.1145/2837614.2837660},
year = {2016},
}
Publisher's Version Article Search Info
We consider the Curry-Howard-Lambek correspondence for effectful computation and resource management, specifically proposing polarised calculi together with presheaf-enriched adjunction models as the starting point for a comprehensive semantic theory relating logical systems, typed calculi, and categorical models in this context. Our thesis is that the combination of effects and resources should be considered orthogonally. Model theoretically, this leads to an understanding of our categorical models from two complementary perspectives: (i) as a linearisation of CBPV (Call-by-Push-Value) adjunction models, and (ii) as an extension of linear/non-linear adjunction models with an adjoint resolution of computational effects. When the linear structure is cartesian and the resource structure is trivial we recover Levy’s notion of CBPV adjunction model, while when the effect structure is trivial we have Benton’s linear/non-linear adjunction models. Further instances of our model theory include the dialogue categories with a resource modality of Melliès and Tabareau, and the [E]EC ([Enriched] Effect Calculus) models of Egger, Møgelberg and Simpson. Our development substantiates the approach by providing a lifting theorem of linear models into cartesian ones. To each of our categorical models we systematically associate a typed term calculus, each of which corresponds to a variant of the sequent calculi LJ (Intuitionistic Logic) or ILL (Intuitionistic Linear Logic). The adjoint resolution of effects corresponds to polarisation whereby, syntactically, types locally determine a strict or lazy evaluation order and, semantically, the associativity of cuts is relaxed. In particular, our results show that polarisation provides a computational interpretation of CBPV in direct style. Further, we characterise depolarised models: those where the cut is associative, and where the evaluation order is unimportant. We explain possible advantages of this style of calculi for the operational semantics of effects.
@InProceedings{POPL16p44,
author = {Pierre-Louis Curien and Marcelo Fiore and Guillaume Munch-Maccagnoni},
title = {A Theory of Effects and Resources: Adjunction Models and Polarised Calculi},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {44--56},
doi = {10.1145/2837614.2837652},
year = {2016},
}
Publisher's Version Article Search
We present an automated approach to verifying arbitrary omega-regular
properties of higher-order functional programs. Previous automated
methods proposed for this class of programs could only handle safety
properties or termination, and our approach is the first to be able
to verify arbitrary omega-regular liveness properties.
Our approach is automata-theoretic, and extends our recent work on
binary-reachability-based approach to automated termination
verification of higher-order functional programs to fair termination
published in ESOP 2014. In that work, we have shown that checking
disjunctive well-foundedness of (the transitive closure of) the
``calling relation'' is sound and complete for termination. The
extension to fair termination is tricky, however, because the
straightforward extension that checks disjunctive well-foundedness of
the fair calling relation turns out to be unsound, as we shall show in
the paper. Roughly, our solution is to check fairness on the
transition relation instead of the calling relation, and propagate the
information to determine when it is necessary and sufficient to check
for disjunctive well-foundedness on the calling relation. We prove
that our approach is sound and complete. We have implemented
a prototype of our approach, and confirmed that it is able to
automatically verify liveness properties of some non-trivial
higher-order programs.
@InProceedings{POPL16p57,
author = {Akihiro Murase and Tachio Terauchi and Naoki Kobayashi and Ryosuke Sato and Hiroshi Unno},
title = {Temporal Verification of Higher-Order Functional Programs},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {57--68},
doi = {10.1145/2837614.2837667},
year = {2016},
}
Publisher's Version Article Search
On the surface, large data centers with about 100,000 stations and nearly a million routing rules are complex and hard to verify. However, these networks are highly regular by design; for example they employ fat tree topologies with backup routers interconnected by redundant patterns. To exploit these regularities, we introduce network transformations: given a reachability formula and a network, we transform the network into a simpler to verify network and a corresponding transformed formula, such that the original formula is valid in the network if and only if the transformed formula is valid in the transformed network. Our network transformations exploit network surgery (in which irrelevant or redundant sets of nodes, headers, ports, or rules are ``sliced'' away) and network symmetry (say between backup routers). The validity of these transformations is established using a formal theory of networks. In particular, using Van Benthem-Hennessy-Milner style bisimulation, we show that one can generally associate bisimulations to transformations connecting networks and formulas with their transforms. Our work is a development in an area of current wide interest: applying programming language techniques (in our case bisimulation and modal logic) to problems in switching networks. We provide experimental evidence that our network transformations can speed up by 65x the task of verifying the communication between all pairs of Virtual Machines in a large datacenter network with about 100,000 VMs. An all-pair reachability calculation, which formerly took 5.5 days, can be done in 2 hours, and can be easily parallelized to complete in
@InProceedings{POPL16p69,
author = {Gordon D. Plotkin and Nikolaj Bjørner and Nuno P. Lopes and Andrey Rybalchenko and George Varghese},
title = {Scaling Network Verification using Symmetry and Surgery},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {69--83},
doi = {10.1145/2837614.2837657},
year = {2016},
}
Publisher's Version Article Search
We investigate the *model checking* problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory state satisfies a given formula in this language, as arises e.g. in software testing or runtime verification. First, we show that the problem is *decidable*; specifically, we present a bottom-up fixed point algorithm that decides the problem and runs in exponential time in the size of the problem instance. Second, we show that, while model checking for the full language is EXPTIME-complete, the problem becomes NP-complete or PTIME-solvable when we impose natural syntactic restrictions on the schemata defining the inductive predicates. We additionally present NP and PTIME algorithms for these restricted fragments. Finally, we report on the experimental performance of our procedures on a variety of specifications extracted from programs, exercising multiple combinations of syntactic restrictions.
@InProceedings{POPL16p84,
author = {James Brotherston and Nikos Gorogiannis and Max Kanovich and Reuben Rowe},
title = {Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {84--96},
doi = {10.1145/2837614.2837621},
year = {2016},
}
Publisher's Version Article Search
Software applications run on a variety of platforms (filesystems, virtual slices, mobile hardware, etc.) that do not provide 100% uptime. As such, these applications may crash at any unfortunate moment losing volatile data and, when re-launched, they must be able to correctly recover from potentially inconsistent states left on persistent storage. From a verification perspective, crash recovery bugs can be particularly frustrating because, even when it has been formally proved for a program that it satisfies a property, the proof is foiled by these external events that crash and restart the program. In this paper we first provide a hierarchical formal model of what it means for a program to be crash recoverable. Our model captures the recoverability of many real world programs, including those in our evaluation which use sophisticated recovery algorithms such as shadow paging and write-ahead logging. Next, we introduce a novel technique capable of automatically proving that a program correctly recovers from a crash via a reduction to reachability. Our technique takes an input control-flow automaton and transforms it into an encoding that blends the capture of snapshots of pre-crash states into a symbolic search for a proof that recovery terminates and every recovered execution simulates some crash-free execution. Our encoding is designed to enable one to apply existing abstraction techniques in order to do the work that is necessary to prove recoverability. We have implemented our technique in a tool called Eleven82, capable of analyzing C programs to detect recoverability bugs or prove their absence. We have applied our tool to benchmark examples drawn from industrial file systems and databases, including GDBM, LevelDB, LMDB, PostgreSQL, SQLite, VMware and ZooKeeper. Within minutes, our tool is able to discover bugs or prove that these fragments are crash recoverable.
@InProceedings{POPL16p97,
author = {Eric Koskinen and Junfeng Yang},
title = {Reducing Crash Recoverability to Reachability},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {97--108},
doi = {10.1145/2837614.2837648},
year = {2016},
}
Publisher's Version Article Search
We propose a new optimization problem "Q-MaxSAT", an extension of the well-known Maximum Satisfiability or MaxSAT problem. In contrast to MaxSAT, which aims to find an assignment to all variables in the formula, Q-MaxSAT computes an assignment to a desired subset of variables (or queries) in the formula. Indeed, many problems in diverse domains such as program reasoning, information retrieval, and mathematical optimization can be naturally encoded as Q-MaxSAT instances. We describe an iterative algorithm for solving Q-MaxSAT. In each iteration, the algorithm solves a subproblem that is relevant to the queries, and applies a novel technique to check whether the partial assignment found is a solution to the Q-MaxSAT problem. If the check fails, the algorithm grows the subproblem with a new set of clauses identified as relevant to the queries. Our empirical evaluation shows that our Q-MaxSAT solver Pilot achieves significant improvements in runtime and memory consumption over conventional MaxSAT solvers on several Q-MaxSAT instances generated from real-world problems in program analysis and information retrieval.
@InProceedings{POPL16p109,
author = {Xin Zhang and Ravi Mangal and Aditya V. Nori and Mayur Naik},
title = {Query-Guided Maximum Satisfiability},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {109--122},
doi = {10.1145/2837614.2837658},
year = {2016},
}
Publisher's Version Article Search
We study the fundamental issue of decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of their combined theory, which is especially relevant when analysing security vulnerabilities of dynamic web pages in a more realistic browser model. On the one hand, word equations (string logic with concatenations) cannot precisely capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML mutations). On the other hand, transducers suffer from the reverse problem of being able to model sanitisation functions and browser transductions, but not string concatenations. Naively combining word equations and transducers easily leads to an undecidable logic. Our main contribution is to show that the "straight-line fragment" of the logic is decidable (complexity ranges from PSPACE to EXPSPACE). The fragment can express the program logics of straight-line string-manipulating programs with concatenations and transductions as atomic operations, which arise when performing bounded model checking or dynamic symbolic executions. We demonstrate that the logic can naturally express constraints required for analysing mutation XSS in web applications. Finally, the logic remains decidable in the presence of length, letter-counting, regular, indexOf, and disequality constraints.
@InProceedings{POPL16p123,
author = {Anthony W. Lin and Pablo Barceló},
title = {String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {123--136},
doi = {10.1145/2837614.2837641},
year = {2016},
}
Publisher's Version Article Search
Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes paradigm, they have become increasingly popular in computer science, with high-level languages and formal methods such as Petri nets, process algebra, and rule-based systems that are interpreted as ODEs. We consider the problem of comparing and minimizing ODEs automatically. Influenced by traditional approaches in the theory of programming, we propose differential equivalence relations. We study them for a basic intermediate language, for which we have decidability results, that can be targeted by a class of high-level specifications. An ODE implicitly represents an uncountable state space, hence reasoning techniques cannot be borrowed from established domains such as probabilistic programs with finite-state Markov chain semantics. We provide novel symbolic procedures to check an equivalence and compute the largest one via partition refinement algorithms that use satisfiability modulo theories. We illustrate the generality of our framework by showing that differential equivalences include (i) well-known notions for the minimization of continuous-time Markov chains (lumpability), (ii)~bisimulations for chemical reaction networks recently proposed by Cardelli et al., and (iii) behavioral relations for process algebra with ODE semantics. With a prototype implementation we are able to detect equivalences in biochemical models from the literature that cannot be reduced using competing automatic techniques.
@InProceedings{POPL16p137,
author = {Luca Cardelli and Mirco Tribastone and Max Tschaikowski and Andrea Vandin},
title = {Symbolic Computation of Differential Equivalences},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {137--150},
doi = {10.1145/2837614.2837649},
year = {2016},
}
Publisher's Version Article Search
We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.
@InProceedings{POPL16p151,
author = {Matthew Hague and Jonathan Kochems and C.-H. Luke Ong},
title = {Unboundedness and Downward Closures of Higher-Order Pushdown Automata},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {151--163},
doi = {10.1145/2837614.2837627},
year = {2016},
}
Publisher's Version Article Search Info
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to that of an attacker interacting with the program in the source language. Proving compiler full-abstraction is, however, rather complicated. A common proof technique is based on the back-translation of target-level program contexts to behaviourally-equivalent source-level contexts. However, constructing such a back-translation is problematic when the source language is not strong enough to embed an encoding of the target language. For instance, when compiling from the simply-typed λ-calculus (λτ) to the untyped λ-calculus (λu), the lack of recursive types in λτ prevents such a back-translation. We propose a general and elegant solution for this problem. The key insight is that it suffices to construct an approximate back-translation. The approximation is only accurate up to a certain number of steps and conservative beyond that, in the sense that the context generated by the back-translation may diverge when the original would not, but not vice versa. Based on this insight, we describe a general technique for proving compiler full-abstraction and demonstrate it on a compiler from λτ to λu . The proof uses asymmetric cross-language logical relations and makes innovative use of step-indexing to express the relation between a context and its approximate back-translation. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.
@InProceedings{POPL16p164,
author = {Dominique Devriese and Marco Patrignani and Frank Piessens},
title = {Fully-Abstract Compilation by Approximate Back-Translation},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {164--177},
doi = {10.1145/2837614.2837618},
year = {2016},
}
Publisher's Version Article Search
Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the correctness of separate compilation. Recently, a number of sophisticated techniques have been proposed for proving more flexible, compositional notions of compiler correctness, but these approaches tend to be quite heavyweight compared to the simple "closed simulations" used in verifying whole-program compilation. Applying such techniques to a compiler like CompCert, as Stewart et al. have done, involves major changes and extensions to its original verification. In this paper, we show that if we aim somewhat lower---to prove correctness of separate compilation, but only for a *single* compiler---we can drastically simplify the proof effort. Toward this end, we develop several lightweight techniques that recast the compositional verification problem in terms of whole-program compilation, thereby enabling us to largely reuse the closed-simulation proofs from existing compiler verifications. We demonstrate the effectiveness of these techniques by applying them to CompCert 2.4, converting its verification of whole-program compilation into a verification of separate compilation in less than two person-months. This conversion only required a small number of changes to the original proofs, and uncovered two compiler bugs along the way. The result is SepCompCert, the first verification of separate compilation for the full CompCert compiler.
@InProceedings{POPL16p178,
author = {Jeehoon Kang and Yoonseung Kim and Chung-Kil Hur and Derek Dreyer and Viktor Vafeiadis},
title = {Lightweight Verification of Separate Compilation},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {178--190},
doi = {10.1145/2837614.2837642},
year = {2016},
}
Publisher's Version Article Search Info
Reconstructing the meaning of a program from its binary executable is known as reverse engineering; it has a wide range of applications in software security, exposing piracy, legacy systems, etc. Since reversing is ultimately a search for meaning, there is much interest in inferring a type (a meaning) for the elements of a binary in a consistent way. Unfortunately existing approaches do not guarantee any semantic relevance for their reconstructed types. This paper presents a new and semantically-founded approach that provides strong guarantees for the reconstructed types. Key to our approach is the derivation of a witness program in a high-level language alongside the reconstructed types. This witness has the same semantics as the binary, is type correct by construction, and it induces a (justifiable) type assignment on the binary. Moreover, the approach effectively yields a type-directed decompiler. We formalise and implement the approach for reversing MinX, an abstraction of x86, to MinC, a type-safe dialect of C with recursive datatypes. Our evaluation compiles a range of textbook C algorithms to MinX and then recovers the original structures.
@InProceedings{POPL16p191,
author = {Ed Robbins and Andy King and Tom Schrijvers},
title = {From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {191--203},
doi = {10.1145/2837614.2837633},
year = {2016},
}
Publisher's Version Article Search
Syntactic language extensions can introduce new facilities into a programming language while requiring little implementation effort and modest changes to the compiler. It is typical to desugar language extensions in a distinguished compiler phase after parsing or type checking, not affecting any of the later compiler phases. If desugaring happens before type checking, the desugaring cannot depend on typing information and type errors are reported in terms of the generated code. If desugaring happens after type checking, the code generated by the desugaring is not type checked and may introduce vulnerabilities. Both options are undesirable. We propose a system for syntactic extensibility where desugaring happens after type checking and desugarings are guaranteed to only generate well-typed code. A major novelty of our work is that desugarings operate on typing derivations instead of plain syntax trees. This provides desugarings access to typing information and forms the basis for the soundness guarantee we provide, namely that a desugaring generates a valid typing derivation. We have implemented our system for syntactic extensibility in a language-independent fashion and instantiated it for a substantial subset of Java, including generics and inheritance. We provide a sound Java extension for Scala-like for-comprehensions.
@InProceedings{POPL16p204,
author = {Florian Lorenzen and Sebastian Erdweg},
title = {Sound Type-Dependent Syntactic Language Extension},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {204--216},
doi = {10.1145/2837614.2837644},
year = {2016},
}
Publisher's Version Article Search
Decidability and Complexity
Decidability of Inferring Inductive Invariants
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, and Mooly Sagiv (Tel Aviv University, Israel; University of Massachusetts at Amherst, USA; Academic College of Tel Aviv Yaffo, Israel)
Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant for the system. A key ingredient in this approach is coming up with the inductive invariant, which is known as invariant inference. This is a major difficulty, and it is often left for humans or addressed by sound but incomplete abstract interpretation. This paper is motivated by the problem of inductive invariants in shape analysis and in distributed protocols. This paper approaches the general problem of inferring first-order inductive invariants by restricting the language L of candidate invariants. Notice that the problem of invariant inference in a restricted language L differs from the safety problem, since a system may be safe and still not have any inductive invariant in L that proves safety. Clearly, if L is finite (and if testing an inductive invariant is decidable), then inferring invariants in L is decidable. This paper presents some interesting cases when inferring inductive invariants in L is decidable even when L is an infinite language of universal formulas. Decidability is obtained by restricting L and defining a suitable well-quasi-order on the state space. We also present some undecidability results that show that our restrictions are necessary. We further present a framework for systematically constructing infinite languages while keeping the invariant inference problem decidable. We illustrate our approach by showing the decidability of inferring invariants for programs manipulating linked-lists, and for distributed protocols.
@InProceedings{POPL16p217,
author = {Oded Padon and Neil Immerman and Sharon Shoham and Aleksandr Karbyshev and Mooly Sagiv},
title = {Decidability of Inferring Inductive Invariants},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {217--231},
doi = {10.1145/2837614.2837640},
year = {2016},
}
Publisher's Version Article Search
A program can benefit from improved cache block utilization when contemporaneously accessed data elements are placed in the same memory block. This can reduce the program's memory block working set and thereby, reduce the capacity miss rate. We formally define the problem of data packing for arbitrary number of blocks in the cache and packing factor (the number of data objects fitting in a cache block) and study how well the optimal solution can be approximated for two dual problems. On the one hand, we show that the cache hit maximization problem is approximable within a constant factor, for every fixed number of blocks in the cache. On the other hand, we show that unless P=NP, the cache miss minimization problem cannot be efficiently approximated.
@InProceedings{POPL16p232,
author = {Rahman Lavaee},
title = {The Hardness of Data Packing},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {232--242},
doi = {10.1145/2837614.2837669},
year = {2016},
}
Publisher's Version Article Search
In this paper, we analyze the complexity of functional programs written in the interaction-net computation model, an asynchronous, parallel and confluent model that generalizes linear-logic proof nets. Employing user-defined sized and scheduled types, we certify concrete time, space and space-time complexity bounds for both sequential and parallel reductions of interaction-net programs by suitably assigning complexity potentials to typed nodes. The relevance of this approach is illustrated on archetypal programming examples. The provided analysis is precise, compositional and is, in theory, not restricted to particular complexity classes.
@InProceedings{POPL16p243,
author = {Stéphane Gimenez and Georg Moser},
title = {The Complexity of Interaction},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {243--255},
doi = {10.1145/2837614.2837646},
year = {2016},
}
Publisher's Version Article Search
Language Design
Dependent Types and Multi-monadic Effects in F*
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin (Microsoft Research, USA; Inria, France; University of Maryland, USA; ENS, France; IMDEA Software Institute, Spain; Microsoft Research, UK)
We present a new, completely redesigned, version of F*, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. In support of these complementary roles, F* is a dependently typed, higher-order, call-by-value language with _primitive_ effects including state, exceptions, divergence and IO. Although primitive, programmers choose the granularity at which to specify effects by equipping each effect with a monadic, predicate transformer semantics. F* uses this to efficiently compute weakest preconditions and discharges the resulting proof obligations using a combination of SMT solving and manual proofs. Isolated from the effects, the core of F* is a language of pure functions used to write specifications and proof terms---its consistency is maintained by a semantic termination check based on a well-founded order. We evaluate our design on more than 55,000 lines of F* we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programming language, F* is programmed (but not verified) in F*, and bootstraps in both OCaml and F#. Our experience confirms F*'s pay-as-you-go cost model: writing idiomatic ML-like code with no finer specifications imposes no user burden. As a verification-oriented language, our most significant evaluation of F* is in verifying several key modules in an implementation of the TLS-1.2 protocol standard. For the modules we considered, we are able to prove more properties, with fewer annotations using F* than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss our use of F* in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to System F-omega and even micro-F*, a sizeable fragment of F* itself---these proofs make essential use of F*'s flexible combination of SMT automation and constructive proofs, enabling a tactic-free style of programming and proving at a relatively large scale.
@InProceedings{POPL16p256,
author = {Nikhil Swamy and Cătălin Hriţcu and Chantal Keller and Aseem Rastogi and Antoine Delignat-Lavaud and Simon Forest and Karthikeyan Bhargavan and Cédric Fournet and Pierre-Yves Strub and Markulf Kohlweiss and Jean-Karim Zinzindohoue and Santiago Zanella-Béguelin},
title = {Dependent Types and Multi-monadic Effects in F*},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {256--270},
doi = {10.1145/2837614.2837655},
year = {2016},
}
Publisher's Version Article Search Info
Fabular: Regression Formulas as Probabilistic Programming
Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio Russo, Adam Ścibior, and Marcin Szymczak (Uppsala University, Sweden; Microsoft Research, UK; University of Edinburgh, UK; Stanford University, USA; University of Cambridge, UK; MPI Tübingen, Germany)
Regression formulas are a domain-specific language adopted by several R packages for describing an important and useful class of statistical models: hierarchical linear regressions. Formulas are succinct, expressive, and clearly popular, so are they a useful addition to probabilistic programming languages? And what do they mean? We propose a core calculus of hierarchical linear regression, in which regression coefficients are themselves defined by nested regressions (unlike in R). We explain how our calculus captures the essence of the formula DSL found in R. We describe the design and implementation of Fabular, a version of the Tabular schema-driven probabilistic programming language, enriched with formulas based on our regression calculus. To the best of our knowledge, this is the first formal description of the core ideas of R's formula notation, the first development of a calculus of regression formulas, and the first demonstration of the benefits of composing regression formulas and latent variables in a probabilistic programming language.
@InProceedings{POPL16p271,
author = {Johannes Borgström and Andrew D. Gordon and Long Ouyang and Claudio Russo and Adam Ścibior and Marcin Szymczak},
title = {Fabular: Regression Formulas as Probabilistic Programming},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {271--283},
doi = {10.1145/2837614.2837653},
year = {2016},
}
Publisher's Version Article Search
We present and illustrate Kleenex, a language for expressing general nondeterministic finite transducers, and its novel compilation to streaming string transducers with essentially optimal streaming behavior, worst-case linear-time performance and sustained high throughput. Its underlying theory is based on transducer decomposition into oracle and action machines: the oracle machine performs streaming greedy disambiguation of the input; the action machine performs the output actions. In use cases Kleenex achieves consistently high throughput rates around the 1 Gbps range on stock hardware. It performs well, especially in complex use cases, in comparison to both specialized and related tools such as GNUawk, GNUsed, GNUgrep, RE2, Ragel and regular-expression libraries.
@InProceedings{POPL16p284,
author = {Bjørn Bugge Grathwohl and Fritz Henglein and Ulrik Terp Rasmussen and Kristoffer Aalund Søholm and Sebastian Paaske Tørholm},
title = {Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {284--297},
doi = {10.1145/2837614.2837647},
year = {2016},
}
Publisher's Version Article Search
We present Prophet, a novel patch generation system that works with a set of successful human patches obtained from open- source software repositories to learn a probabilistic, application-independent model of correct code. It generates a space of candidate patches, uses the model to rank the candidate patches in order of likely correctness, and validates the ranked patches against a suite of test cases to find correct patches. Experimental results show that, on a benchmark set of 69 real-world defects drawn from eight open-source projects, Prophet significantly outperforms the previous state-of-the-art patch generation system.
@InProceedings{POPL16p298,
author = {Fan Long and Martin Rinard},
title = {Automatic Patch Generation by Learning Correct Code},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {298--312},
doi = {10.1145/2837614.2837617},
year = {2016},
}
Publisher's Version Article Search
Reverse engineering is an important tool in mitigating vulnerabilities in binaries. As a lot of software is developed in object-oriented languages, reverse engineering of object-oriented code is of critical importance. One of the major hurdles in reverse engineering binaries compiled from object-oriented code is the use of dynamic dispatch. In the absence of debug information, any dynamic dispatch may seem to jump to many possible targets, posing a significant challenge to a reverse engineer trying to track the program flow. We present a novel technique that allows us to statically determine the likely targets of virtual function calls. Our technique uses object tracelets – statically constructed sequences of operations performed on an object – to capture potential runtime behaviors of the object. Our analysis automatically pre-labels some of the object tracelets by relying on instances where the type of an object is known. The resulting type-labeled tracelets are then used to train a statistical language model (SLM) for each type.We then use the resulting ensemble of SLMs over unlabeled tracelets to generate a ranking of their most likely types, from which we deduce the likely targets of dynamic dispatches.We have implemented our technique and evaluated it over real-world C++ binaries. Our evaluation shows that when there are multiple alternative targets, our approach can drastically reduce the number of targets that have to be considered by a reverse engineer.
@InProceedings{POPL16p313,
author = {Omer Katz and Ran El-Yaniv and Eran Yahav},
title = {Estimating Types in Binaries using Predictive Modeling},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {313--326},
doi = {10.1145/2837614.2837674},
year = {2016},
}
Publisher's Version Article Search
In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: 1. qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); 2. quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism.
@InProceedings{POPL16p327,
author = {Krishnendu Chatterjee and Hongfei Fu and Petr Novotný and Rouzbeh Hasheminezhad},
title = {Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {327--342},
doi = {10.1145/2837614.2837639},
year = {2016},
}
Publisher's Version Article Search
Cleaning spreadsheet data types is a common problem faced by millions of spreadsheet users. Data types such as date, time, name, and units are ubiquitous in spreadsheets, and cleaning transformations on these data types involve parsing and pretty printing their string representations. This presents many challenges to users because cleaning such data requires some background knowledge about the data itself and moreover this data is typically non-uniform, unstructured, and ambiguous. Spreadsheet systems and Programming Languages provide some UI-based and programmatic solutions for this problem but they are either insufficient for the user's needs or are beyond their expertise. In this paper, we present a programming by example methodology of cleaning data types that learns the desired transformation from a few input-output examples. We propose a domain specific language with probabilistic semantics that is parameterized with declarative data type definitions. The probabilistic semantics is based on three key aspects: (i) approximate predicate matching, (ii) joint learning of data type interpretation, and (iii) weighted branches. This probabilistic semantics enables the language to handle non-uniform, unstructured, and ambiguous data. We then present a synthesis algorithm that learns the desired program in this language from a set of input-output examples. We have implemented our algorithm as an Excel add-in and present its successful evaluation on 55 benchmark problems obtained from online help forums and Excel product team.
@InProceedings{POPL16p343,
author = {Rishabh Singh and Sumit Gulwani},
title = {Transforming Spreadsheet Data Types using Examples},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {343--356},
doi = {10.1145/2837614.2837668},
year = {2016},
}
Publisher's Version Article Search
Today’s Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requirements, and many practical systems provide causally consistent key-value stores. In this paper, we present a framework called Chapar for modular verification of causal consistency for replicated key-value store implementations and their client programs. Specifically, we formulate separate correctness conditions for key-value store implementations and for their clients. The interface between the two is a novel operational semantics for causal consistency. We have verified the causal consistency of two key-value store implementations from the literature using a novel proof technique. We have also implemented a simple automatic model checker for the correctness of client programs. The two independently verified results for the implementations and clients can be composed to conclude the correctness of any of the programs when executed with any of the implementations. We have developed and checked our framework in Coq, extracted it to OCaml, and built executable stores.
@InProceedings{POPL16p357,
author = {Mohsen Lesani and Christian J. Bell and Adam Chlipala},
title = {Chapar: Certified Causally Consistent Distributed Key-Value Stores},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {357--370},
doi = {10.1145/2837614.2837622},
year = {2016},
}
Publisher's Version Article Search
Large-scale distributed systems often rely on replicated databases that allow a
programmer to request different data consistency guarantees for different
operations, and thereby control their performance. Using such databases is far
from trivial: requesting stronger consistency in too many places may hurt
performance, and requesting it in too few places may violate correctness. To
help programmers in this task, we propose the first proof rule for establishing
that a particular choice of consistency guarantees for various operations on a
replicated database is enough to ensure the preservation of a given data
integrity invariant. Our rule is modular: it allows reasoning about the
behaviour of every operation separately under some assumption on the behaviour
of other operations. This leads to simple reasoning, which we have automated in
an SMT-based tool. We present a nontrivial proof of soundness of our rule and
illustrate its use on several examples.
@InProceedings{POPL16p371,
author = {Alexey Gotsman and Hongseok Yang and Carla Ferreira and Mahsa Najafzadeh and Marc Shapiro},
title = {'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {371--384},
doi = {10.1145/2837614.2837625},
year = {2016},
}
Publisher's Version Article Search
Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on deadlock-freedom and starvation-freedom, progress properties of blocking objects. These properties are more challenging to verify than lock-freedom because they allow the progress of one thread to depend on the progress of another, assuming fair scheduling.
We propose LiLi, a new rely-guarantee style program logic for verifying linearizability and progress together for concurrent objects under fair scheduling. The rely-guarantee style logic unifies thread-modular reasoning about both starvation-freedom and deadlock-freedom in one framework. It also establishes progress-aware abstraction for concurrent objects, which can be applied when verifying safety and liveness of client code. We have successfully applied the logic to verify starvation-freedom or deadlock-freedom of representative algorithms such as ticket locks, queue locks, lock-coupling lists, optimistic lists and lazy lists.
@InProceedings{POPL16p385,
author = {Hongjin Liang and Xinyu Feng},
title = {A Program Logic for Concurrent Objects under Fair Scheduling},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {385--399},
doi = {10.1145/2837614.2837635},
year = {2016},
}
Publisher's Version Article Search
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSync, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSync that efficiently executes on asynchronous networks. We formalise the relation between the runtime system and PSync in terms of observational refinement. The high-level lockstep abstraction introduced by PSync simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSync in the Scala programming language with a runtime system for partially synchronous networks. We show the applicability of PSync by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSync against implementations in other languages in terms of code size, runtime efficiency, and verification.
@InProceedings{POPL16p400,
author = {Cezara Drăgoi and Thomas A. Henzinger and Damien Zufferey},
title = {PSync: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {400--415},
doi = {10.1145/2837614.2837650},
year = {2016},
}
Publisher's Version Article Search
We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our approach is that it can detect a wide range of runtime errors that are missed by previous approaches. Our method is based on the idea to represent type refinements in pattern-matching branches by choice types, which facilitate a separation of the typing and reconciliation phases and thus support case expressions. This idea is formalized in a type system, which is both sound and a conservative extension of the classical Hindley-Milner system. We present the results of an empirical evaluation that compares our algorithm with previous approaches.
@InProceedings{POPL16p416,
author = {Sheng Chen and Martin Erwig},
title = {Principal Type Inference for GADTs},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {416--428},
doi = {10.1145/2837614.2837665},
year = {2016},
}
Publisher's Version Article Search
Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the type safety proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not resort to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof reduction. To illustrate the approach, we develop a novel gradually-typed counterpart for a language with record subtyping. Gradual languages designed with the AGT approach satisfy by construction the refined criteria for gradual typing set forth by Siek and colleagues.
@InProceedings{POPL16p429,
author = {Ronald Garcia and Alison M. Clark and Éric Tanter},
title = {Abstracting Gradual Typing},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {429--442},
doi = {10.1145/2837614.2837670},
year = {2016},
}
Publisher's Version Article Search
Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.
@InProceedings{POPL16p443,
author = {Matteo Cimini and Jeremy G. Siek},
title = {The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {443--455},
doi = {10.1145/2837614.2837632},
year = {2016},
}
Publisher's Version Article Search
Is Sound Gradual Typing Dead?
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen (Northeastern University, USA)
Programmers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, researchers have explored the idea of gradually-typed programming languages which allow the incremental addition of type annotations to software written in one of these untyped languages. Some of these new, hybrid languages insert run-time checks at the boundary between typed and untyped code to establish type soundness for the overall system. With sound gradual typing, programmers can rely on the language implementation to provide meaningful error messages when type invariants are violated. While most research on sound gradual typing remains theoretical, the few emerging implementations suffer from performance overheads due to these checks. None of the publications on this topic comes with a comprehensive performance evaluation. Worse, a few report disastrous numbers. In response, this paper proposes a method for evaluating the performance of gradually-typed programming languages. The method hinges on exploring the space of partial conversions from untyped to typed. For each benchmark, the performance of the different versions is reported in a synthetic metric that associates runtime overhead to conversion effort. The paper reports on the results of applying the method to Typed Racket, a mature implementation of sound gradual typing, using a suite of real-world programs of various sizes and complexities. Based on these results the paper concludes that, given the current state of implementation technologies, sound gradual typing faces significant challenges. Conversely, it raises the question of how implementations could reduce the overheads associated with soundness and how tools could be used to steer programmers clear from pathological cases.
@InProceedings{POPL16p456,
author = {Asumu Takikawa and Daniel Feltey and Ben Greenman and Max S. New and Jan Vitek and Matthias Felleisen},
title = {Is Sound Gradual Typing Dead?},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {456--468},
doi = {10.1145/2837614.2837630},
year = {2016},
}
Publisher's Version Article Search Artifacts Available
Static analysis has been successfully used in many areas, from verifying mission-critical software to malware detection. Unfortunately, static analysis often produces false positives, which require significant manual effort to resolve. In this paper, we show how to overlay a probabilistic model, trained using domain knowledge, on top of static analysis results, in order to triage static analysis results. We apply this idea to analyzing mobile applications. Android application components can communicate with each other, both within single applications and between different applications. Unfortunately, techniques to statically infer Inter-Component Communication (ICC) yield many potential inter-component and inter-application links, most of which are false positives. At large scales, scrutinizing all potential links is simply not feasible. We therefore overlay a probabilistic model of ICC on top of static analysis results. Since computing the inter-component links is a prerequisite to inter-component analysis, we introduce a formalism for inferring ICC links based on set constraints. We design an efficient algorithm for performing link resolution. We compute all potential links in a corpus of 11,267 applications in 30 minutes and triage them using our probabilistic approach. We find that over 95.1% of all 636 million potential links are associated with probability values below 0.01 and are thus likely unfeasible links. Thus, it is possible to consider only a small subset of all links without significant loss of information. This work is the first significant step in making static inter-application analysis more tractable, even at large scales.
@InProceedings{POPL16p469,
author = {Damien Octeau and Somesh Jha and Matthew Dering and Patrick McDaniel and Alexandre Bartel and Li Li and Jacques Klein and Yves Le Traon},
title = {Combining Static Analysis with Probabilistic Models to Enable Market-Scale Android Inter-component Analysis},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {469--484},
doi = {10.1145/2837614.2837661},
year = {2016},
}
Publisher's Version Article Search
The core challenge in designing an effective static program analysis is to find a good program abstraction -- one that retains only details relevant to a given query. In this paper, we present a new approach for automatically finding such an abstraction. Our approach uses a pessimistic strategy, which can optionally use guidance from a probabilistic model. Our approach applies to parametric static analyses implemented in Datalog, and is based on counterexample-guided abstraction refinement. For each untried abstraction, our probabilistic model provides a probability of success, while the size of the abstraction provides an estimate of its cost in terms of analysis time. Combining these two metrics, probability and cost, our refinement algorithm picks an optimal abstraction. Our probabilistic model is a variant of the Erdos--Renyi random graph model, and it is tunable by what we call hyperparameters. We present a method to learn good values for these hyperparameters, by observing past runs of the analysis on an existing codebase. We evaluate our approach on an object sensitive pointer analysis for Java programs, with two client analyses (PolySite and Downcast).
@InProceedings{POPL16p485,
author = {Radu Grigore and Hongseok Yang},
title = {Abstraction Refinement Guided by a Learnt Probabilistic Model},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {485--498},
doi = {10.1145/2837614.2837663},
year = {2016},
}
Publisher's Version Article Search Info
Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first learning algorithms in this model with implication counter-examples that are based on machine learning techniques. In particular, we extend classical decision-tree learning algorithms in machine learning to handle implication samples, building new scalable ways to construct small decision trees using statistical measures. We also develop a decision-tree learning algorithm in this model that is guaranteed to converge to the right concept (invariant) if one exists. We implement the learners and an appropriate teacher, and show that the resulting invariant synthesis is efficient and convergent for a large suite of programs.
@InProceedings{POPL16p499,
author = {Pranav Garg and Daniel Neider and P. Madhusudan and Dan Roth},
title = {Learning Invariants using Decision Trees and Implication Counterexamples},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {499--512},
doi = {10.1145/2837614.2837664},
year = {2016},
}
Publisher's Version Article Search Artifacts Available
Formal specification is a vital ingredient to scalable verification of software systems. In the case of efficient implementations of concurrent objects like atomic registers, queues, and locks, symbolic formal representations of their abstract data types (ADTs) enable efficient modular reasoning, decoupling clients from implementations. Writing adequate formal specifications, however, is a complex task requiring rare expertise. In practice, programmers write reference implementations as informal specifications. In this work we demonstrate that effective symbolic ADT representations can be automatically generated from the executions of reference implementations. Our approach exploits two key features of naturally-occurring ADTs: violations can be decomposed into a small set of representative patterns, and these patterns manifest in executions with few operations. By identifying certain algebraic properties of naturally-occurring ADTs, and exhaustively sampling executions up to a small number of operations, we generate concise symbolic ADT representations which are complete in practice, enabling the application of efficient symbolic verification algorithms without the burden of manual specification. Furthermore, the concise ADT violation patterns we generate are human-readable, and can serve as useful, formal documentation.
@InProceedings{POPL16p513,
author = {Michael Emmi and Constantin Enea},
title = {Symbolic Abstract Data Type Inference},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {513--525},
doi = {10.1145/2837614.2837645},
year = {2016},
}
Publisher's Version Article Search
The polyhedral model provides an expressive intermediate representation that is convenient for the analysis and subsequent transformation of affine loop nests. Several heuristics exist for achieving complex program transformations in this model. However, there is also considerable scope to utilize this model to tackle the problem of automatic memory footprint optimization. In this paper, we present a new automatic storage optimization technique which can be used to achieve both intra-array as well as inter-array storage reuse with a pre-determined schedule for the computation. Our approach works by finding statement-wise storage partitioning hyperplanes that partition a unified global array space so that values with overlapping live ranges are not mapped to the same partition. Our heuristic is driven by a fourfold objective function which not only minimizes the dimensionality and storage requirements of arrays required for each high-level statement, but also maximizes inter-statement storage reuse. The storage mappings obtained using our heuristic can be asymptotically better than those obtained by any existing technique. We implement our technique and demonstrate its practical impact by evaluating its effectiveness on several benchmarks chosen from the domains of image processing, stencil computations, and high-performance computing.
@InProceedings{POPL16p526,
author = {Somashekaracharya G. Bhaskaracharya and Uday Bondhugula and Albert Cohen},
title = {SMO: An Integrated Approach to Intra-array and Inter-array Storage Optimization},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {526--538},
doi = {10.1145/2837614.2837636},
year = {2016},
}
Publisher's Version Article Search
High-level compiler transformations, especially loop transformations, are widely recognized as critical optimizations to restructure programs to improve data locality and expose parallelism. Guaranteeing the correctness of program transformations is essential, and to date three main approaches have been developed: proof of equivalence of affine programs, matching the execution traces of programs, and checking bit-by-bit equivalence of program outputs. Each technique suffers from limitations in the kind of transformations supported, space complexity, or the sensitivity to the testing dataset. In this paper, we take a novel approach that addresses all three limitations to provide an automatic bug checker to verify any iteration reordering transformations on affine programs, including non-affine transformations, with space consumption proportional to the original program data and robust to arbitrary datasets of a given size. We achieve this by exploiting the structure of affine program control- and data-flow to generate at compile-time lightweight checker code to be executed within the transformed program. Experimental results assess the correctness and effectiveness of our method and its increased coverage over previous approaches.
@InProceedings{POPL16p539,
author = {Wenlei Bao and Sriram Krishnamoorthy and Louis-Noël Pouchet and Fabrice Rastello and P. Sadayappan},
title = {PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {539--554},
doi = {10.1145/2837614.2837656},
year = {2016},
}
Publisher's Version Article Search
Floating-point numbers are an essential part of modern software, recently gaining particular prominence on the web as the exclusive numeric format of Javascript. To use floating-point numbers, we require a way to convert binary machine representations into human readable decimal outputs. Existing conversion algorithms make trade-offs between completeness and performance. The classic Dragon4 algorithm by Steele and White and its later refinements achieve completeness --- i.e. produce correct and optimal outputs on all inputs --- by using arbitrary precision integer (bignum) arithmetic which leads to a high performance cost. On the other hand, the recent Grisu3 algorithm by Loitsch shows how to recover performance by using native integer arithmetic but sacrifices optimality for 0.5% of all inputs. We present Errol, a new complete algorithm that is guaranteed to produce correct and optimal results for all inputs while simultaneously being 2x faster than the incomplete Grisu3 and 4x faster than previous complete methods.
@InProceedings{POPL16p555,
author = {Marc Andrysco and Ranjit Jhala and Sorin Lerner},
title = {Printing Floating-Point Numbers: A Faster, Always Correct Method},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {555--567},
doi = {10.1145/2837614.2837654},
year = {2016},
}
Publisher's Version Article Search
Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the lambda-calculus and its variants, the latter for the pi-calculus. In this paper we explore their relative expressive power. Firstly, we give an embedding from PCF, augmented with a parameterised effect system, into a session-typed pi-calculus (session calculus), showing that session types are powerful enough to express effects. Secondly, we give a reverse embedding, from the session calculus back into PCF, by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result. We also discuss various extensions to our embeddings.
@InProceedings{POPL16p568,
author = {Dominic Orchard and Nobuko Yoshida},
title = {Effects as Sessions, Sessions as Effects},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {568--581},
doi = {10.1145/2837614.2837634},
year = {2016},
}
Publisher's Version Article Search Info
Session types provide a means to prescribe the communication behavior between concurrent message-passing processes. However, in a distributed setting, some processes may be written in languages that do not support static typing of sessions or may be compromised by a malicious intruder, violating invariants of the session types. In such a setting, dynamically monitoring communication between processes becomes a necessity for identifying undesirable actions. In this paper, we show how to dynamically monitor communication to enforce adherence to session types in a higher-order setting. We present a system of blame assignment in the case when the monitor detects an undesirable action and an alarm is raised. We prove that dynamic monitoring does not change system behavior for welltyped processes, and that one of an indicated set of possible culprits must have been compromised in case of an alarm.
@InProceedings{POPL16p582,
author = {Limin Jia and Hannah Gommerstadt and Frank Pfenning},
title = {Monitors and Blame Assignment for Higher-Order Session Types},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {582--594},
doi = {10.1145/2837614.2837662},
year = {2016},
}
Publisher's Version Article Search
Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ- calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as ‘up-to techniques’, are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.
@InProceedings{POPL16p595,
author = {Davide Sangiorgi and Valeria Vignudelli},
title = {Environmental Bisimulations for Probabilistic Higher-Order Languages},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {595--607},
doi = {10.1145/2837614.2837651},
year = {2016},
}
Publisher's Version Article Search
In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware. Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor's architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition. This means it can be discussed in detail with ARM architects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t.~the first. The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model. We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct representation of the ARM reference manual instruction descriptions. We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables. We prove correctness of some optimisations needed for tool performance. We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single- instruction tests and concurrent litmus tests.
@InProceedings{POPL16p608,
author = {Shaked Flur and Kathryn E. Gray and Christopher Pulte and Susmit Sarkar and Ali Sezgin and Luc Maranget and Will Deacon and Peter Sewell},
title = {Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {608--621},
doi = {10.1145/2837614.2837615},
year = {2016},
}
Publisher's Version Article Search Info
Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all common optimisations without also admitting undesired behaviour. Especially problematic are the ``thin-air'' examples involving high-performance concurrent accesses, such as C/C++11 relaxed atomics. The C/C++11 model is in a per-candidate-execution style, and previous work has identified a tension between that and the fact that compiler optimisations do not operate over single candidate executions in isolation; rather, they operate over syntactic representations that represent all executions. In this paper we propose a novel approach that circumvents this difficulty. We define a concurrency semantics for a core calculus, including relaxed-atomic and non-atomic accesses, and locks, that admits a wide range of optimisation while still forbidding the classic thin-air examples. It also addresses other problems relating to undefined behaviour. The basic idea is to use an event-structure representation of the current state of each thread, capturing all of its potential executions, and to permit interleaving of execution and transformation steps over that to reflect optimisation (possibly dynamic) of the code. These are combined with a non-multi-copy-atomic storage subsystem, to reflect common hardware behaviour. The semantics is defined in a mechanised and executable form, and designed to be implementable above current relaxed hardware and strong enough to support the programming idioms that C/C++11 does for this fragment. It offers a potential way forward for concurrent programming language semantics, beyond the current C/C++11 and Java models.
@InProceedings{POPL16p622,
author = {Jean Pichon-Pharabod and Peter Sewell},
title = {A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {622--633},
doi = {10.1145/2837614.2837616},
year = {2016},
}
Publisher's Version Article Search Info
Despite the conceptual simplicity of sequential consistency (SC), the semantics of SC atomic operations and fences in the C11 and OpenCL memory models is subtle, leading to convoluted prose descriptions that translate to complex axiomatic formalisations. We conduct an overhaul of SC atomics in C11, reducing the associated axioms in both number and complexity. A consequence of our simplification is that the SC operations in an execution no longer need to be totally ordered. This relaxation enables, for the first time, efficient and exhaustive simulation of litmus tests that use SC atomics. We extend our improved C11 model to obtain the first rigorous memory model formalisation for OpenCL (which extends C11 with support for heterogeneous many-core programming). In the OpenCL setting, we refine the SC axioms still further to give a sensible semantics to SC operations that employ a ‘memory scope’ to restrict their visibility to specific threads. Our overhaul requires slight strengthenings of both the C11 and the OpenCL memory models, causing some behaviours to become disallowed. We argue that these strengthenings are natural, and that all of the formalised C11 and OpenCL compilation schemes of which we are aware (Power and x86 CPUs for C11, AMD GPUs for OpenCL) remain valid in our revised models. Using the HERD memory model simulator, we show that our overhaul leads to an exponential improvement in simulation time for C11 litmus tests compared with the original model, making *exhaustive* simulation competitive, time-wise, with the *non-exhaustive* CDSChecker tool.
@InProceedings{POPL16p634,
author = {Mark Batty and Alastair F. Donaldson and John Wickerson},
title = {Overhauling SC Atomics in C11 and OpenCL},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {634--648},
doi = {10.1145/2837614.2837637},
year = {2016},
}
Publisher's Version Article Search
We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports fence instructions that restore sequential consistency; and (iii) admits an equivalent intuitive operational semantics based on point-to-point communication. This strengthening has no additional implementation cost: it allows the same local optimizations as C11 release and acquire accesses, and has exactly the same compilation schemes to the x86-TSO and Power architectures. In fact, the compilation to Power is complete with respect to a recent axiomatic model of Power; that is, the compiled program exhibits exactly the same behaviors as the source one. Moreover, we provide criteria for placing enough fence instructions to ensure sequential consistency, and apply them to an efficient RCU implementation.
@InProceedings{POPL16p649,
author = {Ori Lahav and Nick Giannarakis and Viktor Vafeiadis},
title = {Taming Release-Acquire Consistency},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {649--662},
doi = {10.1145/2837614.2837643},
year = {2016},
}
Publisher's Version Article Search Info
Recently, Esparza et al. generalized Newton's method -- a numerical-analysis algorithm for finding roots of real-valued functions---to a method for finding fixed-points of systems of equations over semirings. Their method provides a new way to solve interprocedural dataflow-analysis problems. As in its real-valued counterpart, each iteration of their method solves a simpler ``linearized'' problem. One of the reasons this advance is exciting is that some numerical analysts have claimed that ```all' effective and fast iterative [numerical] methods are forms (perhaps very disguised) of Newton's method.'' However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: when Newton's method is used on numerical-analysis problems, multiplicative commutativity is relied on to rearrange expressions of the form ``c*X + X*d'' into ``(c+d) * X.'' Such equations correspond to path problems described by regular languages. In contrast, when Newton's method is used for interprocedural dataflow analysis, the ``multiplication'' operation involves function composition, and hence is non-commutative: ``c*X + X*d'' cannot be rearranged into ``(c+d) * X.'' Such equations correspond to path problems described by linear context-free languages (LCFLs). In this paper, we present an improved technique for solving the LCFL sub-problems produced during successive rounds of Newton's method. Our method applies to predicate abstraction, on which most of today's software model checkers rely.
@InProceedings{POPL16p663,
author = {Thomas Reps and Emma Turetsky and Prathmesh Prabhu},
title = {Newtonian Program Analysis via Tensor Product},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {663--677},
doi = {10.1145/2837614.2837659},
year = {2016},
}
Publisher's Version Article Search
Call traces, i.e., sequences of function calls and returns, are fundamental to a wide range of program analyses such as bug reproduction, fault diagnosis, performance analysis, and many others. The conventional approach to collect call traces that instruments each function call and return site incurs large space and time overhead. Our approach aims at reducing the recording overheads by instrumenting only a small amount of call sites while keeping the capability of recovering the full trace. We propose a call trace model and a logged call trace model based on an LL(1) grammar, which enables us to define the criteria of a feasible solution to call trace collection. Based on the two models, we prove that to collect call traces with minimal instrumentation is an NP-hard problem. We then propose an efficient approach to obtaining a suboptimal solution. We implemented our approach as a tool Casper and evaluated it using the DaCapo benchmark suite. The experiment results show that our approach causes significantly lower runtime (and space) overhead than two state-of-the-arts approaches.
@InProceedings{POPL16p678,
author = {Rongxin Wu and Xiao Xiao and Shing-Chi Cheung and Hongyu Zhang and Charles Zhang},
title = {Casper: An Efficient Approach to Call Trace Collection},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {678--690},
doi = {10.1145/2837614.2837619},
year = {2016},
}
Publisher's Version Article Search
Pushdown Control-Flow Analysis for Free
Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn (University of Utah, USA; University of Maryland, USA)
Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been published that provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, implementing CFA2 and PDCFA requires significant engineering effort. Furthermore, all three are computationally expensive. For a monovariant analysis, CFA2 is in O(2^n), PDCFA is in O(n^6), and AAC is in O(n^8).
In this paper, we describe a new technique that builds on these but is both straightforward to implement and computationally inexpensive. The crucial insight is an unusual state-dependent allocation strategy for the addresses of continuations. Our technique imposes only a constant-factor overhead on the underlying analysis and costs only O(n^3) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis.
@InProceedings{POPL16p691,
author = {Thomas Gilray and Steven Lyde and Michael D. Adams and Matthew Might and David Van Horn},
title = {Pushdown Control-Flow Analysis for Free},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {691--704},
doi = {10.1145/2837614.2837631},
year = {2016},
}
Publisher's Version Article Search
Our new macro expander for Racket builds on a novel approach to hygiene. Instead of basing macro expansion on variable renamings that are mediated by expansion history, our new expander tracks binding through a set of scopes that an identifier acquires from both binding forms and macro expansions. The resulting model of macro expansion is simpler and more uniform than one based on renaming, and it is sufficiently compatible with Racket's old expander to be practical.
@InProceedings{POPL16p705,
author = {Matthew Flatt},
title = {Binding as Sets of Scopes},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {705--717},
doi = {10.1145/2837614.2837620},
year = {2016},
}
Publisher's Version Article Search Info Artifacts Available
In the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many problems are encoded as parity games, which are then solved by the seminal algorithm by Jurdzinski. In this paper we identify the essence of this workflow to be the notion of progress measure, and formalize it in general, possibly infinitary, lattice-theoretic terms. Our view on progress measures is that they are to nested/alternating fixed points what invariants are to safety/greatest fixed points, and what ranking functions are to liveness/least fixed points. That is, progress measures are combination of the latter two notions (invariant and ranking function) that have been extensively studied in the context of (program) verification. We then apply our theory of progress measures to a general model-checking framework, where systems are categorically presented as coalgebras. The framework's theoretical robustness is witnessed by a smooth transfer from the branching-time setting to the linear-time one. Although the framework can be used to derive some decision procedures for finite settings, we also expect the proposed framework to form a basis for sound proof methods for some undecidable/infinitary problems.
@InProceedings{POPL16p718,
author = {Ichiro Hasuo and Shunsuke Shimizu and Corina Cîrstea},
title = {Lattice-Theoretic Progress Measures and Coalgebraic Model Checking},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {718--732},
doi = {10.1145/2837614.2837673},
year = {2016},
}
Publisher's Version Article Search
We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.
@InProceedings{POPL16p733,
author = {Krishnendu Chatterjee and Amir Kafshdar Goharshady and Rasmus Ibsen-Jensen and Andreas Pavlogiannis},
title = {Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {733--747},
doi = {10.1145/2837614.2837624},
year = {2016},
}
Publisher's Version Article Search
A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the internal states of the latter (called memories) are exploited for accommodating algebraic effects of Plotkin and Power. The translation is compositional, hence ``denotational,'' where transducers are inductively composed using an adaptation of Barbosa's coalgebraic component calculus. In the current paper we extend the mGoI framework and provide a systematic treatment of recursion---an essential feature of programming languages that was however missing in our previous work. Specifically, we introduce two new fixed-point operators in the coalgebraic component calculus. The two follow the previous work on recursion in GoI and are called Girard style and Mackie style: the former obviously exhibits some nice domain-theoretic properties, while the latter allows simpler construction. Their equivalence is established on the categorical (or, traced monoidal) level of abstraction, and is therefore generic with respect to the choice of algebraic effects. Our main result is an adequacy theorem of our mGoI translation, against Plotkin and Power's operational semantics for algebraic effects.
@InProceedings{POPL16p748,
author = {Koko Muroya and Naohiko Hoshino and Ichiro Hasuo},
title = {Memoryful Geometry of Interaction II: Recursion and Adequacy},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {748--760},
doi = {10.1145/2837614.2837672},
year = {2016},
}
Publisher's Version Article Search
We present a new approach for learning programs from noisy datasets. Our approach is based on two new concepts: a regularized program generator which produces a candidate program based on a small sample of the entire dataset while avoiding overfitting, and a dataset sampler which carefully samples the dataset by leveraging the candidate program's score on that dataset. The two components are connected in a continuous feedback-directed loop. We show how to apply this approach to two settings: one where the dataset has a bound on the noise, and another without a noise bound. The second setting leads to a new way of performing approximate empirical risk minimization on hypotheses classes formed by a discrete search space. We then present two new kinds of program synthesizers which target the two noise settings. First, we introduce a novel regularized bitstream synthesizer that successfully generates programs even in the presence of incorrect examples. We show that the synthesizer can detect errors in the examples while combating overfitting -- a major problem in existing synthesis techniques. We also show how the approach can be used in a setting where the dataset grows dynamically via new examples (e.g., provided by a human). Second, we present a novel technique for constructing statistical code completion systems. These are systems trained on massive datasets of open source programs, also known as ``Big Code''. The key idea is to introduce a domain specific language (DSL) over trees and to learn functions in that DSL directly from the dataset. These learned functions then condition the predictions made by the system. This is a flexible and powerful technique which generalizes several existing works as we no longer need to decide a priori on what the prediction should be conditioned (another benefit is that the learned functions are a natural mechanism for explaining the prediction). As a result, our code completion system surpasses the prediction capabilities of existing, hard-wired systems.
@InProceedings{POPL16p761,
author = {Veselin Raychev and Pavol Bielik and Martin Vechev and Andreas Krause},
title = {Learning Programs from Noisy Data},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {761--774},
doi = {10.1145/2837614.2837671},
year = {2016},
}
Publisher's Version Article Search
Many advanced programming tools---for both end-users and expert developers---rely on program synthesis to automatically generate implementations from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms because they require synthesized programs to be not only correct, but also optimal with respect to a desired cost metric, such as program size. Finding these optimal solutions efficiently requires domain-specific search strategies, but existing synthesizers hard-code the strategy, making them difficult to reuse. This paper presents metasketches, a general framework for specifying and solving optimal synthesis problems. metasketches make the search strategy a part of the problem definition by specifying a fragmentation of the search space into an ordered set of classic sketches. We provide two cooperating search algorithms to effectively solve metasketches. A global optimizing search coordinates the activities of local searches, informing them of the costs of potentially-optimal solutions as they explore different regions of the candidate space in parallel. The local searches execute an incremental form of counterexample-guided inductive synthesis to incorporate information sent from the global search. We present Synapse, an implementation of these algorithms, and show that it effectively solves optimal synthesis problems with a variety of different cost functions. In addition, metasketches can be used to accelerate classic (non-optimal) synthesis by explicitly controlling the search strategy, and we show that Synapse solves classic synthesis problems that state-of-the-art tools cannot.
@InProceedings{POPL16p775,
author = {James Bornholt and Emina Torlak and Dan Grossman and Luis Ceze},
title = {Optimizing Synthesis with Metasketches},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {775--788},
doi = {10.1145/2837614.2837666},
year = {2016},
}
Publisher's Version Article Search
Maximal Specification Synthesis
Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel (University of Wisconsin-Madison, USA; University of Texas at Austin, USA; Carnegie Mellon University, USA)
Many problems in program analysis, verification, and synthesis require inferring specifications of unknown procedures. Motivated by a broad range of applications, we formulate the problem of maximal specification inference: Given a postcondition Phi and a program P calling a set of unknown procedures F_1,…,F_n, what are the most permissive specifications of procedures F_i that ensure correctness of P? In other words, we are looking for the smallest number of assumptions we need to make about the behaviours of F_i in order to prove that P satisfies its postcondition. To solve this problem, we present a novel approach that utilizes a counterexample-guided inductive synthesis loop and reduces the maximal specification inference problem to multi-abduction. We formulate the novel notion of multi-abduction as a generalization of classical logical abduction and present an algorithm for solving multi-abduction problems. On the practical side, we evaluate our specification inference technique on a range of benchmarks and demonstrate its ability to synthesize specifications of kernel routines invoked by device drivers.
@InProceedings{POPL16p789,
author = {Aws Albarghouthi and Isil Dillig and Arie Gurfinkel},
title = {Maximal Specification Synthesis},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {789--801},
doi = {10.1145/2837614.2837628},
year = {2016},
}
Publisher's Version Article Search
Input-output examples have emerged as a practical and user-friendly
specification mechanism for program synthesis in many environments.
While example-driven tools have demonstrated tangible impact that has
inspired adoption in industry, their underlying semantics are less well-understood:
what are "examples" and how do they
relate to other kinds of specifications? This paper
demonstrates that examples can, in general, be interpreted
as refinement types. Seen in this light, program
synthesis is the task of finding an inhabitant of
such a type. This insight provides an immediate
semantic interpretation for examples. Moreover,
it enables us to exploit decades of research in type theory as
well as its correspondence with intuitionistic logic rather
than designing ad hoc theoretical frameworks for synthesis from scratch.
We put this observation into practice by formalizing synthesis
as proof search in a sequent calculus with
intersection and union refinements that we prove
to be sound with respect to a conventional type system.
In addition, we show how to handle negative examples,
which arise from user feedback or counterexample-guided loops.
This theory serves as the basis for a prototype
implementation that extends our core language to
support ML-style algebraic data types and structurally
inductive functions. Users can also specify
synthesis goals using polymorphic refinements and
import monomorphic libraries.
The prototype serves as a vehicle
for empirically evaluating a number of different
strategies for resolving the nondeterminism of the sequent
calculus---bottom-up theorem-proving,
term enumeration with refinement type checking, and
combinations of both---the results of which classify, explain, and
validate the design choices of existing synthesis systems.
It also provides a platform for measuring the practical
value of a specification language that combines
"examples" with the more general expressiveness of refinements.
@InProceedings{POPL16p802,
author = {Jonathan Frankle and Peter-Michael Osera and David Walker and Steve Zdancewic},
title = {Example-Directed Synthesis: A Type-Theoretic Interpretation},
booktitle = {Proc.\ POPL},
publisher = {ACM},
pages = {802--815},
doi = {10.1145/2837614.2837629},
year = {2016},
}
Publisher's Version Article Search