Research Interests

My main research field is static analysis of programs, both abstract-interpretation based and type based.

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

In the past, I also developed several analyses for the parallel-functional language Eden as part of my Phd. Thesis.

 

Refereed Publications

2010

  • 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

    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.

  • M. Montenegro, R. Peña, C. Segura
    A Simple Region Inference Algorithm for a First-Order Functional Language
    18th International 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.

2009

  • M. Montenegro, R. Peña, C. Segura
    An Inference Algorithm for Guaranteeing Safe Destruction
    18th International Symposium on 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 Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
    17th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2008. ENTCS 246, pages 167-182. Elsevier.
    The original publication is available at www.sciencedirect.com
    .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.

2008

  • M. Montenegro, R. Peña, C. Segura
    A Type System for Safe Memory Management and its Proof of Correctness
    10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2008, pages 152-162. ACM Press.
    The original publication is available at dl.acm.org
    .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.

2007

  • R. Peña, C. Segura, M. Montenegro
    A Sharing Analysis for Safe
    Trends in Functional Programming, volume 7. Selected papers of 7th Symposium on Trends in Functional Programming, TFP 2006, 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.
  • C. Segura, C. Torrano
    Using Template Haskell for Abstract Interpretation
    15th International Workshop on Functional and Constraint Logic Programming, WFLP 2006, ENTCS 177, pages 201-217, Elsevier, 2007.
    The original publication is available at www.sciencedirect.com
    .pdf    View abstract
    Abstract Close

    Metaprogramming consists of writing programs that generate or manipulate other programs. Template Haskell is a recent extension of Haskell, currently implemented in the Glasgow Haskell Compiler, giving support to metaprogramming at compile time. Our aim is to apply these facilities in order to statically analyse programs and transform them at compile time. In this paper we use Template Haskell to implement an abstract interpretation based strictness analysis and a let-to-case transformation that uses the results of the analysis. This work shows the advantages and disadvantages of the tool in order to incorporate new analyses and transformations into the compiler without modifying it.

    Keywords: Meta-programming, Template Haskell, abstract interpretation, strictness analysis.

2006

  • R. Peña, C. Segura
    Reasoning about Skeletons in Eden
    Parallel Computing and Future Issues of High-End Computing, PARCO 2005, NIC Series Volume 33, pages 851-858, John von Neumann Institute for Computing, 2006.
    .pdf    View abstract
    Abstract Close

    The parallel-functional language Eden extends the lazy functional language Haskell by constructs to explicitly define and launch processes. Skeletons can be implemented in the language itself and can be invoked in parallel applications as higher-order functions. So, Eden can be used both as a system-level implementation language and as an application-level parallel one. In order to be useful, skeletons should be proved correct and should lead to an efficient use of the underlying machine. The paper presents examples of system-level programming in Eden, showing the conciseness of defining skeletons at a high level of abstraction. Efficiency reasoning is provided by accurate cost models and correctness is proved by induction proofs. If the parallel program uses finite data structures, the proof implies also successful termination. If it uses infinite ones (i.e. streams), the proof implies productivity. A program is productive if, whenever it receives continuous input, it provides continuous output. Productivity amounts to deadlock freedom.

  • F. Rosa and C. Segura and A. Verdejo
    Typed Mobile Ambients in Maude
    6th International Workshop on Rule-Based Programming, RULE 2005, ENTCS 147(1), pages 135-161, Elsevier, 2006.
    The original publication is available at www.sciencedirect.com
    A web page with additional code
    .pdf    View abstract    Extended version
    Abstract Close

    Maude has revealed itself as a powerful tool for implementing different kinds of semantics so that quick prototypes are available for trying examples and proving properties. In this paper we show how to define in Maude two semantics for Cardelli and Gordon's Ambient Calculus. The first one is the operational (reduction) semantics which requires the definition of Maude strategies in order to avoid infinite loops. The second one is a type system defined by Cardelli and Gordon to avoid communication errors. The correctness of that system was not formally proved. We enrich the operational semantics with error rules and prove that well-typed processes do not produce such errors. The type system is highly non-deterministic. We show here one possible way of implementing such non-determinism in the rules.

