nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Programming Languages and Systems

13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings

herausgegeben von: Xinyu Feng, Sungwoo Park

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 13th Asian Symposium on Programming Languages and Systems, APLAS 2015, held in Pohang, South Korea, in November/December 2015. The 24 regular papers presented together with 1 short paper were carefully reviewed and selected from 74 submissions. The papers cover a variety of foundational and practical issues in programming languages and systems and have been organized in topical sections on compilers, separation logic, static analysis and abstract interpretation, Hoare logic and types, functional programming and semantics, model checking, program analysis, medley, and programming models.

Inhaltsverzeichnis

Frontmatter

Invited Talk

Frontmatter

Programming with “Big Code”

Abstract

The vast amount of code available on the web is increasing on a daily basis. Open-source hosting sites such as GitHub contain billions of lines of code. Community question-answering sites provide millions of code snippets with corresponding text and metadata. The amount of code available in executable binaries is even greater. In this talk, I will cover recent research trends on leveraging such “big code” for program analysis, program synthesis and reverse engineering. We will consider a range of semantic representations based on symbolic automata [11, 15], tracelets [3], numerical abstractions [13, 14], and textual descriptions [1, 22], as well as different notions of code similarity based on these representations.

To leverage these semantic representations, we will consider a number of prediction techniques, including statistical language models [19, 20], variable order Markov models [2], and other distance-based and model-based sequence classification techniques.

Finally, I will show applications of these techniques including semantic code search in both source code and stripped binaries, code completion and reverse engineering.

Eran Yahav

Compilers

Frontmatter

Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects

Abstract

This paper presents FCore: a JVM implementation of System F with support for full tail-call elimination (TCE). Our compilation technique for FCore is innovative in two respects: it uses a new representation for first-class functions called imperative functional objects; and it provides a way to do TCE on the JVM using constant space.

Unlike conventional TCE techniques on the JVM, allocated function objects are reused in chains of tail calls. Thus, programs written in FCore can use idiomatic functional programming styles, relying on TCE, and perform well without worrying about the JVM limitations. Our empirical results show that programs which use tail calls can run in constant space and with low execution time overhead when compiled with FCore.

Tomáš Tauber, Xuan Bi, Zhiyuan Shi, Weixin Zhang, Huang Li, Zhenrui Zhang, Bruno C. D. S. Oliveira

A Secure Compiler for ML Modules

Abstract

Many functional programming languages compile to low-level languages such as C or assembly. Numerous security properties of those compilers, however, apply only when the compiler compiles whole programs. This paper presents a compilation scheme that securely compiles a standalone module of \({\text {ModuleML}}\), a light-weight version of an ML with modules, into untyped assembly. The compilation scheme is secure in that it reflects the abstractions of a \({\text {ModuleML}}\) module, for every possible piece of assembly code that it interacts with. This is achieved by isolating the compiled module through a low-level memory isolation mechanism and by dynamically type checking its interactions. We evaluate an implementation of the compiler on relevant test scenarios.

Adriaan Larmuseau, Marco Patrignani, Dave Clarke

Detection of Redundant Expressions: A Complete and Polynomial-Time Algorithm in SSA

Abstract

Detection of redundant expressions in a program based on values is a well researched problem done with a view to eliminate the redundancies so as to improve the run-time efficiency of the program. The problem entails the detection of equivalent expressions in a program. Here we present an iterative data-flow analysis algorithm to detect equivalent expressions in SSA for the purpose of detection of redundancies. The central challenge in this static analysis is to define a “join” operation to detect all equivalences at a join point such that any later occurrences of redundant expressions are detected in polynomial time. We achieve this by introducing the notion of value \(\phi \) -function. We claim the algorithm is complete and takes only polynomial time. We implemented the algorithm in LLVM and demonstrated its performance.

Rekha R. Pai

Separation Logic

Frontmatter

Separation Logic with Monadic Inductive Definitions and Implicit Existentials

Abstract

This paper proves the decidability of entailments in separation logic with monadic inductive definitions and implicit existentials. This system is obtained from the bounded-treewidth separation logic SLRDbtw of Iosif et al. in 2013 by adding implicit existential variables and restricting inductive definitions to monadic ones. The system proposed in this paper is a decidable system where one can use general recursive data structures with pointers as data, such as lists of pointers. The key idea is to reduce the problem to the decidability of SLRDbtw, by assigning local addresses or some distingu ished address to implicit existential variables so that the resulting definition clauses satisfy the establishment condition of SLRDbtw. This paper also proves the undecidability of the entailments when one adds implicit existentials to SLRDbtw. This shows that the implicit existentials are critical for the decidability.

Makoto Tatsuta, Daisuke Kimura

