Correas Fernández, Jesús

Profile Picture
First Name
Last Name
Correas Fernández
Universidad Complutense de Madrid
Faculty / Institute
Estudios estadísticos
Sistemas Informáticos y Computación
Lenguajes y Sistemas Informáticos
UCM identifierORCIDScopus Author IDDialnet IDGoogle Scholar ID

Search Results

Now showing 1 - 10 of 15
  • Publication
    Static Inference of Transmission Data Sizes in Distributed Systems
    (2014-10) Albert Albiol, Elvira; Correas Fernández, Jesús; Martín Martín, Enrique; Román Díez, Guillermo
    We present a static analysis to infer the amount of data that a distributed system may ransmit. The different locations of a distributed system communicate and coordinate their actions by posting tasks among them. A task is posted by building a message with the task name and the data on which such task has to be executed. When the task completes, the result can be retrieved by means of another message from which the result of the computation can be obtained. Thus, the transmission data size of a distributed system mainly depends on the amount of messages posted among the locations of the system, and the sizes of the data transferred in the messages. Our static analysis has two main parts: (1) we over-approximate the sizes of the data at the program points where tasks are spawned and where the results are received, and (2) we over-approximate the total number of messages. Knowledge of the transmission data sizes is essential, among other things, to predict the bandwidth required to achieve a certain response time, or conversely, to estimate the response time for a given bandwidth. A prototype implementation in the SACO system demonstrates the accuracy and feasibility of the proposed analysis.
  • Publication
    Non-Cumulative Resource Analysis (Author’s version)
    (Springer, 2015) Albert Albiol, Elvira; Correas Fernández, Jesús; Román Díez, Guillermo
    Existing cost analysis frameworks have been defined for cumulative resources which keep on increasing along the computation. Traditional cumulative resources are execution time, number of executed steps, amount of memory allocated, and energy consumption. Noncumulative resources are acquired and (possibly) released along the execution. Examples of non-cumulative cost are memory usage in the presence of garbage collection, number of connections established that are later closed, or resources requested to a virtual host which are released after using them. We present, to the best of our knowledge, the first generic static analysis framework to infer an upper bound on the peak cost for non-cumulative types of resources. Our analysis comprises several components: (1) a pre-analysis to infer when resources are being used simultaneously, (2) a program-point resource analysis which infers an upper bound on the cost at the points of interest (namely the points where resources are acquired) and (3) the elimination from the upper bounds obtained in (2) of those resources accumulated that are not used simultaneously. We report on a prototype implementation of our analysis that can be used on a simple imperative language.
  • Publication
    Peak Cost Analysis of Distributed Systems (Author's version)
    (2014-08) Albert Albiol, Elvira; Correas Fernández, Jesús; Román Díez, Guillermo
    We present a novel static analysis to infer the peak cost of distributed systems. The different locations of a distributed system communicate and coordinate their actions by posting tasks among them. Thus, the amount of work that each location has to perform can greatly vary along the execution depending on: (1) the amount of tasks posted to its queue, (2) their respective costs, and (3) the fact that they may be posted in parallel and thus be pending to execute simultaneously. The peak cost of a distributed location refers to the maximum cost that it needs to carry out along its execution. Inferring the peak cost is challenging because it increases and decreases along the execution, unlike the standard notion of total cost which is cumulative. Our key contribution is the novel notion of quantified queue configuration which captures the worst-case cost of the tasks that may be simultaneously pending to execute at each location along the execution. A prototype implementation demonstrates the accuracy and feasibility of the proposed peak cost analysis.
  • Publication
    Resource Analysis: From Sequential to Concurrent and Distributed Programs
    (2015-06) Albert Albiol, Elvira; Arenas Sánchez, Puri; Correas Fernández, Jesús; Genaim, Samir; Gómez Zamalloa, Miguel; Martín Martín, Enrique; Puebla, Germán; Román Díez, Guillermo
    Resource analysis aims at automatically inferring upper/lower bounds on the worst/best-case cost of executing programs. Ideally, a resource analyzer should be parametric on the cost model, i.e., the type of cost that the user wants infer (e.g., number of steps, amount of memory allocated, amount of data transmitted, etc.). The inferred upper bounds have important applications in the fields of program optimization, verification and certification. In this talk, we will review the basic techniques used in resource analysis of sequential programs and the new extensions needed to handle concurrent and distributed systems.
  • Publication
    Parallel Cost Analysis of Distributed Systems
    (2015-09) Albert Albiol, Elvira; Correas Fernández, Jesús; Johnsen, Einar Broch; Román Díez, Guillermo
    We present a novel static analysis to infer the parallel cost of distributed systems. Parallel cost differs from the standard notion of serial cost by exploiting the truly concurrent execution model of distributed processing to capture the cost of synchronized tasks executing in parallel. It is challenging to analyze parallel cost because one needs to soundly infer the parallelism between tasks while accounting for waiting and idle processor times at the different locations. Our analysis works in three phases: (1) It first performs a block-level analysis to estimate the serial costs of the blocks between synchronization points in the program; (2) Next, it constructs a distributed ow graph (DFG) to capture the parallelism, the waiting and idle times at the locations of the distributed system; Finally, (3) the parallel cost can be obtained as the path of maximal cost in the DFG. A prototype implementation demonstrates the accuracy and feasibility of the proposed analysis.
  • Publication
    A Multi-Domain Incremental Analysis Engine and its Application to Incremental Resource Analysis
    (Elsevier, 2015-06) Albert Albiol, Elvira; Correas Fernández, Jesús; Puebla, Germán; Román Díez, Guillermo
    The aim of incremental analysis is, given a program, its analysis results, and a series of changes to the program, to obtain the new analysis results as eficiently as possible and, ideally, without having to (re-)analyze fragments of code which are not affected by the changes. Incremental analysis can significantly reduce both the time and the memory requirements of analysis. The first contribution of this article is a multi-domain incremental fixed-point algorithm for a sequential Java-like language. The algorithm is multi-domain in the sense that it interleaves the (re-)analysis for multiple domains by taking into account dependencies among them. Importantly, this allows the incremental analyzer to invalidate only those analysis results previously inferred by certain dependent domains. The second contribution is an incremental resource usage analysis which, in its first phase, uses the multi-domain incremental fixed-point algorithm to carry out all global pre-analyses required to infer cost in an interleaved way. Such resource analysis is parametric on the cost metrics one wants to measure (e.g., number of executed instructions, number of objects created, etc.). Besides, we present a novel form of cost summaries which allows us to incrementally reconstruct only those components of cost functions affected by the changes. Experimental results in the costa system show that the proposed incremental analysis provides significant performance gains, ranging from a speedup of 1.48 up to 5.13 times faster than non-incremental analysis.
  • Publication
    Quantified Abstract Configurations of Distributed Systems
    (Springer, 2014-11) Albert Albiol, Elvira; Correas Fernández, Jesús; Puebla, Germán; Román Díez, Guillermo
    When reasoning about distributed systems, it is essential to have information about the different kinds of nodes that compose the system, how many instances of each kind exist, and how nodes communicate with other nodes. In this paper we present a static-analysis-based approach which is able to provide information about the questions above. In order to cope with an unbounded number of nodes and an unbounded number of calls among them, the analysis performs an abstraction of the system producing a graph whose nodes may represent (infinitely) many concrete nodes and arcs represent any number of (infinitely) many calls among nodes. The crux of our approach is that the abstraction is enriched with upper bounds inferred by resource analysis that limit the number of concrete instances that the nodes and arcs represent and their resource consumption. The information available in our quantified abstract configurations allows us to define performance indicators which measure the quality of the system. In particular, we present several indicators that assess the level of distribution in the system, the amount of communication among distributed nodes that it requires, and how balanced the load of the distributed nodes that compose the system is. Our performance indicators are given as functions on the input data sizes, and they can be used to automate the comparison of different distributed settings and guide towards finding the optimal configuration.
  • Publication
    AuxAula: contruyendo puentes entre alumno y profesor. Transformar la distracción en productividad
    (2019) Montoto Jáuregui, Carlos; Correas Fernández, Jesús
    La rápida evolución de la tecnología móvil y su democratización, debido al decremento de su coste y a su alta variedad de gamas en el mercado; junto a la inexistencia de una educación de manejo responsable y a su uso inadecuado, han conllevado a que las nuevas generaciones cada vez tengan mayor dependencia de estos dispositivos. Este uso continuado afecta, en consecuencia, a muchos aspectos de nuestras vidas, incluyendo las relaciones personales, laborales o académicas. El objetivo de este proyecto es el de desarrollar una herramienta que, utilizando el potencial positivo de esta tecnología, ayude a los usuarios a disminuir las distracciones y a enfocar su atención, inhibiendo factores disruptivos de la concentración mostrando, de forma transparente, el uso del dispositivo y utilizando métodos de la educación dinámica. Para ello, tras realizar un estudio de la situación actual, se ha diseñado e implementado el prototipo de una aplicación académica para alumnos y profesores, que, utilizando los métodos ya mencionados, incremente los resultados del aprendizaje en el aula, a la par que intenta construir buenos hábitos de uso y recuperar la confianza en la tecnología.
  • Publication
    Evaluación del impacto sobre el aprendizaje de bases de datos del juez automático LearnSQL
    (2022) Martín Martín, Enrique; Correas Fernández, Jesús; Garmendia Salvador, Luis; Montenegro Montes, Manuel; Riesco Rodríguez, Adrián; Rubio Cuéllar, Rubén Rafael; Sáenz Pérez, Fernando
    Utilizamos el juez automático "LearnSQL" en la docencia de varios grupos de la asignatura "Bases de Datos" y medimos de manera rigurosa y extensiva el impacto que este tiene sobre el aprendizaje de los estudiantes.
  • Publication
    SQLab Extension: Laboratorio virtual lenguaje SQL
    (2019-03-14) García Merayo, María de las Mercedes; Núñez García, Manuel; Estévez Martín, Sonia; Martínez Torres, Rafael; Ibias Martínez, Alfredo; Pareja Flores, Cristobal; Rincón Martínez, Santiago; Correas Fernández, Jesús
    Extensión de la plataforma SQLab con nuevas funcionalidades que permitan a estudiantes de Bases de Datos evaluar sus conocimientos de diseño de instrucciones DML del lenguaje SQL y a los docentes hacer un seguimiento de la evolucion de sus alumnos.