Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2012 | Book

Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection Read chapter Read first chapter

Programming Languages and Systems

10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings

Editors: Ranjit Jhala, Atsushi Igarashi

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the refereed proceedings of the 10th Asian Symposium on Programming Languages and Systems, APLAS 2012, held in Kyoto, Japan, in December 2012. The 24 revised full papers presented together with the abstracts of 3 invited talks were carefully reviewed and selected from 58 submissions. The papers are organized in topical sections on concurrency, security, static analysis, language design, dynamic analysis, complexity and semantics, and program logics and verification.

Table of Contents

Frontmatter

Session I: Invited Talk

Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection
Abstract
A fundamental belief underlying forty years of programming languages research, aptly captured by the slogan “Well-typed programs can’t go wrong”, is that programs augmented with machine-checked annotations are more likely to be free of bugs. But of course, real programs do wrong and programmers are voting with their feet. Dynamic languages such as Ruby, Python, Lua, JavaScript and R are unencumbered by redundant type annotations and are increasingly popular. JavaScript, the lingua franca of the web, is moving to the server with the success of Node.js. R, another dynamic language, is being used in statistics, biology and finance for data analysis and visualization. Not only are these languages devoid of types, but they utterly lack any static structure that could be used for program verification. This talk will draw examples from recent results on JavaScript and R to illustrate the extent of the problem and propose some directions for research.
Jan Vitek

Session II: Concurrency

JATO: Native Code Atomicity for Java
Abstract
Atomicity enforcement in a multi-threaded application can be critical to the application’s safety. In this paper, we take the challenge of enforcing atomicity in a multilingual application, which is developed in multiple programming languages. Specifically, we describe the design and implementation of JATO, which enforces the atomicity of a native method when a Java application invokes the native method through the Java Native Interface (JNI). JATO relies on a constraint-based system, which generates constraints from both Java and native code based on how Java objects are accessed by threads. Constraints are then solved to infer a set of Java objects that need to be locked in native methods to enforce the atomicity of the native method invocation. We also propose a number of optimizations that soundly improve the performance. Evaluation through JATO’s prototype implementation demonstrates it enforces native-method atomicity with reasonable run-time overhead.
Siliang Li, Yu David Liu, Gang Tan
Ownership Types for Object Synchronisation
Abstract
Shared-memory concurrent programming is difficult and error prone because memory accesses by concurrent threads need to be coordinated through synchronisation, which relies on programmer discipline and suffers from a lack of modularity and compile-time support. This paper exploits object structures, provided by ownership types, to enable a structured synchronisation scheme which guarantees safety and allows more concurrency within structured tasks.
Yi Lu, John Potter, Jingling Xue

Session III: Security

A Functional View of Imperative Information Flow
Abstract
We analyze dynamic information-flow control for imperative languages in terms of functional computation. Specifically, we translate an imperative language to a functional language, thus accounting for the main difficulties of information-flow control in the imperative language.
Thomas H. Austin, Cormac Flanagan, Martín Abadi
End-to-end Multilevel Hybrid Information Flow Control
Abstract
We present models and soundness results for hybrid information flow, i.e. for mechanisms that enforce noninterference-style security guarantees using a combination of static analysis and dynamic taint tracking. Our analysis has the following characteristics: (i) we formulate hybrid information flow as an end-to-end property, in contrast to disruptive monitors that prematurely terminate or otherwise alter an execution upon detecting a potentially illicit flow; (ii) our security notions capture the increased precision that is gained when static analysis is combined with dynamic enforcement; (iii) we introduce path tracking to incorporate a form of termination-sensitivity, and (iv) develop a novel variant of purely dynamic tracking that ignores indirect flows; (v) our work has been formally verified, by a comprehensive representation in the theorem prover Coq.
Lennart Beringer
Succour to the Confused Deputy
Types for Capabilities
Abstract
The possession of secrets is a recurrent theme in security literature and practice. We present a refinement type system, based on indexed intuitonist S4 necessity, for an object calculus with explicit locations (corresponding to principals) to control the principals that may possess a secret. Type safety ensures that if the execution of a well-typed program leads to a configuration with an object p located at principal a, then a possesses the capability to p. We illustrate the type system with simple examples drawn from web applications, including an illustration of how Cross-Site Request Forgery (CSRF) vulnerabilities may manifest themselves as absurd refinements on object declarations during type checking.
A fuller version of the paper is available at fpl.cs.depaul.edu/jriely/papers/2012-aplas.pdf.
Radha Jagadeesan, Corin Pitcher, James Riely
Types and Access Controls for Cross-Domain Security in Flash
Abstract
The ubiquitous Flash platform enables programmers to build sophisticated web application “mash-ups” that combine Flash executables loaded from multiple trust domains with complex, asymmetric trust relationships. Flash provides APIs and run-time checks to help programmers declare and enforce trust relationships between different domains, but there is currently no formal security model for Flash.
This paper presents the first formal security model for the Flash platform. Our formal model instantly reveals that the run-time checks performed by the Flash runtime are not sufficient to enforce data integrity – we present simple example programs that are vulnerable to attacks. We then develop a static type system for Flash programs that lets programmers specify fine-grained trust relationships, and we show that, combined with the run-time checks already performed by the Flash runtime, well-typed programs cannot violate data integrity at run-time.
Aseem Rastogi, Avik Chaudhuri, Rob Johnson