Tree-Like Grammars and Separation Logic

Abstract

Separation Logic with inductive predicate definitions (\(\texttt {SL}\)) and hyperedge replacement grammars (HRG) are established formalisms to describe the abstract shape of data structures maintained by heap-manipulating programs. Fragments of both formalisms are known to coincide, and neither the entailment problem for \(\texttt {SL}\) nor its counterpart for HRGs, the inclusion problem, are decidable in general.

We introduce tree-like grammars (TLG), a fragment of HRGs with a decidable inclusion problem. By the correspondence between HRGs and \(\texttt {SL}\), we simultaneously obtain an equivalent \(\texttt {SL}\) fragment (\(\texttt {SL}_{\texttt {tl}}\)) featuring some remarkable properties including a decidable entailment problem.

Christoph Matheja, Christina Jansen, Thomas Noll

Static Analysis and Abstract Interpretation

Frontmatter

Randomized Resource-Aware Path-Sensitive Static Analysis

Abstract

Many interesting properties of programs can only be proved by a path-sensitive analysis. However, path sensitivity may drastically increase analysis time and memory consumption. For existing approaches, the amount of required resources is hard to predict in advance. As a consequence, in a particular analysis run available resources may either be wasted or turn out to be insufficient.

In this paper, we propose a resource-aware approach to path-sensitive analysis that allows to control the maximal amount of required memory. It employs randomly-drawn hash functions to decide which paths to distinguish. Due to randomization, two analysis runs of the same program may yield different results. We show how to use this feature to trade analysis time for space.

Tomasz Dudziak

Quadratic Zonotopes

An Extension of Zonotopes to Quadratic Arithmetics

Abstract

Affine forms are a common way to represent convex sets of \(\mathbb {R}\) using a base of error terms \(\epsilon \in [-1, 1]^m\). Quadratic forms are an extension of affine forms enabling the use of quadratic error terms \(\epsilon _i \epsilon _j\).

In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide range of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms.

In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.

Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey

Abstraction of Optional Numerical Values

Abstract

We propose a technique to describe properties of numerical stores with optional values, that is, where some variables may have no value. Properties of interest include numerical equalities and inequalities. Our approach lifts common linear inequality based numerical abstract domains into abstract domains describing stores with optional values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded sets of program variables, and where these symbolic variables may be undefined, as in some array or shape analyses. We describe the general form of abstract states, and propose sound and automatic static analysis algorithms. We evaluate our construction in the case of an array abstract domain.

Jiangchao Liu, Xavier Rival

Hoare Logic and Types

Frontmatter

Fault-Tolerant Resource Reasoning

Abstract

Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.

Gian Ntzik, Pedro da Rocha Pinto, Philippa Gardner

Shifting the Blame

A Blame Calculus with Delimited Control

Abstract

We study integration of static and dynamic typing in the presence of delimited-control operators. In a program where typed and untyped parts coexist, the run-time system has to monitor the flow of values between these parts and abort program execution if invalid values are passed. However, control operators, which enable us to implement useful control effects, make such monitoring tricky; in fact, it is known that, with a standard approach, certain communications between typed and untyped parts can be overlooked.

We propose a new cast-based mechanism to monitor all communications between typed and untyped parts for a language with control operators shift and reset. We extend a blame calculus with shift/reset to give its semantics (operational semantics and CPS transformation) and prove two important correctness properties of the proposed mechanism: Blame Theorem and soundness of the CPS transformation.

Taro Sekiyama, Soichiro Ueda, Atsushi Igarashi

Aliasing Control in an Imperative Pure Calculus

Abstract

We present an imperative object calculus where types are annotated with two modifiers for aliasing control. The \({\mathtt{lent}}\) modifier prevents objects to be aliased, whereas the \({\mathtt{capsule}}\) modifier characterizes expressions that will reduce to isolated portions of store. There are two key novelties w.r.t. similar proposals. First, the expressivity of the type system is greatly enhanced by promotion and swapping rules. The former recognizes as \({\mathtt{capsule}}\) an expression which only uses external references as \({\mathtt{lent}}\). The latter allows a \({\mathtt{lent}}\) reference to be freely aliased, if all the other references are regarded as \({\mathtt{lent}}\). Second, execution is modeled in a pure setting, where it is simpler to understand alias control. That is, properties of modifiers can be directly expressed on source terms, rather than as invariants on an auxiliary structure which mimics physical memory. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of store when evaluated.

Marco Servetto, Elena Zucca

Functional Programming and Semantics

Frontmatter

A Strong Distillery

Abstract

Abstract machines for the strong evaluation of \(\lambda \)-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.

Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza

From Call-by-Value to Interaction by Typed Closure Conversion

