Workshop: Advances in Programming Languages and Systems

In this talk, I will argue that formally verifying the correctness and the termination of a program is not sufficient: to prevent bugs, one ought to also verify the asymptotic complexity of the program. I will present an extension of CFML, a Coq-based verification tool for imperative programs, with time credits, which allow establishing the amortized asymptotic complexity of a program in Separation Logic. I will present application of this tool to the verification of the correctness and asymptotic complexity of an OCaml implementation of the classic Union-Find data structure, which yields a bound expressed using the inverse Ackermann function.

Object capabilities are a technique for fine-grained privilege separation in programming languages and systems, with important applications in security. However, current formal characterisations do not fully capture capability-safety of a programming language and are not sufficient for verifying typical applications. Using state-of-the-art techniques from programming languages research, we define a logical relation for a core calculus of JavaScript that better characterises capability-safety. The relation is powerful enough to reason about typical capability patterns and supports evolvable invariants on shared data structures, capabilities with restricted authority over them and isolated components with restricted communication channels. We use a novel notion of effect parametricity for deriving properties about effects. We demonstrate that our results imply memory access bounds that have previously been used to characterise capability-safety.

Static type checking guarantees the absence of particular classes of errors at run-time but may also impede programmer productivity by rejecting programs that are dynamically safe. Dynamic typing allows a flexible programming style but unsafe programs crash at run-time. Gradual typing combines static and dynamic typing into a single language to allow programmers to use both typing disciplines in their projects as appropriate. Gradual Security Typing applies the principles of gradual typing to type systems for information flow control. We start with a Java core calculus and a standard security type system that annotates types with security levels. To “gradualize” the calculus we extend it with a dynamic security annotation that is ignored during typechecking, and cast instructions that convert between dynamically and statically annotated types. The information flow for values of dynamic type is checked at run-time using standard dynamic or hybrid information flow control. Passing values between dynamically and statically typed code is only possible through casts which ensures that static code does not require dynamic checking.

We present some recent and future work on improving the precision of control-flow analyses for languages with rich static type systems. In particular, we give a monovariant flow analysis for System~F (with recursion) that yields both control-flow information, approximating the λ- and Λ-expressions that may be bound to variables, and type-flow information, approximating the type expressions that may instantiate type variables. Moreover, the two flows are mutually beneficial: the control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may instantiate which type variables), while the type flow filters the λ- and Λ-expressions that may be bound to variables (by rejecting expressions with static types that are incompatible with the static type of the variable under the type flow). We briefly recount the key challenges in obtaining a decidable analysis and an efficient algorithm and consider future directions for this research.

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 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.

Reversibility allows the execution of programs not only in the standard, forward direction, but also backward, going to past states. The notion of reversibility suited to concurrent systems is causal-consistent reversibility, where any action can be undone provided that its consequences (if any) are undone beforehand. We will discuss the basic theory of causal-consistent reversibility, together with applications to reliability and to debugging.

Unlike traditional static type checking, the type system in the Dart programming language is unsound by design, even for fully annotated programs. The rationale has been that this allows compile-time detection of likely errors and enables code completion in integrated development environments, without being restrictive on programmers.

Despite unsoundness, judicious use of type annotations can ensure useful properties of the runtime behavior of Dart programs. We present a formal model of a core of Dart with a focus on its type system, which allows us to elucidate the causes of unsoundness. Our main contribution is a characterization of message-safe programs and a theorem stating that such programs will never encounter ‘message not understood’ errors at runtime. Message safety is less restrictive than traditional type soundness, and we argue that it forms a natural intermediate point between dynamically typed and statically typed Dart programs.

Grace is new purely object-oriented educational language that we are developing. Grace needs some kind of support for “code reuse” but what should we choose: inheritance, delegation, or something else? Inheritance and delegation are often considered roughly equivalent, but differ strongly in the details. Grace’s hopes to support both object- and class-based programming is greatly complicated by this difference.

We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view (or UNPUSH to recall effects) and PULL the effects of potentially uncommitted concurrent transactions into their local view (or UNPULL to detangle). Each operation comes with simple criteria given in terms of commutativity (Lipton’s left-movers and right-movers). The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules’ criteria.

Although type soundness is usually proved for a call-by-value semantics, it often also holds for full reduction, as is the case in core ML, System F, or Fsub. Hence, these type systems prevent erroneous expressions to appear in any context—a useful property that the programmer knows.

However, this is no more true with GADTs (or dependent types): full reduction could be unsafe in branches of GADTs that make type assumptions that may not hold in all executions of the program. The usual solution to freeze the evaluation in all branches of GADTs is too coarse.

We argue that when extending a language with propositions, we should distinguish consistent assumptions, which are erasable from possibly inconsistent assumptions, which are not and must delay the evaluation. We also introduce hiding of assumptions, to allow full reduction of subexpressions that do not depend on inconsistent assumptions. This increases flexibility, but it is also necessary to recover confluence.

We want to prove that a static analysis of a given program is complete, namely, no imprecision arises when asking some query on the program behavior in the concrete (i.e. for its concrete semantics) or in the abstract (i.e. for its abstract interpretation). Completeness proofs are therefore useful to assign confidence to alarms raised by static analyses. We introduce the completeness class of an abstraction as the set of all programs for which the abstraction is complete. We show that for any nontrivial abstraction, its completeness class is not recursively enumerable. We then introduce a stratified deductive system to prove the completeness of program analyses over an abstract domain A. We prove the soundness of the deductive system and we observe that the only sources of incompleteness are assignments and Boolean tests — unlikely a common belief in static analysis, joins do not induce incompleteness. The first layer of this proof system is generic, abstraction-agnostic, and it deals with the standard constructs for program composition, that is, sequential composition, branching and guarded iteration. The second layer is instead abstraction-specific: the designer of an abstract domain A provides conditions for completeness in A of assignments and Boolean tests which have to be checked by a suitable static analysis or assumed in the completeness proof as hypotheses. We instantiate the second layer of this proof system first with a generic nonrelational abstraction in order to provide a sound rule for the completeness of assignments. Orthogonally, we instantiate it to the numerical abstract domains of Intervals and Octagons, providing necessary and sufficient conditions for the completeness of their Boolean tests and of assignments for Octagons.

Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to abandon standard specification techniques, such as linearizability, in favor of more relaxed consistency requirements. However, the variety of alternative correctness conditions makes it difficult to choose which one to employ in a particular case, and to compose them when using objects whose behaviors are specified via different criteria. The lack of syntactic verification methods for most of these criteria poses challenges in their systematic adoption and application.

In this work, we argue for using Hoare-style program logics as an alternative and uniform approach for specification and compositional formal verification of safety properties for concurrent objects and heir client programs. Through a series of case studies, we demonstrate how an existing program logic for concurrency can be employed off-the-shelf to capture important state and history invariants, allowing one to explicitly quantify over interference of environment threads and provide intuitive and expressive Hoare-style specifications for several non-linearizable concurrent objects that were previously specified only via dedicated correctness criteria. We illustrate the adequacy of our specifications by verifying a number of concurrent client scenarios, that make use of the previously specified concurrent objects, capturing the essence of such correctness conditions as concurrency-aware linearizability, quiescent, and quantitative quiescent consistency.

As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution [joint with Hugo López, Eduardo Marques, Francisco Martins, Nicholas Ng, César Santos, Nobuko Yoshida]