Session IV: Static Analysis I

Linear Approximation of Continuous Systems with Trapezoid Step Functions
Abstract
We introduce a novel abstract domain for the safe approximation of continuous functions in the context of abstract interpretation-based static analysis. The key-idea is to represent \(\mathcal{C}_+^2\) functions by a finite sequence of trapezoids. In this way, we get a strictly more precise approximation of the actual values with respect to existing approaches in the literature. Experimental results underline the effectiveness of the approach in terms of both precision and efficiency.
Giulia Costantini, Pietro Ferrara, Agostino Cortesi
Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code
Abstract
Many compilers target common back-ends, thereby avoiding the need to implement the same analyses for many different source languages. This has led to interest in static analysis of LLVM code. In LLVM (and similar languages) most signedness information associated with variables has been compiled away. Current analyses of LLVM code tend to assume that either all values are signed or all are unsigned (except where the code specifies the signedness). We show how program analysis can simultaneously consider each bit-string to be both signed and unsigned, thus improving precision, and we implement the idea for the specific case of integer bounds analysis. Experimental evaluation shows that this provides higher precision at little extra cost. Our approach turns out to be beneficial even when all signedness information is available, such as when analysing C or Java code.
Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks
Abstract
We propose a hierarchical shape abstract domain, so as to infer structural invariants of dynamic structures such as lists living inside static structures, such as arrays. This programming pattern is often used in safety critical embedded software as an alternative to dynamic memory allocation. Our abstract domain precisely describes such hierarchies of structures. It combines several instances of simple shape abstract domains, dedicated to the representation of elementary shape properties, and also embeds a numerical abstract domain. This modular construction greatly simplifies the design and the implementation of the abstract domain. We provide an implementation, and show the effectiveness of our approach on a problem taken from a real code.
Pascal Sotin, Xavier Rival
Vinter: A Vampire-Based Tool for Interpolation
Abstract
This paper describes the Vinter tool for extracting interpolants from proofs and minimising such interpolants using various measures. Vinter takes an input problem written in either SMT-LIB or TPTP syntax, generates so called local proofs and then uses a technique of playing in the grey areas of proofs to find interpolants minimal with respect to various measures. Proofs are found using either Z3 or Vampire, solving pseudo-boolean optimisation is delegated to Yices, while localising proofs and generating minimal interpolants is done by Vampire. We describe the use of Vinter and give experimental results on problems from bounded model checking.
Kryštof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov

Session V: Static Analysis II

Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis
Abstract
Side-effecting constraint systems were originally introduced for the analysis of multi-threaded code [22]. In this paper, we show how this formalism provides a unified framework for realizing efficient interprocedural analyses where the amount of context-sensitivity can be tweaked and where the context-sensitive analyses of local properties can be combined with flow-insensitive analyses of global properties, e.g., about the heap. Side-effecting constraint systems thus form the ideal basis for building general-purpose infrastructures for static analysis. One such infrastructure is the analyzer generator Goblint, which we used to practically evaluate this approach on real-world examples.
Kalmer Apinis, Helmut Seidl, Vesal Vojdani
Inference of Necessary Field Conditions with Abstract Interpretation
Abstract
We present a new static analysis to infer necessary field conditions for object-oriented programs. A necessary field condition is a property that should hold on the fields of a given object, for otherwise there exists a calling context leading to a failure due to bad object state. Our analysis also infers the provenance of the necessary condition, so that if a necessary field condition is violated then an explanation containing the sequence of method calls leading to a failing assertion can be produced.
When the analysis is restricted to readonly fields, i.e., fields that can only be set in the initialization phase of an object, it infers object invariants. We provide empirical evidence on the usefulness of necessary field conditions by integrating the analysis into cccheck, our static analyzer for .NET. Robust inference of readonly object field invariants was the #1 request from cccheck users.
Mehdi Bouaziz, Francesco Logozzo, Manuel Fähndrich

Session VI: Language Design