Abstract

We study the efficient implementation of call-by-value using the structure of interactive computation models. This structure has been useful in applications to resource-bounded compilation, but much of the existing work in this area has focused on call-by-name programming languages. This paper works towards the goal of a simple, efficient treatment of call-by-value languages. In previous work we have studied cps-translation as an approach to implementing call-by-value and have observed that it needs to be refined in order to achieve efficient space usage. In this paper we give an alternative presentation of the refined translation, which is close to existing methods of typed closure conversion. We show that a simple correctness proof following Benton and Hur is possible for this formulation. Moreover, we extend previous work to cover full recursion in the source language.

Ulrich Schöpp

Kripke Open Bisimulation

A Marriage of Game Semantics and Operational Techniques

Abstract

Proving that two programs are contextually equivalent is notoriously hard, particularly for functional languages with references (i.e., local states). Many operational techniques have been designed to prove such equivalences, and fully abstract denotational model, using game semantics, have been built for such languages. In this work, we marry ideas coming from trace semantics, an operational variant of game semantics, and from Kripke logical relations, notably the notion of worlds as transition systems of invariants, to define a new operational technique: Kripke open bisimulations. It is the first framework whose completeness does not rely on any closure by contexts.

Guilhem Jaber, Nicolas Tabareau

Model Checking

Frontmatter

Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs

Abstract

Higher-order model checking has been recently applied to automated verification of higher-order functional programs, but there have been difficulties in dealing with algebraic data types such as lists and trees. To remedy the problem, we propose an automata-based abstraction of tree data, and a counterexample-guided refinement of the abstraction. By combining them with higher-order model checking, we can construct a fully-automated verification tool for higher-order, tree-processing functional programs. We formalize the verification method, prove its correctness, and report experimental results.

Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno

Decision Algorithms for Checking Definability of Order-2 Finitary PCF

Abstract

We consider a definability problem for finitary PCF, which asks whether, given a function (as an element of a cpo), there exists a term of finitary PCF whose interpretation is the function. The definability problem for finitary PCF is known to be decidable for types of order at most 2. However, its complexity and practical algorithms have not been well studied. In this paper, we give two algorithms for checking definability: one based on Sieber’s sequentiality relation, which runs in quadruply exponential time for the size of the type of the given function, and the other based on a saturation method, which runs in triply exponential time for the size. With the recent advance of higher-order model checking, our result may be useful for implementing a tool for deciding observational equivalence between finitary PCF terms of types of order at most 3.

Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi

Program Analysis - I

Frontmatter

Uncovering JavaScript Performance Code Smells Relevant to Type Mutations

Abstract

In dynamic typing languages such as JavaScript, object types can be mutated easily such as by adding a field to an object. However, compiler optimizations rely on a fixed set of types, unintentional type mutations can invalidate the speculative code generated by the type-feedback JIT and deteriorate the quality of compiler optimizations. Since type mutations are invisible, finding and understanding the performance issues relevant to type mutations can be an overwhelming task to programmers. We develop a tool JSweeter to detect performance bugs incurred by type mutations based on the type evolution graphs extracted from program execution. We apply JSweeter to the Octane benchmark suite and identify 46 performance issues, where 19 issues are successfully fixed with the refactoring hints generated by JSweeter and the average performance gain is 5.3 % (up to 23 %). The result is persuasive because those issues are hidden in such well developed benchmark programs.

Xiao Xiao, Shi Han, Charles Zhang, Dongmei Zhang

Analyzing Distributed Multi-platform Java and Android Applications with ShadowVM

Abstract

In this tool demonstration, we present ShadowVM, a dynamic program analysis framework for Java and Android applications. ShadowVM offers a high-level programming model for expressing analyses, ensures complete bytecode coverage, and isolates the analysis from the observed application to avoid unwanted interference. An analysis implemented on top of ShadowVM can handle both Java and Android applications. First, we present and evaluate a simple code-coverage analysis implemented with ShadowVM. Second, we demonstrate the use of ShadowVM to analyze a distributed application comprising a Java server backend and an Android client frontend.

Haiyang Sun, Yudi Zheng, Lubomír Bulej, Stephen Kell, Walter Binder

Medley

Frontmatter

Quasi-Linearizability is Undecidable

Abstract

Quasi-linearizability is a quantitative relaxation of linearizability. It preserves the intuition of the standard notion of linearizability and permits more flexibility. The decidability of quasi-linearizability has been remaining open in general for a bounded number of processes. In this paper we show that the problem of whether a library is quasi-linearizable with respect to a regular sequential specification is undecidable for a bounded number of processes. This is proved by reduction from the k-Z decision problem of a k-counter machine, a known undecidable problem. The key idea of the proof is to establish a correspondence between the quasi-sequential specification of quasi-linearizability and the set of all unadmitted runs of the k-counter machines.

