Person:
Gordillo Alguacil, Pablo

Profile Picture
First Name
Pablo
Last Name
Gordillo Alguacil
Affiliation
Universidad Complutense de Madrid
Faculty / Institute
Informática
Department
Sistemas Informáticos y Computación
Area
Ciencia de la Computación e Inteligencia Artificial
Identifiers
UCM identifierORCIDScopus Author IDWeb of Science ResearcherIDDialnet ID

Filters

2015 - 20202
Reset filters

Settings

Search Results

Now showing 1 - 2 of 2
  • Thumbnail Image
    Publication
    Static analysis of concurrent objects: May-Happen-in-Parallel fo asynchronous programs with Inter-procedural synchronization
    (2015) Gordillo Alguacil, Pablo; Albert Albiol, Elvira María; Genaim, Samir
    This work presents a may-happen-in-parallel analysis with inter-procedural synchronization for languages based in concurrent objects. In this model of concurrency (based on actors) the objects are the concurrency units. The idea behind it is that each object has its own processor. A may-happen-inparallel (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. We can distinguish diferent phases in the development of the analysis: (1) The first one where MHF analysis is performed to infer the relations of synchronization that exist between the methods, (2) a second local phase to analyze each method separately and (3) a last phase to composed all information. As the problem is undecidable when considering a full concurrent objects programming language, the analysis over-approximates the real parallelism programs. Finally, the implementation of the analysis has been integrated in SACO, a static analyzer of concurrent programs. The main technical results [5] have been selected to be published in the proceedings of Static Analysis Symposium 2015: http://sas2015.inria.fr. It is the main conference on static analysis (classified as category A in the international ranking CORE).
  • Thumbnail Image
    Publication
    Análisis estático de sistemas concurrentes y distribuidos: objetos concurrentess y Bytecode de Ethereum
    (Universidad Complutense de Madrid, 2020-10-28) Gordillo Alguacil, Pablo; Albert Albiol, Elvira; Genaim, Samir
    Hoy en día la concurrencia y la distribución se han convertido en una parte fundamental del proceso de desarrollo de software. Indiscutiblemente, Internet y el uso cada vez más extendido de los procesadores multicore ha influido en el tipo de aplicaciones que se desarrollan. Esto ha dado lugar a la creación de distintos modelos de concurrencia .En particular, uno de los modelos de concurrencia que está ganando importancia es el modelo de objetos concurrentes basado en actores. En este modelo, los objetos (denominados actores) son las unidades de concurrencia. Cada objeto tiene su propio procesador y un estado local. La comunicación entre los mismos se lleva a cabo mediante el paso de mensajes. Cuando un objeto recibe un mensaje puede: actualizar su estado, mandar mensajes o crear nuevos objetos. Es bien sabido que la creación de programas concurrentes correctos es más compleja que la de programas secuenciales ya que es necesario tener en cuenta distintos aspectos inherentes a la concurrencia como los errores asociados a las carreras de datos o a los interbloqueos. Con el n de asegurar el correcto comportamiento de estos programas concurrentes se han desarrollado distintas técnicas de análisis estático y verificación para los diversos modelos de concurrencia existentes...