Programming Languages and Systems

Frontmatter

Abductive Inference for Reasoning about Heaps

Abstract

The driving force behind Space Invader [1,2,3] - an automatic tool aiming to perform accurate static analysis of programs using pointers - is the idea of local reasoning, which is enabled by the Frame Rule of separation logic [4]:

$$\frac{\{P\} C \{Q \}}{\{P * R \} C \{ Q* R \}} $$

In this rule R is the frame, i.e., the part of the heap which is not touched by the execution of the command C. The Frame Rule allows pre and postconditions to concentrate on the footprint: the cells touched by command C.

Dino Distefano

A Sound Floating-Point Polyhedra Abstract Domain

Abstract

The polyhedra abstract domain is one of the most powerful and commonly used numerical abstract domains in the field of static program analysis based on abstract interpretation. In this paper, we present an implementation of the polyhedra domain using floating-point arithmetic without sacrificing soundness. Floating-point arithmetic allows a compact memory representation and an efficient implementation on current hardware, at the cost of some loss of precision due to rounding. Our domain is based on a constraint-only representation and employs sound floating-point variants of Fourier-Motzkin elimination and linear programming. The preliminary experimental results of our prototype are encouraging. To our knowledge, this is the first time that the polyhedra domain is adapted to floating-point arithmetic in a sound way.

Liqian Chen, Antoine Miné, Patrick Cousot

A Flow-Sensitive Region Inference for CLI

Abstract

Region-based memory management can offer improved time performance, relatively good memory locality and reuse, and also provide better adherence to real-time constraints during execution, when compared against traditional garbage collection. We have implemented a region-memory subsystem into the SSCLI 2.0 platform and then adapted an inference system to region-enable CIL programs, with the aid of newly introduced instructions. Initial results are promising, as the programs running with regions have considerably smaller interrupting delays, compared to those running with garbage collection. Regions can bring runtime improvement for some programs (up to 50%), depending on how complicated are the data structures used in execution.

Alexandru Stefan, Florin Craciun, Wei-Ngan Chin

Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution

Abstract

Symbolic execution is a flexible and powerful, but computationally expensive technique to detect dynamic behaviors of a program. In this paper, we present a context-sensitive relevancy analysis algorithm based on weighted pushdown model checking, which pinpoints memory locations in the program where symbolic values can flow into. This information is then utilized by a code instrumenter to transform only relevant parts of the program with symbolic constructs, to help improve the efficiency of symbolic execution of Java programs. Our technique is evaluated on a generalized symbolic execution engine that is developed upon Java Path Finder with checking safety properties of Java applications. Our experiments indicate that this technique can effectively improve the performance of the symbolic execution engine with respect to the approach that blindly instruments the whole program.

Xin Li, Daryl Shannon, Indradeep Ghosh, Mizuhito Ogawa, Sreeranga P. Rajan, Sarfraz Khurshid

Static Detection of Place Locality and Elimination of Runtime Checks

Abstract

Harnessing parallelism particularly for high performance computing is a demanding topic of research. Limitations and complexities of automatic parallelization have led to programming language notations wherein a user programs parallelism explicitly and partitions a global address space for harnessing parallelism. X10 from IBM uses the notion of places to partition the global address space. The model of computation for such languages involves threads and data distributed over local and remote places. A computation is said to be place local if all the threads and data pertaining to it are at the same place. Analysis and optimizations targeting derivations of place-locality have recently gained ground with the advent of partitioned global address space (PGAS) languages like UPC and X10, wherein efficiency of place local accesses is performance critical.

In this paper, we present a novel framework for statically establishing place locality in X10. The analysis framework is based on a static abstraction of activities (threads) incorporating places and an extension to classical escape analysis to track the abstract-activities to which an object can escape. Using this framework, we describe an algorithm that eliminates runtime checks that are inserted by the X10 compiler to enforce place locality of data access. We also identify place locality checks that are guaranteed to fail. Our framework takes advantage of the high level abstraction of X10 distributions to reason about place locality of array accesses in loops as well. The underlying issues, the framework and its power are illustrated through a series of examples.

Shivali Agarwal, RajKishore Barik, V. Krishna Nandivada, Rudrapatna K. Shyamasundar, Pradeep Varma

Certified Reasoning in Memory Hierarchies

Abstract

Parallel programming is rapidly gaining importance as a vector to develop high performance applications that exploit the improved capabilities of modern computer architectures. In consequence, there is a need to develop analysis and verification methods for parallel programs.

Sequoia is a language designed to program parallel divide-and-conquer programs over a hierarchical, tree-structured, and explicitly managed memory. Using abstract interpretation, we develop a compositional proof system to analyze Sequoia programs and reason about them. Then, we show that common program optimizations transform provably correct Sequoia programs into provably correct Sequoia programs.

Gilles Barthe, César Kunz, Jorge Luis Sacchini

The Complexity of Coverage

Abstract

We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing “reset” action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies.

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar

Game Characterizations of Process Equivalences

Abstract

