Research Interests

My main research field is memory management in functional languages, particularly pointer safety and memory consumption analysis. I work on the Safe project, a research platform aimed at investigating the suitability of functional languages for programming devices with strict memory requirements.

Safe is a first-order functional programming language which provides semiexplicit memory management through two mechanisms: region-based memory management (inferred by the compiler) and destructive pattern matching (specified by the programmer). We have designed a static analysis guaranteeing the absence of dangling pointers due to the latter. Now we are developing an abstract interpretation-based static analysis for inferring upper bounds of the memory consumption (heap and stack) of Safe programs.

 

Refereed Publications

2011

  • M. Montenegro, O. Shkaravska, M. van Eekelen, R. Peña
    Interpolation-based height analysis for improving a recurrence solver
    Draft proceedings of the 2nd Workshop on Foundational and Practical Aspects of Resource Analysis, FOPARA 2011, Tech. report SIC-08/11. Dept. Computer Systems and Computing. Universidad Complutense de Madrid, pages 96-110.
    Accepted for publication in Springer LNCS series (To appear)
    The original publication is available here
    .pdf    View abstract   

  • Abstract Close

    The COSTA system infers resource consumption bounds from Java bytecode using an internal recurrence solver PUBS. This paper suggests an improvement of the COSTA system, such that it can solve a larger number of recurrences. The idea is to replace one of its static analyses, the ranking function analysis, by another kind of analysis, height analysis, in such a way that polynomial bounds of any degree may be inferred instead of just linear expressions. The work can be seen as an application of some polynomial interpolation techniques used by some of the authors in prior analyses. Finding a way to choose proper test nodes is the key to the solution presented in this paper.

2010

  • J. de Dios, M. Montenegro, R. Peña
    Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
    8th International Conference on Integrated Formal Methods, IFM 2010, LNCS vol. 6396, pages 305-319. Springer Verlag.
    The original publication is available at www.springerlink.com
    .pdf    View abstract    Extended version (Tech. Report)

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

  • 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 35-50. Springer Verlag.
    .pdf    View abstract    Extended version

  • 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

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

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

  • 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

  • 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

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

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

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

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.
 

Ph.D. Thesis

Master's Thesis

  • Inferencia de tipos seguros en un lenguaje funcional con destrucción explícita de memoria
    M. Montenegro (supervisors: R. Peña and C. Segura)
    Defended: September 2007
    .pdf
    It is written in Spanish and contains a previous version of the inference algorithm shown in [LOPSTR'08]. It also describes some implementation aspects of the sharing analysis [TFP'06] and a variant of HM-inference involving latent unifications and region type inequalities.