Chao Wang, Yi Lv, Gaoang Liu, Peng Wu

Objects in Polynomial Time

Abstract

A type system based on non-interference and data ramification principles is introduced in order to capture the set of functions computable in polynomial time on OO programs. The studied language is general enough to capture most OO constructs and our characterization is quite expressive as it allows the analysis of a combination of imperative loops and of data ramification scheme based on Bellantoni and Cook’s safe recursion using function algebra.

Emmanuel Hainry, Romain Péchoux

Programming Models

Frontmatter

Programming Techniques for Reversible Comparison Sorts

Abstract

A common approach to reversible programming is to reversibly simulate an irreversible program with the desired functionality, which in general puts additional pressure on the computational resources (time, space.) If the same running time is required, ensuring a minimal space overhead is a significant programming challenge.

We introduce criteria for the optimality of reversible simulation: A reversible simulation is faithful if it incurs no asymptotic time overhead and bounds the space overhead (the garbage) by some function g(n), and hygienic if g is (asymptotically) optimal for faithful simulation.

We demonstrate the programming techniques used to develop faithful and hygienic reversible simulations of several well-known comparison sorts, e.g. insertion sort and quicksort, using representations of permutations in both the output and intermediate additional space required.

Holger Bock Axelsen, Tetsuo Yokoyama

Transactions on Mergeable Objects

Abstract

Destructible updates on shared objects require careful handling of concurrent accesses in multi-threaded programs. Paradigms such as Transactional Memory support the programmer in correctly synchronizing access to mutable shared data by serializing the transactional reads and writes. But under high contention, serializable transactions incur frequent aborts and limit parallelism. This can lead to a severe performance degradation.

In this paper, we propose mergeable transactions which provide a consistency semantics that allows for more scalability even under contention. Instead of aborting and re-executing, object versions from conflicting updates on shared objects are merged using data-type specific semantics. The evaluation of our prototype implementation in Haskell shows that mergeable transactions outperform serializable transactions even under low contention while providing a structured and type-safe interface.

Deepthi Devaki Akkoorath, Annette Bieniusa

A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers

Abstract

Key features of context-oriented programming (COP) are layers—modules to describe context-dependent behavioral variations of a software system—and their dynamic activation, which can modify the behavior of multiple objects that have already been instantiated. Typechecking programs written in a COP language is difficult because the activation of a layer can even change objects’ interfaces. We formalize a small COP language called \(\text {ContextFJ}_{{<:}}\) with its operational semantics and type system and show its soundness. The language features (1) dynamically activated first-class layers, (2) inheritance of layer definitions, and (3) layer subtyping.

Hiroaki Inoue, Atsushi Igarashi

Program Analysis - II

Frontmatter

Bottom-Up Context-Sensitive Pointer Analysis for Java

Abstract

This paper describes a new bottom-up, subset-based, and context-sensitive pointer analysis for Java. The main novelty of our technique is the constraint-based handling of virtual method calls and instantiation of method summaries. Since our approach generates polymorphic method summaries, it can be context-sensitive without reanalyzing the same method multiple times. We have implemented this algorithm in a tool called Scuba, and we compare it with k-CFA and k-obj algorithms on Java applications from the DaCapo and Ashes benchmarks. Our results show that the new algorithm achieves better or comparable precision to k-CFA and k-obj analyses at only a fraction of the cost.

Yu Feng, Xinyu Wang, Isil Dillig, Thomas Dillig

More Sound Static Handling of Java Reflection

Abstract

Reflection is a highly dynamic language feature that poses grave problems for static analyses. In the Java setting, reflection is ubiquitous in large programs. Any handling of reflection will be approximate, and overestimating its reach in a large codebase can be catastrophic for precision and scalability. We present an approach for handling reflection with improved empirical soundness (as measured against prior approaches and dynamic information) in the context of a points-to analysis. Our approach is based on the combination of string-flow and points-to analysis from past literature augmented with (a) substring analysis and modeling of partial string flow through string builder classes; (b) new techniques for analyzing reflective entities based on information available at their use-sites. In experimental comparisons with prior approaches, we demonstrate a combination of both improved soundness (recovering the majority of missing call-graph edges) and increased performance.

Yannis Smaragdakis, George Balatsouras, George Kastrinis, Martin Bravenboer

Backmatter

Titel: Programming Languages and Systems
herausgegeben von: Xinyu Feng
Sungwoo Park
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-26529-2
Print ISBN: 978-3-319-26528-5
DOI: https://doi.org/10.1007/978-3-319-26529-2