Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide very pessimistic overestimates, causing unnecessary verification failure. Furthermore, there are no available rigorous approaches that handle transcendental functions other than by analyzing truncated series expansions thereof. We have developed a new approach called Symbolic Taylor Expansions that avoids these problems, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. In addition to providing far tighter upper bounds of round-off error in a vast majority of cases, FPTaylor also emits per-instance analysis certificates in the form of HOL Light proofs that can be machine checked. In this paper, we present details of Symbolic Taylor Expansions, and comparisons with other rigorous approaches. We also release FPTaylor along with our benchmarks for evaluation.
In security-typed programming languages, types statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions. But to adopt static security types, like other advanced type disciplines, programmers face a steep wholesale transition, often forcing them to refactor working code just to satisfy their type checker. To provide a gentler path to security typing that supports safe and stylish but hard-to-verify programming idioms, researchers have designed languages that blend static and dynamic checking of security types. Unfortunately the resulting languages only support static, type-based reasoning about noninterference if a program is purely statically secured. This limitation substantially weakens the benefits that dynamic enforcement bring to static security typing. In this paper we present GSLref, a gradual security-typed higher-order language with references, which lets programmers use types to reason statically about noninterference in all programs, even those that enforce security dynamically. We prove that GSLref satisfies all but one of Siek et al.'s refined criteria for gradually-typed languages, which ensure that programs can seamlessly combine and transition between simple typing and security typing. It remains an open question whether such a language could satisfy Siek et al.'s dynamic gradual guarantee. To realize this design, we were led to acknowledge a sharp distinction between syntactic type safety and semantic type soundness, each of which constrains the design of the gradual language.
Some interesting communication protocols can be precisely described only by context-free session types, an extension of conventional session types supporting a general form of sequential composition. The complex metatheory of context-free session types, however, hinders the de nition of corresponding checking and inference algorithms. In this work we address and solve these problems introducing a new syntax-directed type system for context-free session types of which we provide two OCaml embeddings.
Program analyses often utilize various forms of sensitivity such as context sensitivity and object sensitivity. These techniques all allow for more precise program analyses, that are able to compute more precise program invariants, and to verify stronger properties. Despite the fact that sensitivity techniques are now part of the standard toolkit of static analyses designers and implementers, no comprehensive frameworks allow the description of all common forms of sensitivity. As a consequence, the soundness proofs of static analysis tools involving sensitivity often rely on ad hoc formalization, which are not always carried out in an abstract interpretation framework. Moreover, this also means that opportunities to identify similarities between analysis techniques to better improve abstractions or to tune static analysis tools can easily be missed. In this paper, we present and formalize a framework for the description of sensitivity in static analysis. Our framework is based on a powerful abstract domain construction, and utilizes reduced cardinal power to tie basic abstract predicates to the properties analyses are sensitive to. We formalize this abstraction, and the main abstract operations that are needed to turn it into a generic abstract domain construction. We demonstrate that our approach can allow for a more precise description of program states, and that it can also describe a large set of sensitivity techniques, both when sensitivity criteria are static or dynamic, and sensitive analysis tuning parameters. Last, we show that sensitivity techniques used in state of the art static analysis tools can be described in our framework.
Constructing a high-performance garbage collector is hard. Constructing a fully concurrent on-the-fly (OTF), compacting collector is much more so. We describe our experience of implementing the Sapphire algorithm as the first on-the-fly, parallel, replication copying, garbage collector for the Jikes RVM Java virtual machine. In part, we explain our innovations such as copying with hardware and software transactions, OTF management of Javas reference types and simple, yet correct, lock-free management of volatile fields in a replicating collector. We fully evaluate, for the first time, and using realistic benchmarks, Sapphires performance and suitability as a low latency collector. An important contribution of this work is a detailed description of our experience of building an OTF copying collector for a complete JVM with some assurance that it is correct. A key aspect of this is model checking of critical components of this complicated and highly concurrent system.
Dependent types are a key feature of the type systems used by the proof assistants based on the intuitionistic Curry-Howard correspondence. On the other hand, this correspondence can be extended to classical logic provided the language of proofs is enriched with control operators. Alas, control operators are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. Besides, while sequent calculi smoothly support abstract machine and continuation-passing style interpretations, there is no such presentation of a language with dependent types. The main achievement of this paper is to give a sequent calculus presentation of a call-by-value language with a control operator and dependent types, and to justify its soundness through a continuation-passing style translation. We start from the call-by-value version of the »µµ~-language and design a minimal language with a value restriction and a type system that includes a list of explicit dependencies and maintains type safety. We then show how to relax the value restriction and introduce delimited continuations to directly prove the consistency by means of a continuation-passing-style translation. Finally, we relate our calculus to a similar system by Lepigre, and present a methodology to transfer properties from this system to our own.
Medical prescriptions are algorithmic sets of instructions that may include orders for drug therapy, diet, activity, clinical assessment, laboratory testing, and other tasks. Clinicians have long used algorithmic thinking to describe and implement these prescriptions without the benefit of the conceptual framework provided by a programming language. Instead, medical algorithms are expressed using a natural language patois, flowcharts, or (more recently) as structured data in database tables. This lack of a programming language often results in prescriptions that are difficult to understand, hard to debug, and awkward to reuse. This article reports on the design and evaluation of POP-PL, a domain-specific programming language for expressing prescriptions. The language design draws on the experience of researchers in two disciplines, programming languages and medicine. The language is based around the idea that programs and humans have complementary strengths, that when combined can make for safer, more accurate performance of prescriptions. Use of POP-PL will facilitate automation of certain low-level vigilance tasks, freeing up human cognition for abstract thinking, empathy, and communication. We implemented this language and evaluated its design by writing prescriptions in the new language and administering a usability survey to medical professionals. This evaluation suggests that medical prescriptions can be conveyed by a programming languages mode of expression and provides useful information for refining the language. Analysis of the survey results suggests that medical professionals can understand and correctly modify programs in POP-PL. We also identified opportunities for refining POP-PL.
We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure, which provides no room for tradeoff between preprocessing and query time. Our contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time.
Static backward slicing of non-deterministic programs and systems
We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. The core of our approach is a specification style that prescribes a way to assign a level expression to each method such that each callees level is below the callers, even in the presence of dynamic binding. The specification style yields specifications that properly hide implementation details. The main idea is to use multisets of method names as levels, and to associate with each object levels that abstractly reflect the way the object is built from other objects. A methods level is then defined in terms of the methods own name and the levels associated with the objects passed as arguments. We first present the specification style in the context of programs that do not modify object fields. We then combine it with separation logic and abstract predicate families to obtain an approach for programs with heap mutation. In a third step, we address concurrency, by incorporating an existing approach for verifying deadlock-freedom of channels and locks. Our main contribution here is to achieve information hiding by using the proposed termination levels for lock ordering as well. Also, we introduce call permissions to enable elegant verification of termination of programs where threads cause work in other threads, such as in thread pools or fine-grained concurrent algorithms involving compare-and-swap loops. We explain how our approach can be used also to verify liveness of non-terminating programs.
We present Armus, a verification tool for dynamically detecting or avoiding barrier deadlocks. The core design of Armus is based on phasers, a generalisation of barriers that supports split-phase synchronisation, dynamic membership, and optional-waits. This allows Armus to handle the key barrier synchronisation patterns found in modern languages and libraries. We implement Armus for X10 and Java, giving the first sound and complete barrier deadlock verification tools in these settings. Armus introduces a novel event-based graph model of barrier concurrency constraints that distinguishes between task-event and event-task dependencies. Decoupling these two kinds of dependencies facilitates the verification of distributed barriers with dynamic membership, a challenging feature of X10. Our base representation can dynamically switch between a task-to-task model, Wait-for Graph (WFG), and an event-to- event model, State Graph (SG), to improve the scalability of the analysis. Formally, we show that the verification is sound and complete with respect to the occurrence of deadlock in our core phaser language; and that switching graph representations preserves the soundness and completeness properties. These results are machine checked with the Coq proof assistant. Practically, we evaluate the runtime overhead of our implementations using three benchmark suites in local and distributed scenarios. Regarding deadlock detection, distributed scenarios show negligible overheads and local scenarios show overheads below 1.15×. Deadlock avoidance is more demanding, and highlights the potential gains from dynamic graph selection. In one benchmark scenario, the runtime overheads vary from: 1.8× for dynamic selection, 2.6× for SG-static selection, and 5.9× for WFG-static selection.