Refereed publications
2011
- J. de Dios, R. Peña
Certification of Safe Polynomial Memory Bounds
Int. Symp. on Formal Methods, FM'11, Limerick, (Ireland), June 2011, LNCS (to appear)
.pdf View abstract Extended version (Tech. Report)
| Abstract | Close |
|
In previous works, we have developed several algorithms for inferring upper bounds to heap and stack consumption for a simple functional language called \safe. The bounds inferred for a particular recursive function with $n$ arguments takes the form of symbolic $n$-ary functions from $(\miR)^n$ to $\miR$ relating the input argument sizes to the number of cells or words respectively consumed in the heap and in the stack. Most frequently, these functions are multivariate polynomials of any degree, although exponential and other functions can be inferred in some cases. Certifying memory bounds is important because the analyses could be unsound, or have been wrongly implemented. But the certifying process should not be necessarily tied to the method used to infer those bounds. Although the motivation for the work presented here is certifying the bounds inferred by our compiler, we have developed a certifying method which could equally be applied to bounds computed by hand. The certification process is divided into two parts: (a) an off-line part consisting of proving the soundness of a set of proof rules. This part is independent of the program being certified, and its correctness is established once forever by using the proof assistant \isab; and (b) a compile-time program-specific part in which the proof rules are applied to a particular program and their premises proved correct. The key idea for the first part is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the symbolic information asserted by the proof-rule to the dynamic properties about the heap and stack consumption satisfied at runtime. For the second part, we use a mathematical tool for proving instances of the Tarski decision problem on quantified formulas in real closed fields. |
|
2010
- J. de Dios, M. Montenegro, R. Peña
Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
8th Int. Conf. on Integrated Formal Methods, IFM 2010, LNCS 6396, pp. 305-319
The original publication is available at www.springerlink.com
.pdf View abstract Extended version (Tech. Report)
Isabelle/HOL theories - M. Montenegro, R. Peña, C. Segura
A Space Consumption Analysis by Abstract Interpretation
1st International Workshop on Foundational and Practical Aspects of Resource Analysis, FOPARA 2009 LNCS vol. 6324, pages 34-50. Springer Verlag
The original publication is available at www.springerlink.com
.pdf View abstract Extended version
| Abstract | Close |
|
Here we present how to generate formal certificates about the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/HOL proof scripts which can be proof-checked by this tool when loaded with a database of previously proved theorems. The key idea is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the static types inferred by the compiler to the dynamic properties about the heap that will be satisfied at runtime. |
|
| Abstract | Close |
|
In this paper we present a new analysis aimed at inferring upper bounds for heap and stack consumption. It is based on abstract interpretation, being the abstract domain the set of all n-ary monotonic functions from real non-negative numbers to a real non-negative result. This domain turns out to be a complete lattice under the usual relation on functions. Our interpretation is monotonic in this domain and the solution we seek is the least fixpoint of the interpretation. We first explain the abstract domain and some correctness properties of the interpretation rules with respect to the language semantics, then present the inference algorithms for recursive functions, and finally illus- trate the approach with the upper bounds obtained by our implementa- tion for some case studies. |
|
2009
- M. Montenegro, R. Peña, C. Segura
A Simple Region Inference Algorithm for a First-Order Functional Language
18th Int'l Workshop on Functional and (Constraint) Logic Programming, WFLP 2009, LNCS vol. 5979, pages 145-161. Springer Verlag
The original publication is available at www.springerlink.com
.pdf View abstract Extended version - J. de Dios, R. Peña, M. Montenegro
Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
IX Jornadas sobre Programación y Lenguajes, PROLE'09, San Sebastián, Spain, September 2009, pages 65-74
.pdf View abstract - M. Montenegro, R. Peña, C. Segura
Experiences in developing a compiler for Safe using Haskell
I Taller de Programación Funcional, TPF'09, San Sebastián, Spain, September 2009, pages 31-46
.pdf View abstract -
J. de Dios, R. Peña
A Certified Implementation on Top of the Java Virtual Machine
Formal Methods for Industrial Critical Systems, FMICS'09. LNCS vol. 5825, pages 181-196. Springer Verlag.
The original publication is available at www.springerlink.com
Isabelle/HOL theories -
J. de Dios, R. Peña
Formal Certification of a Resource-Aware Language Implementation
Theorem Proving in Higher Order Logics, TPHOL'09. LNCS vol. 5674, pages 196-211. Springer Verlag.
The original publication is available at www.springerlink.com
Isabelle/HOL theories
| Abstract | Close |
|
In this paper we present an inference algorithm for annotating programs with regions which is both simpler to understand and more efficient than other related algorithms. Programmers are assumed to write programs and to declare datatypes without any reference to regions. The algorithm decides the regions needed by every function. It also allows polymorphic recursion with respect to regions. We show convincing examples of programs before and after region annotation, prove the correctness and optimality of the algorithm, and give its asymptotic cost. Keywords: Memory management, type-based analysis, formal certificates, proof assistants. |
|
| Abstract | Close |
|
Safe is a first-order eager functional language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures. A region is a collection of cells, each one is big enough to allocate a data constructor. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in constant time. Deallocating cells or regions may create dangling pointers. The language is aimed at inferring and certifying memory safety properties in a Proof Carrying Code environment. Some of its analyses have been presented elsewhere. The one relevant to this paper is a type system and a type inference algorithm guaranteeing that well-typed programs will be free of dangling pointers at runtime. In this paper we present how to generate formal certificates of the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/HOL proof scripts which can be proof-checked by this tool when loaded with a database of previously proved theorems. The key idea is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the static types inferred by the compiler to the dynamic properties about the heap that will be satisfied at runtime. Keywords: Memory management, type-based analysis, formal certificates, proof assistants. |
|
| Abstract | Close |
|
Safe is an eager language introduced as a research platform for programming small devices and embedded systems with strict memory requirements. It follows a semi-explicit approach to memory control combining regions and a deallocation construct but with a very low effort from the programmer's point of view. Here we describe our experiences in implementing a compiler for Safe using Haskell. We show how polymorphism, higher-order functions, monads and different kinds of libraries have been useful in the implementation of all compiler phases. Keywords: Memory management, compiler implementation. |
|
2008
- R. Peña, D. Rupérez
A Certified Implementation of a Functional Virtual Machine on top of the Java Virtual Machine
Jornadas sobre Programación y Lenguajes, PROLE'08, Gijón, Spain, October 2008, pages 131-140
.pdf View abstract - M. Montenegro, R. Peña, C. Segura
An Inference Algorithm for Guaranteeing Safe Destruction
Logic-Based Program Synthesis and Transformation, LOPSTR'08. LNCS vol. 5438, pages 135-151. Springer Verlag.
The original publication is available at www.springerlink.com
.pdf View abstract Extended version - M. Montenegro, R. Peña, C. Segura
A Type System for Safe Memory Management and its Proof of Correctness
Proceedings of ACM Symposium on Principles and Practice of Declarative Programming, PPDP'08, pages 152-162. ACM Press.
.pdf View abstract Extended version - M. Montenegro, R. Peña, C. Segura
A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008). ENTCS vol. 246, pages 167-182. Elsevier.
.pdf View abstract Extended version - S. Lucas, R. Peña
Rewriting Techniques for Analysing Termination and Complexity Bounds of Safe Programs
Informal proceedings of Logic-Based Program Synthesis and Transformation, LOPSTR'08, Valencia, Spain, July 2008, pages 43-57
.pdf View abstract
| Abstract | Close |
|
As part of a bigger project, we have defined the virtual machine SVM (Safe Virtual Machine) which is the target machine of the Safe compiler. Safe is a first-order functional language with unusual memory management features: memory is explicitly and implicitly deallocated at some specific points in the program text, and there is no need for a runtime garbage collector. We have implemented the SVM on top of the Java Virtual Machine (JVM) because Safe is embedded in a Proof Carrying Code (PCC) framework and the final code emitted by the Safe compiler should be Java bytecode. As one of the aims of Safe is providing certificates (mathematical proofs) for some program properties, we require this implementation to be also certified, i.e. the semantics of Safe must be preserved across all the translations. We have used the proof assistant Isabelle/HOL for this purpose. The paper presents ongoing work on this implementation: first an introduction to Safe and SVM is done; then the main decisions in order to map the SVM data structures to the JVM are explained. Finally, the Isabelle/HOL formalisations of SVM, JVM, and of the mapping between both are presented, and the main correctness theorem is stated. Keywords: Virtual machines, Java bytecode, proof carrying code, certification. |
|
| Abstract | Close |
|
Safe is a first-order eager functional language with destructive pattern matching controlled by the programmer. A previously presented type system is used to avoid dangling pointers arising from the inadequate usage of this facility. In this paper we present a type inference algorithm, prove its correctness w.r.t. the type system, describe its implementation and give a number of successfully typed examples. Keywords: memory management, Keywords: Memory management, type-based analysis, type inference. |
|
| Abstract | Close |
|
We present a destruction-aware type system for the functional language Safe, which is a first-order eager language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in constant time. The language is equipped with several analyses and inference algorithms so that regions, sharing information and types are automatically inferred by the compiler. Here, we concentrate on the correctness of the type system with respect to the operational semantics of the language. In particular, we prove that, in spite of sharing and of the use of implicit and explicit memory deallocation operations, all well-typed programs will be free of dangling pointers at runtime. The paper ends up with some examples of well-typed programs. Keywords: Type systems, safe memory deallocation. |
|
| Abstract | Close |
|
Safe is a first-order eager language with heap regions and unusual facilities such as programmer-controlled destruction and copying of data structures. The regions are disjoint parts of the heap where the compiler may allocate data structures. Thanks to regions, a runtime garbage collector is not needed. The language and its associated type system, guaranteeing that destruction facilities and region management are done in a safe way, have been presented previously. In this paper, we start from a high-level big-step operational semantics for Safe, and in a series of semiformal steps we derive its compilation to an imperative language and imperative abstract machine. Once the memory needs of the machine are known, we enrich the semantics with memory consumption annotations and prove that the enriched semantics is correct with respect to the translation and the abstract machine. All the steps are derived in such a way that it is easy to understand the translation and to formally establish its correctness. Keywords: Functional languages, Region based heaps, Abstract machines, Code generation. |
|
| Abstract | Close |
|
Safe is a first-order eager functional language with facilities for programmer-controlled destruction and copying of data structures and is intended for compile-time analysis of memory consumption. In Safe, heap and stack memory consumption during the evaluation of an expression f(e1,...,en) depends on the number of calls to f . Ensuring termination of Safe programs (or of particular function calls) is therefore essential to implement these analysis. Furthermore, being able to give bounds to the number of recursive calls required by a terminating initial call becomes essential in computing space bounds. In this paper, we first investigate how to analyze termination of Safe programs by using standard term rewriting techniques. First, we transform a Safe program into a term rewriting system. We provide a correct and complete transformation for that purpose, i.e., termination of the original Safe program P is completely characterized as (innermost) termination of the transformed TRS RP . Then, termination can be automatically analysed by means of existing tools such as AProVE, MU-TERM, or TTT. We provide explicit bounds for the number of calls which are issued during the evaluation of an expression as above. We also investigate how to use proofs of termination which combine the dependency pairs approach with polynomial interpretations to obtain such numeric bounds. Safe is an eager language introduced as a research platform for programming small devices and embedded systems with strict memory requirements. It follows a semi-explicit approach to memory control combining regions and a deallocation construct but with a very low effort from the programmer's point of view. Here we describe our experiences in implementing a compiler for Safe using Haskell. We show how polymorphism, higher-order functions, monads and different kinds of libraries have been useful in the implementation of all compiler phases. Keywords: Termination, Term Rewriting Systems, Space complexity. |
|
2006
- R. Peña, C. Segura, M. Montenegro
A Sharing Analysis for Safe
Selected Papers of Trends in Functional Programming, TFP'06, pages 109-128. Intellect.
.pdf View abstract
| Abstract | Close |
|
We present a sharing analysis for the functional language Safe. This is a first-order eager language with facilities for programmer-controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap where the programmer may allocate data structures. The analysis gives upper approximations to the sets of variables respectively sharing a recursive substructure, or any substructure, of a given variable. Its results will be used to guarantee that destruction facilities and region management are done in a safe way. In order to have a modular and efficient analysis, we provide signatures for functions, which summarize their sharing behaviour. The paper ends up describing the implementation of the analysis and some examples. Keywords: Memory management, compiler implementation. |
|
PhD Thesis
- M. Montenegro
Safety properties and memory bound analysis in a functional language without a garbage collector.
Universidad Complutense de Madrid. November 18, 2011.
.pdf