Resumen Técnico: PaSTTeL

Planteamiento del Problema

Demostrar la terminación o la no terminación de los programas es un problema fundamental, aunque indecidible, en las ciencias de la computación. Un enfoque práctico consiste en buscar argumentos explícitos: un argumento de terminación (por ejemplo, una función de ranking lineal) implica terminación, mientras que un argumento de no terminación (por ejemplo, un conjunto de recurrencia lineal o un argumento de no terminación geométrico) implica no terminación. Estos análisis se aplican frecuentemente a programas lasso —trazas de ejecución que consisten en código de línea recta seguido de un único bucle while, representando caminos infinitos candidatos que suelen extraerse durante la síntesis de terminación basada en CEGAR.

Si bien los argumentos específicos de terminación o no terminación son decidibles, el problema general sigue siendo un desafío. Las herramientas actuales de vanguardia suelen emplear estrategias secuenciales, y existe la necesidad de un marco unificado que pueda integrar diversos algoritmos de análisis, ejecutarlos de forma concurrente y servir como un componente modular para herramientas de verificación externas.

Metodología: El Marco de Trabajo PaSTTeL

Los autores presentan PaSTTeL (Parallel analysiS framework for Termination and non-Termination of Lasso programs), un marco de trabajo de portafolio modular, genérico y paralelo implementado en C++17. La arquitectura está diseñada para unificar los enfoques de terminación y no terminación dentro de un modelo de ejecución concurrente.

Arquitectura Central

El marco de trabajo se estructura en torno a tres componentes principales, ilustrados mediante un diseño modular:

1. Motor SMT (SMTSolverInterface): Una capa de abstracción que permite el uso de motores SMT intercambiables. La implementación actual soporta Z3 y CVC5. La instancia del solver se pasa a los analizadores secuenciales para las técnicas basadas en restricciones.
2. Analizador Secuencial (AnalysisInterface): Un adaptador que define la interfaz para las estrategias individuales de terminación o no terminación. Los métodos clave incluyen:
   • analyze(): Ejecuta el análisis y devuelve un resultado (TERMINATING, NON_TERMINATING o UNKNOWN).
   • getProof(): Devuelve un certificado de prueba en texto plano.
3. Capa de Paralelización (PortfolioAnalyzer): Gestiona la ejecución concurrente de múltiples estrategias registradas sobre el mismo programa lasso de entrada. Se encarga del despliegue de hilos, el registro de estrategias y la agregación de resultados.

Instanciación e Integración

PaSTTeL está diseñado como una biblioteca autónoma. Para instanciar el marco de trabajo, un usuario adapta una función init-PaSTTeL (Algoritmo 1) que:

• Crea múltiples instancias de solvers SMT basadas en el tipo deseado (Z3 o CVC5).
• Inicializa el PortfolioAnalyzer con el programa lasso y el recuento de hilos.
• Registra técnicas de análisis específicas (por ejemplo, síntesis de terminación, argumentos de no terminación) en el portafolio.
• Lanza la búsqueda concurrente mediante solve() y espera a un resultado concluyente o un límite de tiempo mediante join().

Prueba de Concepto: P-ULR

Para validar la genericidad del marco de trabajo, los autores instanciaron PaSTTeL para replicar las capacidades principales de Ultimate LassoRanker (ULR), una herramienta de vanguardia y ganadora de SV-COMP 2025. Esta instanciación, denominada P-ULR, implementa:

• Gestión de Entradas: Un formato de entrada basado en JSON que sigue los estándares SMT-LIB con soporte para Asignación Estática Simple (SSA). Linealiza los programas lasso cuando es necesario.
• Estrategias de Terminación: Síntesis basada en restricciones utilizando plantillas de ranking lineales, específicamente plantillas de ranking afines y anidadas.
• Estrategias de No Terminación: Síntesis basada en restricciones que incluye verificación de punto fijo y Argumentos de No Terminación Geométrica (GNTA).

Nota sobre Limitaciones: La implementación actual de P-ULR tiene restricciones específicas: no cubre completamente los casos no lineales (por ejemplo, operaciones complejas de arreglos), depende de fórmulas lineales para la mayoría de las estrategias y actualmente solo soporta QF_LRA para la terminación y QF_LIA para GNTA.

Resultados Experimentales

El marco de trabajo fue evaluado con 4,619 programas lasso derivados de los repositorios SV-COMP 2025, TermCOMP 2025 y Ultimate. Los experimentos se realizaron en una máquina con 16 procesadores Intel Core i5-14400T y 30 GB de memoria, con un tiempo de espera de 600 segundos por instancia.

Comparación de Rendimiento

El estudio comparó tres configuraciones:

1. ULR-Baseline: La herramienta ULR original ejecutando estrategias de forma secuencial.
2. P-ULR-Seq: PaSTTeL ejecutando las mismas estrategias de forma secuencial (para asegurar una comparación justa).
3. P-ULR-Par4: PaSTTeL ejecutando con 4 hilos concurrentes (Fixpoint, GNTA, Affine, Nested).

Hallazgos Clave:

• Eficiencia Secuencial: P-ULR-Seq superó a ULR-Baseline, logrando un ahorro de tiempo total de 862 segundos (~14 minutos). Notablemente, el tiempo acumulado para la síntesis de no terminación cayó de 47.13s a 1.78s (una reducción de 26 veces).
• Análisis de Terminación: P-ULR-Seq redujo significativamente el tiempo para encontrar funciones de ranking. Sin embargo, ULR-Baseline ocasionalmente produjo funciones de ranking más simples debido a un paso de partición interno que P-ULR carece actualmente.
• Análisis de No Terminación: P-ULR-Seq demostró una clara ventaja en el manejo de pruebas de no terminación complejas (GNTA) en comparación con la base.
• Ejecución Paralela: P-ULR-Par4 redujo el tiempo total de ejecución por un factor de 2.8 en comparación con ULR-Baseline. Sin embargo, la aceleración respecto a P-ULR-Seq fue marginal. Los autores atribuyen esto a la composición del benchmark: el 98% de los programas lasso admiten una función de ranking afín, la cual P-UR-Seq resuelve inmediatamente en su orden secuencial, dejando poco margen para que las estrategias paralelas mejoren el rendimiento en este conjunto de datos específico.

Significación y Contribuciones

El artículo afirma que PaSTTeL demuestra con éxito que un marco de trabajo modular y genérico puede unificar técnicas de vanguardia de terminación y no terminación sin comprometer el rendimiento. Las contribuciones clave son:

1. Modularidad: Un diseño que facilita la integración de nuevos algoritmos de análisis en un portafolio unificado.
2. Concurrencia: La capacidad de ejecutar estrategias registradas de forma concurrente para acelerar el análisis.
3. Reutilización: Un componente de biblioteca C++ autónomo que permite a proyectos externos embeber capacidades de análisis de (no) terminación sin necesidad de comprender el diseño interno.
4. Rendimiento Competitivo: La instanciación (P-ULR) rinde competitivamente frente a la herramienta ULR original, con aceleraciones significativas en la síntesis de no terminación y en el tiempo de ejecución general, validando la eficiencia del marco de trabajo.

Los autores concluyen que, si bien la implementación actual tiene limitaciones respecto a la aritmética no lineal y pasos de optimización específicos, el marco de trabajo proporciona una base robusta para futuras extensiones, tales como la integración de la síntesis de conjuntos de recurrencia y el soporte para aritmética no lineal (QF_NRA/QF_NIA).