In this paper we propose a hierarchy of games that allows us to make a systematic comparison of process equivalences by characterizing process equivalences as games. The well-known linear/branching time hierarchy of process equivalences can be embedded into the game hierarchy, which not only provides us with a refined analysis of process equivalences, but also offers a guidance to defining interesting new process equivalences.

Xin Chen, Yuxin Deng

Extensional Universal Types for Call-by-Value

Abstract

We propose \({\lambda_{\text{c}}2_{\eta}}\) -calculus, which is a second-order polymorphic call-by-value calculus with extensional universal types. Unlike product types or function types in call-by-value, extensional universal types are genuinely right adjoint to the weakening, i.e., β-equality and η-equality hold for not only values but all terms. We give monadic style categorical semantics, so that the results can be applied also to languages like Haskell. To demonstrate validity of the calculus, we construct concrete models for the calculus in a generic manner, exploiting “relevant” parametricity. On such models, we can obtain a reasonable class of monads consistent with extensional universal types. This class admits polynomial-like constructions, and includes non-termination, exception, global state, input/output, and list-non-determinism.

Kazuyuki Asada

Harnessing the Multicores: Nested Data Parallelism in Haskell

Abstract

If you want to program a parallel computer, a purely functional language like Haskell is a promising starting point. Since the language is pure, it is by-default safe for parallel evaluation, whereas imperative languages are by-default unsafe. But that doesn’t make it easy! Indeed it has proved quite difficult to get robust, scalable performance increases through parallel functional programming, especially as the number of processors increases.

A particularly promising and well-studied approach to employing large numbers of processors is to use data parallelism. Blelloch’s pioneering work on NESL showed that it was possible to combine a rather flexible programming model (nested data parallelism) with a fast, scalable execution model (flat data parallelism). In this talk I will describe Data Parallel Haskell, which embodies nested data parallelism in a modern, general-purpose language, implemented in a state-of-the-art compiler, GHC. I will focus particularly on the vectorisation transformation, which transforms nested to flat data parallelism, and I hope to present performance numbers.

Simon Peyton Jones

Minimal Ownership for Active Objects

Abstract

Active objects offer a structured approach to concurrency, encapsulating both unshared state and a thread of control. For efficient data transfer, data should be passed by reference whenever possible, but this introduces aliasing and undermines the validity of the active objects. This paper proposes a minimal variant of ownership types that preserves the required race freedom invariant yet enables data transfer by reference between active objects (that is, without copying) in many cases, and a cheap clone operation where copying is necessary. Our approach is general and should be adaptable to several existing active object systems.

Dave Clarke, Tobias Wrigstad, Johan Östlund, Einar Broch Johnsen

Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References

Abstract

We present a type-based deadlock-freedom verification for concurrent programs with non-block-structured lock primitives and mutable references. Though those two features are frequently used, they are not dealt with in a sufficient manner by previous verification methods. Our type system uses a novel combination of lock levels, obligations and ownerships. Lock levels are used to guarantee that locks are acquired in a specific order. Obligations and ownerships guarantee that an acquired lock is released exactly once.

Kohei Suenaga

Reasoning about Java’s Reentrant Locks

Abstract

This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permissionaccounting separation logic. As usual, each lock is associated with a resource invariant, i.e., when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parameterized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.

Christian Haack, Marieke Huisman, Clément Hurlin

ML Modules and Haskell Type Classes: A Constructive Comparison

Abstract

Researchers repeatedly observed that the module system of ML and the type class mechanism of Haskell are related. So far, this relationship has received little formal investigation. The work at hand fills this gap: It introduces type-preserving translations from modules to type classes and vice versa, which enable a thorough comparison of the two concepts.

Stefan Wehr, Manuel M. T. Chakravarty

The Essence of Form Abstraction

Abstract

Abstraction is the cornerstone of high-level programming; HTML forms are the principal medium of web interaction. However, most web programming environments do not support abstraction of form components, leading to a lack of compositionality. Using a semantics based on idioms, we show how to support compositional form construction and give a convenient syntax.

Ezra Cooper, Sam Lindley, Philip Wadler, Jeremy Yallop

On Affine Usages in Signal-Based Communication

Abstract

We describe a type system for a synchronous π-calculus formalising the notion of affine usage in signal-based communication. In particular, we identify a limited number of usages that preserve affinity and that can be composed. As a main application of the resulting system, we show that typable programs are deterministic.

Roberto M. Amadio, Mehdi Dogguy

Abstraction of Clocks in Synchronous Data-Flow Systems

Abstract

Synchronous data-flow languages such as Lustre manage infinite sequences or streams as basic values. Each stream is associated to a clock which defines the instants where the current value of the stream is present. This clock is a type information and a dedicated type system — the so-called clock-calculus — statically rejects programs which cannot be executed synchronously. In existing synchronous languages, it amounts at asking whether two streams have the same clocks and thus relies on clock equality only. Recent works have shown the interest of introducing some relaxed notion of synchrony, where two streams can be composed as soon as they can be synchronized through the introduction of a finite buffer (as done in the SDF model of Edward Lee). This technically consists in replacing typing by subtyping. The present paper introduces a simple way to achieve this relaxed model through the use of clock envelopes. These clock envelopes are sets of concrete clocks which are not necessarily periodic. This allows to model various features in real-time embedded software such as bounded jitter as found in video-systems, execution time of real-time processes and scheduling resources or the communication through buffers. We present the algebra of clock envelopes and its main theoretical properties.

