Registro:
Documento: | Tesis Doctoral |
Disciplina: | computacion |
Título: | Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT |
Título alternativo: | Efficient sequential tight field bounds computation, and their impact on the performance of SAT based program analysis |
Autor: | Ponzio, Pablo Daniel |
Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
Lugar de trabajo: | Departamento de Computación
|
Publicación en la Web: | 2014-10-14 |
Fecha de defensa: | 2014-06-13 |
Fecha en portada: | 2014 |
Grado Obtenido: | Doctorado |
Título Obtenido: | Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación |
Departamento Docente: | Departamento de Computación |
Director: | Aguirre, Nazareno Matías; López Pombo, Carlos Gustavo |
Jurado: | Areces, Carlos Eduardo; Bonelli, Eduardo Augusto; Chiotti, Omar Juan Alfredo |
Idioma: | Español |
Tema: | computación/ingeniería del software computación/lógica y computabilidad
|
Formato: | PDF |
Handle: |
http://hdl.handle.net/20.500.12110/tesis_n5547_Ponzio |
PDF: | https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n5547_Ponzio.pdf |
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/tesis/document/tesis_n5547_Ponzio |
Ubicación: | COM 005547 |
Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Ponzio, Pablo Daniel. (2014). Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales). Recuperado de http://hdl.handle.net/20.500.12110/tesis_n5547_Ponzio |
Resumen:
Dada una descripción formal de los estados válidos del heap -por ejemplo, un invariantede una estructuras de datos- las cotas ajustadas para los campos del heapson el conjunto de los valores que pueden tomar los campos en alguna instanciaválida. Así, los valores de campos que no pertenecen a las cotas ajustadas puedenser ignorados por los análisis automáticos (acotados) de código, reduciendo así elespacio de estados a explorar, y mejorando la performance del análisis. Sin embargo,el cómputo de cotas ajustadas es costoso. El único enfoque conocido que computaestas cotas en un tiempo aceptable, TACO+, es intrínsecamente paralelo, y requierede un cluster con varias computadoras para su ejecución eficiente. En este trabajo se aborda el problema de computar eficientemente cotas ajustadasen entornos de ejecución secuenciales. Así, se presentan dos nuevos enfoques pararesolver este problema. El primero, denominado bottom-up, utiliza un procedimientode decisión basado en SAT para visitar instancias válidas del heap, y computacotas ajustadas usando los valores de los campos de estas instancias. bottom-up, aligual que TACO+, requiere de una especificación en algún lenguaje declarativo dealto nivel -como JML para JAVA- de los estados válidos del heap. De esta manera,bottom-up y TACO+ generan cotas ajustadas equivalentes. El segundo, SLBD, sebasa en una especificación del heap en términos de un predicado inductivo de lalógica de separación. Este enfoque computa cotas ajustadas mientras realiza (unnúmero finito de) desplegados del predicado inductivo de entrada. En algunos casos SLBD puede producir cotas ajustadas diferentes a las de TACO+ (y bottom-up). Se evaluaron experimentalmente los enfoques bottom-up, SLBD y la técnicarelacionada TACO+, en la generación de cotas ajustadas para varias clases contenedoras JAVA. Los resultados muestran que, en un ambiente de ejecución secuencial,bottom-up es un orden de magnitud más rápido que TACO+ (secuencializado),y que SLBD es dos órdenes de magnitud más rápido que bottom-up. Además, seevaluó el impacto de las cotas ajustadas generadas por nuestros enfoques en la verificación de código y en la generación exhaustiva de estructuras (que satisfacen unpredicado) basados en SAT. Los resultados indican que los enfoques que computancotas ajustadas secuencialmente (vía bottom-up o SLBD), y luego las aprovechandurante el análisis, son significativamente más eficientes que los análisis convencionales,que no explotan la idea de cotas ajustadas. Además, para los análisis basadosen SAT mencionados, los resultados muestran que las cotas ajustadas computadaspor SLBD tienen un impacto similar a las computadas por TACO+ y bottom-up.
Abstract:
Given a formal description of the feasible heap states -for example, an invariantfor a data structure-, tight field bounds for heap fields are the set of values that thefields can take in any valid instance. Thus, field values that do not belong to thetight field bounds can be safely ignored by automated (bounded) program analyses,reducing the state space to be explored, and improving the performance of theanalysis. However, computing tight field bounds is an expensive process. The onlyknown approach to compute these bounds that performs reasonably, TACO+, isintrinsically parallel, and it requires a cluster of several computers to run efficiently. In this work we address the problem of computing tight field bounds efficientlyunder a secuential execution environment. Thus, we introduce two novel approachesto solve this problem. The first, called bottom-up, uses a SAT based decision procedureto traverse valid heap instances, and computes tight field bounds using thefield values of the visited instances. bottom-up, like TACO+, requires a descriptionof the feasible heap states in a high level declarative language -like JML for JAVA-. In this way, bottom-up and TACO+ yield equivalent tight field bounds. The second, SLBD, is based on a specification of the valid heap states in terms ofa separation logic's inductive predicate. This approach computes tight field boundsduring the process of unfolding its input's inductive predicate (a finite number oftimes). In some cases, the tight field bounds computed by SLBD and TACO+ (andbottom-up) might differ. We assessed bottom-up, SLBD and the related technique TACO+ experimentally,in generating tight field bounds for several JAVA container classes. The resultsshow that, under a secuential execution environment, bottom-up is an orderof magnitude faster than TACO+ (secuentialized), and that SLBD is two orders ofmagnitude faster than bottom-up. Moreover, we assesed the impact of the tight fieldbounds produced by our approaches in SAT based code analysis and in exhaustivebounded generation of structures (satisfying a predicate). The results show that theapproaches that compute tight field bounds secuentially (via bottom-up or SLBD),and subsecuently exploit them during analysis, are significatively faster than themore conventional analyses that do not take advantage of tight field bounds. Furthermore,for the aformentioned SAT based analyses, the experiments show that thetight field bounds computed by SLBD have a similar impact to those computed by TACO+ and bottom-up.
Citación:
---------- APA ----------
Ponzio, Pablo Daniel. (2014). Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/tesis_n5547_Ponzio
---------- CHICAGO ----------
Ponzio, Pablo Daniel. "Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT". Tesis Doctoral, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2014.https://hdl.handle.net/20.500.12110/tesis_n5547_Ponzio
Estadísticas:
Descargas totales desde :
Descargas mensuales
https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n5547_Ponzio.pdf