Deadlock_Racer
v1.0.1
Deadlock es un analizador estático para la detección de posibles plazos en los programas C implementados como un complemento de la plataforma frama-C.
El algoritmo central se basa en una herramienta Racerx existente. El llamado análisis de bloqueo de bloqueo atraviesa el gráfico de flujo de control y calcula el conjunto de bloqueos sostenidos en cualquier punto de programa. Cuando se adquiere el bloqueo B con el bloque de bloqueo actual que ya contiene el bloqueo A, se agrega dependencia A -> B al bloqueo de bloqueo. Cada ciclo en este gráfico se informa como un punto muerto potencial.
El complemento utiliza EVA (complemento de análisis de valor de Frama-C) para calcular la información de May-Point-To para los parámetros de las operaciones de bloqueo. Debido a que EVA no puede analizar de forma nativa programas concurrentes, primero identificamos todos los hilos en un programa y luego lo ejecutamos para cada hilo por separado con contextos de puntos del programa, donde se creó el hilo. El resultado es entonces sub-acroximación, que no tiene en cuenta las entradas de hilo.
Este ejemplo demuestra el resultado para el programa con un punto muerto simple. El ejemplo más complejo se puede encontrar aquí.
void * thread1 ( void * v )
{
pthread_mutex_lock ( & lock1 );
pthread_mutex_lock ( & lock2 );
...
pthread_mutex_unlock ( & lock2 );
pthread_mutex_unlock ( & lock1 );
}
void * thread2 ( void * v )
{
pthread_mutex_lock ( & lock2 );
pthread_mutex_lock ( & lock1 );
...
pthread_mutex_unlock ( & lock1 );
pthread_mutex_unlock ( & lock2 );
} [kernel] Parsing simple_deadlock.c (with preprocessing)
[Deadlock] Deadlock analysis started
[Deadlock] === Assumed threads: ===
[Deadlock] main
[Deadlock] thread1
[Deadlock] thread2
[Deadlock] === Lockgraph: ===
[Deadlock] lock1 -> lock2
[Deadlock] lock2 -> lock1
[Deadlock] ==== Results: ====
[Deadlock] Deadlock between threads thread1 and thread2:
Trace of dependency (lock2 -> lock1):
In thread thread2:
Lock of lock2 (simple_deadlock.c:20)
Lock of lock1 (simple_deadlock.c:21)
Trace of dependency (lock1 -> lock2):
In thread thread1:
Lock of lock1 (simple_deadlock.c:10)
Lock of lock2 (simple_deadlock.c:11)
La versión actual es compatible con el vanadio frama-c, su guía de instalación detallada se puede encontrar en el manual del usuario y requiere la versión OCAML al menos 4.12. Además de Frama-C, Deadlock requiere que se instalen los siguientes paquetes OPAM:
ounit2
containers
Después de instalar dependencias y clonar este repositario, el punto muerto se puede instalar de la siguiente manera:
cd Deadlock
make setup
make
make install
También puede ejecutar Deadlock en Docker utilizando docker run -it tdacik/deadlock o ejecutando make docker para construir una imagen de la versión más reciente.
La forma más sencilla de ejecutar el complemento es:
frama-c -deadlock source_file1.c source_file2.c ...
Para un uso más avanzado, consulte la lista de opciones de línea de comandos para ajustar el análisis y el manual de GUI para la visualización de resultados en la aplicación GUI de Frama-C.
Dacík T. Detección de punto muerto estático en Frama-C en Actas de Excel@Fit'20 . Universidad Tecnológica de Brno, Facultad de Tecnología de la Información. 2020
El análisis estático de Dacík T. en el entorno Frama-C se centró en la tesis de licenciatura de detección de punto muerto. Universidad Tecnológica de Brno, Facultad de Tecnología de la Información. 2020-07-10. Supervisado por Vojnar Tomáš.
Si tiene alguna pregunta, no dude en comunicarse con los autores de la herramienta/método:
El complemento está disponible bajo la licencia MIT.