Albert Cohen, Louis Mandel, Florence Plateau, Marc Pouzet

From Authorization Logics to Types for Authorization

Abstract

Web services and mashups are collaborative distributed systems built by assembling components from multiple independent applications. Such composition and aggregation involves subtle combinations of authorization, delegation, and trust. Consequently, how to do so securely remains a topic of current research.

Authorization logics elegantly record the change of context from sender to receiver when messages are transmitted in distributed systems. Such logics are well suited to specify security policies since they satisfy a non-interference property: namely, that the dependencies between the statements of principals arise solely from the user-defined non-logical axioms. Building on the prior work of Abadi, Abadi and Garg, and Garg and Pfenning, we describe a semantic approach to such non-interference results.

Authorization logics constitute the logical foundations of our type-and-effect system for TAPIDO, a calculus of distributed objects. The effects are “object-centric” and record the rights associated with the object. Object effects are validated at the point of creation, ensuring that the security policy permits the creation of the object. When such an object is received, the associated rights, perhaps constrained by provenance information, are delegated as a benefit accrued to the recipient. A TAPIDO program is safe if every object creation at runtime is in conformance with the security policy of the system. Well-typed programs are safe even in the face of dishonest opponent processes that aim to subvert the global authorization policy by creating unauthorized objects.

This talk is based on joint work with Abramsky and joint work with Cirillo, Pitcher and Riely.

Radha Jagadeesan

Interface Types for Haskell

Abstract

Interface types are a useful concept in object-oriented programming languages like Java or C#. A clean programming style advocates relying on interfaces without revealing their implementation.

Haskell’s type classes provide a closely related facility for stating an interface separately from its implementation. However, there are situations in which no simple mechanism exists to hide the identity of the implementation type of a type class. This work provides such a mechanism through the integration of lightweight interface types into Haskell.

The extension is non-intrusive as no additional syntax is needed and no existing programs are affected. The implementation extends the treatment of higher-rank polymorphism in production Haskell compilers.

Peter Thiemann, Stefan Wehr

Exception Handlers as Extensible Cases

Abstract

Exceptions are an indispensable part of modern programming languages. They are, however, handled poorly, especially by higherorder languages such as Standard ML and Haskell: in both languages a well-typed program can unexpectedly fail due to an uncaught exception. In this paper, we propose a technique for type-safe exception handling. Our approach relies on representing exceptions as sums and assigning exception handlers polymorphic, extensible row types. Based on this representation, we describe an implicitly typed external language EL where well-typed programs do not raise any unhandled exceptions. EL relies on sums, extensible records, and polymorphism to represent exceptionhandling, and its type system is no more complicated than that for existing languages with polymorphic extensible records.

EL is translated into an internal language IL that is a variant of System F extended with extensible records. The translation performs a CPS transformation to represent exception handlers as continuations. It also relies on duality to transform sums into records. (The details for this translation are given in an accompanying technical report.)

We describe the implementation of a compiler for a concrete language based on EL. The compiler performs full type inference and translates EL-style source code to machine code. Type inference relieves the programmer from having to provide explicit exception annotations. We believe that this is the first practical proposal for integrating exceptions into the type system of a higher-order language.

Matthias Blume, Umut A. Acar, Wonseok Chae

Sound and Complete Type Inference for a Systems Programming Language

Abstract

This paper introduces a new type system designed for safe systems programming. The type system features a new mutability model that combines unboxed types with a consistent typing of mutability. The type system is provably sound, supports polymorphism, and eliminates the need for alias analysis to determine the immutability of a location. A sound and complete type inference algorithm for this system is presented.

Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith

An Operational Semantics for JavaScript

Abstract

We define a small-step operational semantics for the ECMAScript standard language corresponding to JavaScript, as a basis for analyzing security properties of web applications and mashups. The semantics is based on the language standard and a number of experiments with different implementations and browsers. Some basic properties of the semantics are proved, including a soundness theorem and a characterization of the reachable portion of the heap.

Sergio Maffeis, John C. Mitchell, Ankur Taly

JavaScript Instrumentation in Practice

Abstract

JavaScript has been exploited to launch various browser-based attacks. Our previous work proposed a theoretical framework applying policy-based code instrumentation to JavaScript. This paper further reports our experience carrying out the theory in practice. Specifically, we discuss how the instrumentation is performed on various JavaScript and HTML syntactic constructs, present a new policy construction method for facilitating the creation and compilation of security policies, and document various practical difficulties arose during our prototyping. Our prototype currently works with several different web browsers, including Safari Mobile running on iPhones. We report our results based on experiments using representative real-world web applications

Haruka Kikuchi, Dachuan Yu, Ajay Chander, Hiroshi Inamura, Igor Serikov

Backmatter