Lazy v. Yield: Incremental, Linear Pretty-Printing
Abstract
We propose a programming style for incremental stream processing based on typed simple generators. It promotes modularity and decoupling of producers and consumers just like lazy evaluation. Simple generators, however, expose the implicit suspension and resumption inherent in lazy evaluation as computational effects, and hence are robust in the presence of other effects. Simple generators let us accurately reason about memory consumption. To substantiate our claims we give a new solution to the notorious pretty-printing problem. Like earlier solutions, it is linear, backtracking-free and with bounded latency. It is also simpler to write and reason about, and is compatible with effects including IO, letting us read the source document from a file, and format it as we read.
Oleg Kiselyov, Simon Peyton-Jones, Amr Sabry
Dynamic Software Update for Message Passing Programs
Abstract
Global Session Types are typically used to express communication protocols between a number of participating entities. Analyses on these types can be used to prove that message passing programs have a variety of desirable properties such as communications safety and deadlock freedom. In this paper we provide a Global Session Type analysis for queued channel message passing programs whose code may be updated during runtime (Dynamic Software Update). In particular, we prove safety and liveness properties for well-typed programs by identifying suitable restrictions on the runtime points at which dynamic updates may occur. This includes the possibility of updating several threads without requiring global thread synchronisation.
Gabrielle Anderson, Julian Rathke
A Synchronous Language with Partial Delay Specification for Real-Time Systems Programming
Abstract
High-level formal programming languages require system designers to provide a very precise description of the system during early development phases, which may in some cases lead to arbitrary choices (i.e. the designer “overspecifies” the system). In this paper, we propose an extension of synchronous dataflow languages where the designer can specify that he does not care whether some communication is immediate or delayed. It is then up to the compiler to choose where to introduce delays, in a way that breaks causality cycles and satisfies latency requirements imposed on the system.
Rémy Wyss, Frédéric Boniol, Julien Forget, Claire Pagetti

Session VII: Dynamic Analysis

Concurrent Test Generation Using Concolic Multi-trace Analysis
Abstract
Discovering concurrency bugs is inherently hard due to the nondeterminism in multi-thread scheduling. Predictive analysis techniques have been successfully used to find such bugs by observing given test runs, and then searching for other interesting thread interleavings. For sequential code, concolic execution techniques have been used successfully to generate interesting test inputs to increase structural code coverage such as branch or statement coverage. In this paper, we propose the use of a concolic multi-trace analysis (CMTA) to efficiently increase code coverage in concurrent programs. We have implemented CMTA, and show encouraging results for some interesting benchmark programs.
Niloofar Razavi, Franjo Ivančić, Vineet Kahlon, Aarti Gupta
Java Bytecode Instrumentation Made Easy: The DiSL Framework for Dynamic Program Analysis
Abstract
Many software development tools (e.g., profilers, debuggers, testing tools) and frameworks (e.g., aspect weavers) are based on bytecode instrumentation techniques. While there are many low-level bytecode manipulation libraries that support the development of such tools and frameworks, they typically provide only low-level abstractions and require detailed knowledge of the Java Virtual Machine. In addition, they often lack the necessary infrastructure for load-time instrumentation with complete bytecode coverage to ensure that each method with a bytecode representation gets instrumented. In this paper we give an introduction to DiSL, a domain-specific aspect language and framework for bytecode instrumentation that reconciles high expressiveness of the language, high level of abstraction, and efficiency of the generated code. We illustrate the strengths of DiSL with a concrete analysis as a case study. The DiSL framework is open-source and has been successfully used in several research projects.
Lukáš Marek, Yudi Zheng, Danilo Ansaloni, Aibek Sarimbekov, Walter Binder, Petr Tůma, Zhengwei Qi

Session VIII: Complexity and Semantics

