Scaling Language Features for Program Verification

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we make progress towards a better verification experience in general-purpose programming languages by contributing improvements both to the automated checking and the specification of safety properties in languages combining functional and imperative features. We present our extensions in two parts -- reasoning about shared mutable data, and types as specifications -- both of which ultimately rely on reductions of expressive surface languages to a functional core. Throughout, we instantiate our techniques for the particular example of Scala, a mixed-paradigm language widely-used in industry.The first part shows how to extend a verifier for higher-order functions and immutable data to support imperative programs with shared mutable data. We build upon Stainless, a contract-based verification system that relies on SMT solvers to automatically verify a large fragment of Scala. Our technique extends Stainless to check general heap-manipulating programs against modular specifications in the style of dynamic frames. A novelty of our approach is the translation of imperative function contracts that encodes frame conditions using quantifier-free formulas in first-order logic, instead of relying on quantifiers or on dedicated separation logic reasoning. Our quantifier-free encoding enables SMT solvers to both prove safety and to report counterexamples relative to the semantics of procedure contracts.In the second part we turn to types and type-level programming as an alternative means of specifying correctness properties. While dependent types have been studied extensively for purely-functional languages, we investigate their applications to languages with subtyping and (abstractions of) imperative features. We first study a calculus that provides type-level computation through singleton types and allows abstraction of state and IO through a non-deterministic choice operator. This allows for modelling interactions with existing imprecisely-typed and impure code. Our calculus is formalized and mechanically proven correct using the Coq proof assistant. In addition, we develop a prototypical implementation in the Scala compiler and study typical type-level programming use cases in the Scala ecosystem.

Programming language abstractions for mobile code

Stéphane Micheloud

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and supports local type inference. Furthermore it integrates well with the Java and .net platforms: their libraries are accessible without glue code and the Scala compiler generates code for both execution environments. The Scala programming language has several features that make it desirable as a language for distributed application programming. In particular, it supports first-class functions which are useful in relation with the notions of distributed scope and code mobility. In that context, the missing support for run-time types is one important drawback of the Java run-time environment as a target platform. This thesis focuses on the realisation of a new concept combining essential notions from the functional and distributed programming and implying the extension of the notion of lexical scoping to the distributed context. In short, we claim that the notion of lambda abstraction provides an elegant way for dealing with the dynamic rebinding of local references in a distributed execution environment. The key ideas exposed in this research work have been implemented in our Scala compiler. This helped us to evaluate the used techniques, in particular their impact on the reliability and the performance of distributed programs. So far, most research works related to the present subject have focused on functional programming languages, in particular on the ML language family.

EPFL2009

Compiling Scala for Performance

Iulian Dragos

Scala is a new programming language bringing together object-oriented and functional programming. Its defining features are uniformity and extensibility. Scala offers great flexibility for programmers, allowing them to grow the language through libraries. Oftentimes what seems like a language feature is in fact implemented in a library, effectively giving programmers the power of language designers. The downside of this flexibility is that familiar looking code may hide unexpected performance costs. It is important for Scala compilers to bring down this cost as much as possible. We identify several areas of impact for Scala performance: higher-order functions and closures, and generic containers used with primitive types. We present two complementary approaches for improving performance in these areas: optimizations and specialization. Compiler optimization can bring down the cost through a combination of aggressive inlining of higher-order functions, an extended version of copy-propagation and dead-code elimination. Both anonymous functions and boxing can be eliminated by this approach. We show on a number of benchmarks that these language features can be up to 5 times faster when properly optimized, on current day JVMs. We propose a new approach to compiling parametric polymorphism for performance at primitive types. We mix a homogeneous translation scheme with user-directed specialization for primitive types. Type parameters may be annotated to require specialization of code depending on them. We propose definition-site specialization for primitive types, achieving separate compilation and no boxing when both the definition and call site are specialized. Specialized classes are compatible with unspecialized code, and specialization agnostic code can work with specialized instances, meaning that specialization is opportunistic. We present a formalism of a small subset of Scala with specialization and prove that specialization preserves types. We implemented this translation in the Scala compiler and report on improvements on a set of benchmarks, showing that specialization can make programs more than two times faster.

EPFL2010

Stoic: Towards Disciplined Capabilities

Nada Amin, Paolo Giosuè Giarrusso, Fengyun Liu, Martin Odersky, Sandro Stucki

Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasoning and enforcing invariants in capability-based systems challenging if not intractable. How to reason about capability-based systems formally? What abstractions that programming languages should provide to facilitate the construction of capability-based systems? Can we formulate some fundamental capability disciplines as typing rules? In this paper we propose that stoicity is a useful property in designing, reasoning and organizing capabilities in systems both at the macro-level and micro-level. Stoicity means that a component of a system does not interact with its environment in any way except through its interfaces. As an incarnation of this idea, we introduce stoic functions in a functional language. In contrast to normal functions, stoic functions cannot capture capabilities nor non-stoic functions from the environment. We formalize stoic functions in a language with mutable references as capabilities. In that setting, we show that stoic functions enjoy non-interference of memory effects. The concept of stoic functions also shows its advantage in ffect polymorphism and effect masking when used to control side effects of programs.

2020

Compiling Scala for Performance

Iulian Dragos

EPFL2010