Download de Deadlock_Racer - Deadlock_Racer download do código -fonte

Deadlock_Racer

Outras categorias

v1.0.1

Baixar

Impasse

O Deadlock é um analisador estático para a detecção de possíveis deadlocks em programas C implementados como um plug-in da plataforma Frama-C.

O algoritmo do núcleo é baseado em um racerx de ferramentas existente. O chamado Análise de Lockset atravessa o gráfico de fluxo de controle e calcula o conjunto de bloqueios mantidos em qualquer ponto do programa. Quando o bloqueio B é adquirido com o conjunto de bloqueio atual que já contém o bloqueio A, a dependência A -> B é adicionada ao LockGraph. Cada ciclo neste gráfico é então relatado como um impasse em potencial.

O plug-in usa EVA (Value Analysis Plugin de Frama-C) para calcular informações de maio para parâmetros de operações de bloqueio. Como a EVA não pode analisar de maneira nativa os programas simultâneos, primeiro identificamos todos os threads em um programa e depois o executamos para cada thread separadamente com contextos dos pontos do programa, onde o thread foi criado. O resultado é então sub-abrangência, que não leva em consideração as intercaladas do thread.

Exemplo

Este exemplo demonstra saída para o programa com impasse simples. O exemplo mais complexo pode ser encontrado aqui.

 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 );
}

Saída:

 [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)

Instalação

A versão atual é compatível com o Frama-C Vanadium, seu guia de instalação detalhado pode ser encontrado no manual do usuário e requer a versão OCAML pelo menos 4.12. Além do Frama-C, o Deadlock exige que os pacotes Opam seguintes sejam instalados:

 ounit2
containers

Depois de instalar dependências e clonar este repositório, o impasse pode ser instalado da seguinte forma:

 cd Deadlock
make setup
make
make install

Você também pode executar o Deadlock no Docker usando docker run -it tdacik/deadlock ou executando make docker para criar uma imagem da versão mais recente.

Uso

A maneira mais simples de executar o plug -in é:

 frama-c -deadlock source_file1.c source_file2.c ...

Para um uso mais avançado, consulte Lista de opções de linha de comando para ajustar o manual de análise e GUI para obter a visualização dos resultados no aplicativo GUI do Frama-C.