Indexed Realizability for Bounded-Time Programming with References and Type Fixpoints
Abstract
The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We present a realizability semantics for a higher-order functional language based on a fragment of linear logic called LAL which characterizes the complexity class PTIME. This language features recursive types and higher-order store. Our realizability is based on biorthogonality, indexing and is quantitative. This last feature enables us not only to derive a semantical proof of termination, but also to give bounds on the number of computational steps of typed programs.
Aloïs Brunel, Antoine Madet
A New Order-Theoretic Characterisation of the Polytime Computable Functions
Abstract
We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the small polynomial path order (sPOP * for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term rewrite systems fully automatically: for any rewrite system compatible with sPOP* that employs recursion upto depth d, the (innermost) runtime complexity is polynomially bounded of degree d. This bound is tight.
Martin Avanzini, Naohi Eguchi, Georg Moser
A Dynamic Interpretation of the CPS Hierarchy
Abstract
The CPS hierarchy of control operators shift i /reset i of Danvy and Filinski is a natural generalization of the shift and reset static control operators that allow for abstracting delimited control in a structured and CPS-guided manner. In this article we show that a dynamic variant of shift/reset, known as shift 0/reset 0, where the discipline of static access to the stack of delimited continuations is relaxed, can fully express the CPS hierarchy. This result demonstrates the expressive power of shift 0 /reset 0 and it offers a new perspective on practical applications of the CPS hierarchy.
Marek Materzok, Dariusz Biernacki

Session IX: Invited Talk

Scalable Formal Machine Models
Abstract
In the past few years, we have seen machine-checked proofs of relatively large software systems, including compilers and micro-kernels. But like all formal arguments, the assurance gained by these mechanical proofs is only as good as the models we construct of the underlying machine. I will argue that how we construct and validate these models is of vital importance for the research community. In particular, I propose that we develop domain-specific languages (DSLs) for describing the semantics of machines, and build interpretations of these DSLs in our respective proof-development systems. This will allow us to factor out and re-use machine semantics for everything from software to hardware.
Greg Morrisett

Session X: Program Logics and Verification

Modular Verification of Concurrent Thread Management
Abstract
Thread management is an essential functionality in OS kernels. However, verification of thread management remains a challenge, due to two conflicting requirements: on the one hand, a thread manager—operating below the thread abstraction layer–should hide its implementation details and be verified independently from the threads being managed; on the other hand, the thread management code in many real-world systems is concurrent, which might be executed by the threads being managed, so it seems inappropriate to abstract threads away in the verification of thread managers. Previous approaches on kernel verification view thread managers as sequential code, thus cannot be applied to thread management in realistic kernels. In this paper, we propose a novel two-layer framework to verify concurrent thread management. We choose a lower abstraction level than the previous approaches, where we abstract away the context switch routine only, and allow the rest of the thread management code to run concurrently in the upper level. We also treat thread management data as abstract resources so that threads in the environment can be specified in assertions and be reasoned about in a proof system similar to concurrent separation logic.
Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi
A Case for Behavior-Preserving Actions in Separation Logic
Abstract
Separation Logic is a widely-used tool that allows for local reasoning about imperative programs with pointers. A straightforward definition of this ”local reasoning” is that, whenever a program runs safely on some state, adding more state would have no effect on the program’s behavior. However, for a mix of technical and historical reasons, local reasoning is defined in a more subtle way, allowing a program to lose some behaviors when extra state is added. In this paper, we propose strengthening local reasoning to match the straightforward definition mentioned above. We argue that such a strengthening does not have any negative effect on the usability of Separation Logic, and we present four examples that illustrate how this strengthening simplifies some of the metatheoretical reasoning regarding Separation Logic. In one example, our change even results in a more powerful metatheory.
David Costanzo, Zhong Shao
A Generic Cyclic Theorem Prover
Abstract
We describe the design and implementation of an automated theorem prover realising a fully general notion of cyclic proof. Our tool, called \(\textsc{Cyclist}\), is able to construct proofs obeying a very general cycle scheme in which leaves may be linked to any other matching node in the proof, and to verify the general, global infinitary condition on such proof objects ensuring their soundness. \(\textsc{Cyclist}\) is based on a new, generic theory of cyclic proofs that can be instantiated to a wide variety of logics. We have developed three such concrete instantiations, based on: (a) first-order logic with inductive definitions; (b) entailments of pure separation logic; and (c) Hoare-style termination proofs for pointer programs. Experiments run on these instantiations indicate that \(\textsc{Cyclist}\) offers significant potential as a future platform for inductive theorem proving.
James Brotherston, Nikos Gorogiannis, Rasmus L. Petersen
Decision Procedures over Sophisticated Fractional Permissions
Abstract
Fractional permissions enable sophisticated management of resource accesses in both sequential and concurrent programs. Entailment checkers for formulae that contain fractional permissions must be able to reason about said permissions to verify the entailments. We show how entailment checkers for separation logic with fractional permissions can extract equation systems over fractional shares. We develop a set decision procedures over equations drawn from the sophisticated boolean binary tree fractional permission model developed by Dockins et al.[4]. We prove that our procedures are sound and complete and discuss their computational complexity. We explain our implementation and provide benchmarks to help understand its performance in practice. We detail how our implementation has been integrated into the HIP/SLEEK verification toolset. We have machine-checked proofs in Coq.
Xuan Bach Le, Cristian Gherghina, Aquinas Hobor

Session XI: Invited Talk

Mechanized Semantics for Compiler Verification
Abstract
The formal verification of compilers and related programming tools depends crucially on the availability of appropriate mechanized semantics for the source, intermediate and target languages. In this invited talk, I review various forms of operational semantics and their mechanization, based on my experience with the formal verification of the CompCert C compiler.
Xavier Leroy
Backmatter
Metadata
Title
Programming Languages and Systems
Editors
Ranjit Jhala
Atsushi Igarashi
Copyright Year
2012
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-35182-2
Print ISBN
978-3-642-35181-5
DOI
https://doi.org/10.1007/978-3-642-35182-2

Premium Partner

    Image Credits