Docta Complutense :: Browsing by Author "Albert Albiol, Elvira"

Browsing by Author "Albert Albiol, Elvira"

Now showing 1 - 17 of 17

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.
A practical comparator of cost functions and its applications
(Elsevier, 2015-11) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Genaim, Samir; Puebla, Germán
Automatic cost analysis has significantly advanced in the last few years. Nowadays, a number of cost analyzers exist which automatically produce upperand/ or lower-bounds on the amount of resources required to execute a program.Cost analysis has a number of important applications such as resource-usage verification and program synthesis and optimization. For such applications to be successful, it is not suficient to have automatic cost analysis. It is also required to have automated means for handling the analysis results, which are in the form of Cost Functions (CFs for short) i.e., non-recursive expressions composed of a relatively small number of types of basic expressions. In particular, we need automated means for comparing CFs in order to prove that a CF is smaller than or equal to another one for all input values of interest. General function comparison is a hard mathematical problem. Rather than attacking the general problem, in this work we focus on comparing CFs by exploiting their syntactic properties and we present, to the best of our knowledge, the first practical CF comparator which opens the door to fully automated applications of cost analysis. We have implemented the comparator and made its source code available online, so that any cost analyzer can use it.
A Transformational Approach to Resource Analysis with Typed-Norms
(2014-12) Albert Albiol, Elvira; Genaim, Samir; Gutiérrez, Raúl
In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along a program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent thesizes of the corresponding data. When norms are de_ned by taking typeinformation into account, they are named typed-norms. The main contributionof this paper is a transformational approach to resource analysiswith typed-norms. The analysis is based on a transformation of the programinto an intermediate abstract program in which each variable isabstracted with respect to all considered norms which are valid for itstype. We also sketch a simple analysis that can be used to automaticallyinfer the required, useful, typed-norms from programs.
Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing
(2014-05) Albert Albiol, Elvira; Arenas Sánchez, Puri; Gómez Zamalloa, Miguel
Testing concurrent systems requires exploring all possible non-deterministic interleavings that the concurrent execution may have. This is because any of the interleavings may reveal the erroneous behaviour. In testing of actor systems, we can distinguish two sources of non-determinism: (1) actor-selection, the order in which actors are explored and (2) task-selection, the order in which the tasks within each actor are explored. This paper provides new strategies and heuristics for pruning redundant state-exploration when testing actor systems by reducing the amount of unnecessary non-determinism. First, we propose a method and heuristics for actor-selection based on tracking the amount and the type of interactions among actors. Second, we can avoid further redundant interleavings in task-selection by taking into account the access to the shared-memory that the tasks make.
Aplicación del sistema jPET para la generación automática de tests en asignaturas de programación con Java
(2016-01) Gómez-Zamalloa Gil, Miguel; Albert Albiol, Elvira; Arenas Sánchez, Purificación; Correas Fernández, Jesús; Genaim, Samir; Román Díez, Guillermo
Conditional Termination of Loops over Heap-Allocated Data
(Elsevier, 2014-10) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Genaim, Samir; Puebla, Germán; Román Díez, Guillermo
Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable.
Desarrollo de una herramienta de depuración simbólica para las asignaturas de iniciación a la programación en las facultades de Informática y Estudios Estadísticos
(2015-02-20) Gómez-Zamalloa Gil, Miguel; Albert Albiol, Elvira; Arenas Sánchez, Purificación; Correas Fernández, Jesús; Genaim, Samir; Puebla Sánchez, Germán; Román Díez, Guillermo; Peces, Raquel; Giraldo, Carlos Gabriel; Antolín, Clara
El proyecto plantea el desarrollo de una herramienta de depuración simbólica que ayude a los estudiantes de las asignaturas de iniciación a la programación en las facultades de Informática y Estudios Estadísticos
May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization
(2015-09) Albert Albiol, Elvira; Genaim, Samir; Gordillo, Pablo
A may-happen-in-parallel (MHP) analysis computes pairs of program points that may execute in parallel across different distributed components. This information has been proven to be essential to infer both safety properties (e.g., deadlock freedom) and liveness properties termination and resource boundedness) of asynchronous programs. Existing MHP analyses take advantage of the synchronization points to learn that one task has finished and thus will not happen in parallel with other tasks that are still active. Our starting point is an existing MHP analysis developed for intra-procedural synchronization, i.e., it only allows synchronizing with tasks that have been spawned inside the current task. This paper leverages such MHP analysis to handle inter-procedural synchronization, i.e., a task spawned by one task can be awaited within a different task. This is challenging because task synchronization goes beyond the boundaries of methods, and thus the inference of MHP relations requires novel extensions to capture inter-procedural dependencies. The analysis has been implemented and it can be tried online.
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.
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.
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.
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.
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.
SACO: Static analyzer for concurrent objects
(Springer, 2014) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Flores Montoya, A.; Genaim, Samir; Gómez-Zamalloa Gil, Miguel; Martín Martín, Enrique; Puebla, G.; Román Díez, Guillermo
We present the main concepts, usage and implementation of SACO, a static analyzer for concurrent objects. Interestingly, SACO is able to infer both liveness(namely termination and resource boundedness) and safety properties (namely deadlock freedom) of programs based on concurrent objects. The system integrates auxiliary analyses such as points-to and may-happen-in-parallel, which are essential for increasing the accuracy of the aforementioned more complex properties. SACO provides accurate information about the dependencies which may introduce deadlocks, loops whose termination is not guaranteed, and upper bounds on the resource consumption of methods.
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.
Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-based Instance, and Actor-based Concurrency
(2014-05) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Gómez Zamalloa, Miguel; Rojas, José Miguel
The focus of this tutorial is white-box test case generation (TCG) based on symbolic execution. Symbolic execution consists in executing a program with the contents of its input arguments being symbolic variables rather than concrete values. A symbolic execution tree characterizes the set of execution paths explored during the symbolic execution of a program. Test cases can be then obtained from the successful branches of the tree. The tutorial is split into three parts: (1) The first part overviews the basic techniques used in TCG to ensure termination, handling heap-manipulating programs, achieving compositionality in the process and guiding TCG towards interesting test cases. (2) In the second part, we focus on a particular implementation of the TCG framework in constraint logic programming (CLP). In essense, the imperative object-oriented program under test is automatically transformed into an equivalent executable CLP-translated program. The main advantage of CLP-based TCG is that the standard mechanism of CLP performs symbolic execution for free. The PET system is an open-source software that implements this approach. (3) Finally, in the last part, we study the extension of TCG to actor-based concurrent programs.
Test Case Generation of Actor Systems
(2015-10) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Gómez Zamalloa, Miguel
Testing is a vital part of the software development process. It is even more so in the context of concurrent languages, since due to undesired task interleavings and to unexpected behaviours of the underlying task scheduler, errors can go easily undetected. Test case generation (TCG) is the process of automatically generating test inputs for interesting coverage criteria, which are then applied to the system under test. This paper presents a TCG framework for actor systems, which consists of three main elements, which are the original contributions of this work: (1) a symbolic execution calculus, which allows symbolically executing the program (i.e., executing the program for unknown input data), (2) improved techniques to avoid performing redundant computations during symbolic execution, (3) new termination and coverage criteria, which ensure the termination of symbolic execution and guarantee that the test cases provide the desired degree of code coverage. Finally, our framework has been implemented and evaluated within the aPET system.

Browsing by Author "Albert Albiol, Elvira"

Results Per Page

Sort Options