2005

  • F. Rosa and C. Segura and D. de Frutos-Escrig 
    Tagged systems : a framework for the specification of history-dependent properties
    ENTCS 137(1), pages 151-174, Elsevier, 2005.
    The original publication is available at www.sciencedirect.com
    .pdf    View abstract
    Abstract Close

    We propose a general method for the treatment of history-dependent runtime errors. When one has to control this kind of errors, a tagged version of the language is usually defined, in which tags capture only the necessary information of the history of processes. We will characterize such tagged languages as being quotients of the reachability tree defined by the computations of the original language. From this fact we can conclude that the property characterized by each tagged language is indeed a property of the original one. In this way, we can work in a common framework, instead of defining an ad hoc semantics for each property. In particular, we could still use the analysis machinery existing in the calculus in order to prove that or other related properties. We have applied this methodology to the study of resource access control in a distributed pi-calculus, called Dpi. In particular, we have proved that the tagged version of Dpi is indeed a tagging according to our definition.

  • R. Peña and C. Segura
    Non-determinism Analyses in a Parallel-Functional Language
    Journal of Functional Programming, 15(1), pages 67-100, Cambridge University Press, 2005.
    The original publication is available at journals.cambridge.org
    .pdf    View abstract
    Abstract Close

    The parallel-functional language Eden has a non-deterministic construct, the process abstraction merge, which interleaves a set of input lists to produce a single non-deterministic list. Its non-deterministic behaviour is a consequence of its reactivity: it immediately copies to the output list any value appearing at any of the input lists. This feature is essential in reactive systems and very useful in some deterministic parallel algorithms. The presence of non-determinism creates some problems such that some internal transformations in the compiler must be disallowed. The paper describes several non-determinism analyses developed for Eden aimed at detecting the parts of the program that, even in the presence of a process merge, still exhibit a deterministic behaviour. A polynomial cost algorithm which annotates Eden expressions is described in detail. A denotational semantics is described for Eden and the correctness of all the analyses is proved with respect to this semantics.

2004

  • C. Segura and R. Peña
    Correctness of Non-determinism Analyses in a Parallel-Functional Language
    15th International Workshop on Implementation of Functional Languages, IFL 2003, LNCS vol. 3145, pages 69-85, Springer-Verlag, 2004.
    The original publication is available at www.springerlink.com
    .pdf    View abstract    Extended version
    Abstract Close

    The presence of non-determinism in the parallel-functional language Eden creates some problems. Several non-determinism analyses have been developed to determine when an Eden expression is sure to be deterministic, and when it may be non-deterministic. The correctness of these analyses had not been proved yet. In this paper we define a “maximal” denotational semantics for Eden in the sense that the set of possible values produced by an expression is bigger than the actual one. This semantics is enough to prove the correctness of the analyses. We provide the abstraction and concretisation functions relating the concrete and abstract values so that the determinism property is adequately captured. Finally we prove the correctness of the analyses with respect to the previously defined semantics.

2002

  • R. Peña  and C. Segura
    A Polynomial-Cost Non-determinism Analysis
    13th International Workshop on Implementation of Functional Languages, IFL 2001, LNCS vol. 2312, pages 121-137, Springer-Verlag, 2002.
    The original publication is available at www.springerlink.com
    .pdf    View abstract    Extended version
    Abstract Close

    This paper is an extension of a previous workwhere two non-determinism analyses were presented. One of them was efficient but not very powerful and the other one was more powerful but very expensive. Here, we develop an intermediate analysis in both aspects, efficiency and power. The improvement in efficiency is obtained by speeding up the fixpoint calculation by means of a widening operator, and the representation of functions through easily comparable signatures. Also details about the implementation and its cost are given.

  • R. Peña  and C. Segura
    Sized Types for Typing Eden Skeletons
    13th International Workshop on Implementation of Functional Languages, IFL 2001, LNCS vol. 2312, pages 1-17, Springer-Verlag, 2002.
    The original publication is available at www.springerlink.com
    .pdf    View abstract
    Abstract Close

    The parallel-functional language Eden extends Haskell with constructs to explicitly define and communicate processes. These extensions allow the easy definition of skeletons as higher-order functions. However, the programmer can inadvertently introduce busy loops or deadlocks in them. In this paper a sized type system is extended in order to use it for Eden programs, so that those well-typed skeletons are guaranteed either to terminate or to be productive. The problems raised by Eden features and their possible solutions are described in detail, and several skeletons are manually type checked in this modified system such as the parallel map, farm, pipeline, and replicated workers.

  • R. Peña  and F. Rubio and C. Segura
    Deriving Non-hierarchical Process Topologies
    3rd International Scottish Functional Programming Workshop, SFP 2001, Trends in Functional Programming Volume 3, pages 51-62, Intellect, 2002.
    .pdf    View abstract
    Abstract Close

    Eden is a parallel functional language which extends Haskell with new expressions to define and instantiate processes. These extensions allow the easy definition of parallel process topologies as higher order functions. Unfortunately, by only using process abstractions and instantiations it is not possible to implement non-hierarchical topologies, as processes can only communicate with its parent or its children. In this paper we show how to implement non-hierarchical topologies in Eden by using its dynamic channels. The topologies will be specified by only using process abstractions and instantiations, so that they will really be hierarchical. Afterwards, they will be refined into really non-hierarchical topologies using the dynamic reply channels. The usefulness of the translation method will be shown by examples, highlighting the key points to be taken into account to achieve the desired behaviour.

