Techniques to improve testing scalability on concurrent programs: combining static analysis and testing for Deadlock detection

Abstract

Static deadlock analyzers might be able to verify the absence of deadlock, but when they detect a potential deadlock cycle, they provide little (or even none) information on their output. Due to the complex ow of concurrent programs, the user might not be able to find the source of the anomalous behaviour from the abstract information computed by static analysis.This paper proposes the combined use of static analysis and testing for effective deadlock detection in asynchronous programs. Our main contributions are: (1)We present an enhanced semantics which allows an early detection of deadlocks during testing and that can give to the user a precise description of the deadlock trace. (2) We combine our testing framework with the abstract descriptions of potential deadlock cycles computed by an existing static deadlock analyzer. Namely, such descriptions are used by our enhanced semantics to guide the execution towards the potential deadlock paths (while other paths are pruned). When the program features a deadlock, our combined use of static analysis and testing provides an effective technique to find deadlock traces. While if the program does not have deadlock, but the analyzer inaccurately spotted it, we might be able to prove deadlock freedom.

Los análisis estáticos de deadlock son, a menudo, capaces de asegurar la ausencia de bloqueos, pero cuando detectan un posible ciclo de deadlock, la información que devuelven como salida es escasa e insuficiente. Debido al complejo flujo de ejecución existente en los programas concurrentes, el usuario podría ser incapaz de encontrar la causa del comportamiento anómalo a partir de la información abstracta proporcionada por el análisis estático. Este trabajo propone el uso combinado de un análisis estático y el testing dinámico para la detección efectiva de deadlocks en programas asíncronos. Las principales contribuciones son: (1) Presentamos una semántica extendida que permite la detección instantánea de bloqueos durante el testing y dar al usuario una descripción precisa de la traza de deadlock. (2) Además combinamos, nuestra herramienta de testing con las descripciones abstractas de posibles ciclos de deadlock, inferidos por un análisis estático existente. Tales descripciones son usadas en nuestra semántica extendida para guiar la ejecución hacia posibles caminos de deadlock, mientras que el resto son podados. Cuando el programa contiene un bloqueo, el uso combinado del análisis estático y el testing nos proporciona una técnica efectiva para encontrar trazas de deadlock. En caso de que el programa no contenga ninguno, pero el análisis sí que lo detecte debido a pérdidas de precisión, podríamos llegar a demostrar la ausencia de deadlocks.