Como posso verificar lock-free algoritmos?

Question

Em teoria, deve ser possível, pelo menos, a força bruta de uma verificação de um lock-free algoritmo (só existem tantas combinações de chamadas de função de intersecção).Há ferramentas ou formal processos de raciocínio disponíveis para realmente provar que um lock-free algoritmo está correto (idealmente, deveria também ser capaz de verificar as condições de corrida e a ABA problema)?

Nota:Se você conhece uma forma apenas para provar um ponto (por exemplo,apenas provar que é seguro a partir da ABA problema) ou um problema que eu não mencionei, em seguida, postar a solução de qualquer maneira.Na pior das hipóteses, cada método pode ser feito em ligar para verificar integralmente a ele.

Answer 1

Você definitivamente deveria tentar o Verificador de modelo de spin.

Você escreve um modelo semelhante ao programa em uma linguagem simples do tipo C chamada Promela, que o SPIN se traduz internamente em uma máquina de estado. Um modelo pode conter vários processos paralelos.

O que o spin então faz é verificar toda intercalação possível de instruções de cada processo para Quaisquer condições que você queira testar - normalmente, ausência de condições de raça, liberdade de impasse etc. A maioria desses testes pode ser facilmente escrita usando assert() declarações. Se houver alguma sequência de execução possível que viole uma afirmação, a sequência será impressa, caso contrário, você recebe o "limpo".

(Bem, na verdade, ele usa um algoritmo muito mais sofisticado e mais rápido para realizar isso, mas esse é o efeito. Por padrão, todos os estados do programa acessíveis são verificados.)

Isto é um incrível programa, venceu o 2001 Prêmio de software de sistema ACM (Outros vencedores incluem Unix, Postscript, Apache, Tex). Comecei a usá -lo muito rapidamente e em alguns dias consegui implementar modelos das funções do MPI MPI_Isend() e MPI_Irecv() em Promela. Spin encontrou alguns complicado Condições de corrida em um segmento de código paralelo que converti para o Promela para teste.

Answer 2

Spin é realmente excelente, mas também considerar Relacy Corrida Detector De por Dmitriy V'jukov.Ele é construído de propósito para verificar simultâneas de algoritmos, incluindo a não-bloqueio (espera/sem bloqueio) algoritmos.É open source e liberalmente licenciado.

Relacy fornece POSIX e Windows primitivos de sincronização (exclusões mútuas, as variáveis de condição, semáforos, CriticalSections, win32 eventos, Intertravado*, etc), para sua real implementação C++ pode ser alimentados para Relacy para verificação.Não há necessidade de desenvolver um modelo separados de seu algoritmo com Promela e Spin.

Relacy oferece o C++0x std::atomic (explícito memória pedido para a vitória!) então você pode usar o pré-processador #defines para selecionar entre Relacy implementação e sua própria plataforma específica atômica implementação (tbb::atómica, boost::atómica, etc.).

O agendamento é controlável:aleatório, vinculado contexto, e de pesquisa completo (todas as possíveis interleavings) disponíveis.

Aqui está um exemplo Relacy programa.Algumas coisas a observar:

• O $ é um Relacy macro que registra informações de execução.
• rl::var<T> bandeiras "normal" (não-atômica) variáveis que devem ser consideradas como parte da verificação.

Código:

#include <relacy/relacy_std.hpp>

// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
    std::atomic<int> a;
    rl::var<int> x;

    // executed in single thread before main thread function
    void before()
    {
        a($) = 0;
        x($) = 0;
    }

    // main thread function
    void thread(unsigned thread_index)
    {
        if (0 == thread_index)
        {
            x($) = 1;
            a($).store(1, rl::memory_order_relaxed);
        }
        else
        {
            if (1 == a($).load(rl::memory_order_relaxed))
                x($) = 2;
        }
    }

    // executed in single thread after main thread function
    void after()
    {
    }

    // executed in single thread after every 'visible' action in main threads
    // disallowed to modify any state
    void invariant()
    {
    }
};

int main()
{
    rl::simulate<race_test>();
}

Compilar com o seu normal compilador (Relacy é somente cabeçalho) e executar o arquivo executável:

struct race_test
DATA RACE
iteration: 8

execution history:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

thread 0:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)

thread 1:
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

Versões recentes do Relacy também fornecer Java e CLI modelos de memória se você curte esse tipo de coisa.

Answer 3

A detecção de corrida de dados é um problema difícil do NP [Netzer & Miller 1990

Eu ouvi sobre o conjunto de bloqueios das ferramentas e djit+ (eles ensine no curso CDP). Tente ler os slides e pesquisar no Google o que eles fazem referência. Ele contém algumas informações interessantes.

Answer 4

Não sei qual plataforma ou idioma você está usando - mas na plataforma .NET há um projeto de pesquisa da Microsoft chamado Xadrez O que parece muito promissor em ajudar aqueles de nós a fazer componentes multithread - incluindo o bloqueio.

Eu não usei uma quantidade enorme, mente.

Funciona (explicação bruta), explicitamente intercalando fios nas maneiras mais rígidas possíveis de realmente forçar seus bugs para a natureza. Ele também analisa o código para encontrar erros comuns e padrões ruins - semelhante à análise de código.

No passado, também construí versões especiais do código em questão (através de blocos #if etc.) que adicionam informações extras de rastreamento estatal; contagens, versões etc., que eu posso mergulhar em um teste de unidade.

O problema é que leva muito mais tempo para escrever seu código e você nem sempre pode adicionar esse tipo de coisa sem alterar a estrutura subjacente do código que já está lá.

Answer 5

Se você realmente deseja verificar o código sem bloqueio (em vez de testar exaustivamente uma pequena instância), você pode usar o VCC (http://vcc.codeplex.com), um verificador dedutivo para o código C simultâneo, que foi usado para verificar alguns algoritmos interessantes sem bloqueio (por exemplo, listas livres de trava e hashtables redutíveis usando ponteiros de perigo, processamento de transações de multiverso otimista, virtualização de MMU, vários primitivos de sincronização, etc.). Ele faz verificação modular e tem sido usado para verificar pedaços não triviais de código industrial (até cerca de 20kloc).

Observe, no entanto, que o VCC é um verificador, não uma ferramenta de caça a insetos; Você terá que fazer uma anotação substancial em seu código para verificar e a curva de aprendizado pode ser um pouco íngreme. Observe também que ele assume consistência seqüencial (como a maioria das ferramentas).

BTW, a revisão por pares não é uma boa maneira de verificar um algoritmo simultâneo (ou mesmo sequencial). Há uma longa história de pessoas famosas publicando algoritmos simultâneos em periódicos importantes, apenas para descobrir bugs anos depois.