2001

  • C. Pareja, R. Peña , F. Rubio and C. Segura
    Adding Traces to a Lazy Monadic Evaluator
    8th International Workshop on Computer Aided Systems, EUROCAST 2001, LNCS vol. 2178, pages 627-641, Springer-Verlag, 2001.
    The original publication is available at www.springerlink.com
    .pdf    View abstract
    Abstract Close

    The debugging of lazy functional programs is a non yet satisfactorily solved problem. Different approaches have been proposed during the last years, all of them having a property in common: The graph produced by the traced program is different from the original graph, i.e. the one without traces. In this paper we propose a cleaner and more modular approach to the trace problem. We regard traces as observations of the program and at the same time we want to preserve the original graph. In this way, a clean separation between the trace and the program being observed is established. Consequently, there may be variables in the trace referencing parts of the graph (i.e. pointers from the trace to the graph), but not the other way around. By doing so the correctness is guaranteed, as the normal execution process is not altered. In order to reach this goal, a monadic approach is followed. The success of the approach is shown by simulating three up-to-date Haskell tracers.

  • R. Peña  and C. Segura
    Non-determinism analysis in a parallel-functional language
    12th International Workshop on Implementation of Functional Languages, IFL2001, LNCS vol. 2011, pages 1-18, Springer-Verlag, 2001.
    The original publication is available at www.springerlink.com
    .pdf    View abstract    Extended version
    Abstract Close

    The paper presents several analyses to detect non-deterministic expressions in the parallel-functional language Eden. First, the need for the analysis is motivated, and then each one is presented. The first one is type-based, while the other two are based on abstract interpretation. Their power and efficiency is discussed, and an example is used to illustrate the differences. Two interesting functions to adapt abstract values to types appear, and they happen to be a Galois insertion.

2000

  • C. Pareja and R. Peña  and F. Rubio and C. Segura
    Optimizing Eden by Transformation
    2nd Scottish Functional Programming Workshop, SFP 2000, Trends in Functional Programming Volume 2, pages 13-26, Intellect, 2000.
    .pdf    View abstract    Extended version
    Abstract Close

    Eden is a parallel extension of Haskell allowing the programmer to explicitly specify which expressions must be evaluated as parallel processes. Eden is implemented by modifying the Glasgow Haskell Compiler (GHC). This decision has saved a lot of work but has also produced some drawbacks: Some optimizing transformations done by GHC are not convenient for Eden, either because they spoil its semantics or because they negatively affect its ef£ciency. The paper explains how to circumvent these drawbacks and also how to add our own optimizing analysis and transformation steps in order to generate a (correct and) better parallel code.

  • U. Klusik and R. Peña  and C. Segura
    Bypassing of Channels in Eden
    1st Scottish Functional Programming Workshop, SFP 1999, Trends in Functional Programming Volume 1, pages 2-10, Intellect, 2000.
    .pdf    View abstract    Extended version
    Abstract Close

    We describe automatic bypassing, an optimization of Eden’s implementation to reduce the number of messages and/or threads at runtime. Eden [BLOP97] extends the lazy functional language Haskell with a set of coordination features, aimed to express parallel algorithms. These include process abstractions (or process schemes) and process instantiations (or applications of a process scheme to actual inputs). When a new process is instantiated, their input and output channels are connected to its parent process. This implies that, in principle, only tree–like process topologies can be created. But the aimed topology may not be tree–like (e.g. pipelines, grids, etc.). It is desirable to be able to connect every producer to its actual consumer, trying to avoid the intermediate processes frequently used only to set up the topology. The strategy consists of a combination of compile time analysis and runtime support. Both are explained in detail. Also, the savings expected with the proposed strategy are commented.

 

Ph.D. & Master Thesis

  • C. Segura
    Análisis de Programas en Lenguajes Funcionales Paralelos (Program Analyses in Parallel Functional Languages)
    Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid, 2001.
    It was mandatory to write it in Spanish but you can find here a summary of the chapters written in english and links to the relevant publications. My supervisor was Ricardo Peña Marí.
    .ps   
  • C. Segura
    Técnicas de análisis de Programas en Lenguajes Funcionales Paralelos
    Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid, 1999.
    .ps