¿Cómo puedo verificar algoritmos sin bloqueo?

Question

En teoría, debe ser posible a la fuerza al menos bruta una verificación de un algoritmo libre de bloqueo (sólo hay tantas combinaciones de llamadas de función de intersección). ¿Hay herramientas o procesos de razonamiento formales disponibles para probar realmente que un algoritmo libre de bloqueo es correcta (lo ideal es que también debe ser capaz de comprobar las condiciones de carrera y el problema ABA también)?

Nota: Si conoce una manera de demostrar simplemente un punto (por ejemplo, solamente demostrar que está a salvo del problema ABA) o un problema que no he mencionado a continuación, publicar la solución de todos modos. En el peor de los casos, cada método se puede hacer a su vez para verificar completamente.

Answer 1

sin duda debe probar el modelo de Spin corrector .

Usted escribe un modelo de programa como en un simple lenguaje C, llamado PROMELA, que giran internamente se traduce en una máquina de estados. Un modelo puede contener varios procesos paralelos.

Lo vuelta entonces hace es comprobar todas las posibles entrelazado de instrucciones de cada proceso para cualquier condición desea probar - por lo general, la ausencia de condiciones de carrera, la libertad de los puntos muertos etc. La mayoría de estas pruebas se puede escribir fácilmente usando declaraciones assert(). Si hay cualquier posible secuencia de ejecución que viole una afirmación, la secuencia se imprime, de lo contrario se le da la "vía libre".

(Bueno, en realidad, se utiliza un algoritmo mucho más elegante y más rápido para lograr esto, pero eso es el efecto. Por defecto, todos los estados alcanzables programa se comprueban.)

Este es un increíble programa, se ganaron el ACM Premio 2001 del software del sistema (otros ganadores incluyen Unix, PostScript, Apache, tex). Me empecé a usarlo muy rápidamente, y en un par de días era capaz de poner en práctica modelos de la MPI funciones MPI_Isend() y MPI_Irecv() en PROMELA. Giro encontró un par de complicado condiciones de carrera en un segmento de código paralelo Convertí a través PROMELA para la prueba.

Answer 2

Spin es en efecto excelente, pero también consideran detector Race href="http://groups.google.com/group/relacy" Relacy por Dmitriy V'jukov. Es especialmente diseñado para la verificación de algoritmos concurrentes incluyendo sin bloqueo algoritmos (espera- / libre de bloqueo). Es de código abierto y liberalmente con licencia.

Relacy proporciona primitivas POSIX y Windows de sincronización (mutex, variables de condición, semáforos CriticalSections, eventos Win32, Interlocked *, etc), por lo que su aplicación real de C ++ se puede alimentar a Relacy para su verificación. No hay necesidad de desarrollar un modelo separado de su algoritmo que con PROMELA y vuelta.

Relacy ofrece C ++ 0x std::atomic (ordenamiento memoria explícita por la victoria!) Para que pueda utilizar #defines pre-procesador para seleccionar entre la aplicación de Relacy y su propia plataforma de implementación atómica específica ( TBB :: atómica , impulso :: atómica , etc).

La programación es controlable:. Aleatoria, ligado al contexto, y de búsqueda completa (todas las posibles intercalaciones) disponible

El siguiente es un ejemplo de programa Relacy. Un par de cosas a tener en cuenta:

• El $ es una macro Relacy que registra la información de ejecución.
• banderas rl::var<T> "normal" (no atómica) variables que también deben tenerse en cuenta como parte de la verificación.

El 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 con su compilador normal (Relacy es sólo de encabezado) y ejecute el archivo ejecutable:

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)

Las versiones recientes de Relacy también proporcionan modelos de memoria de Java y CLI si usted está en ese tipo de cosas.

Answer 3

Detección de la raza de datos es un problema difícil NP [Netzer & Miller 1990]

Me enteré de la cerradura herramientas y DJit + (que lo enseñan en el curso CDP). Trate de leer las diapositivas, y buscando en Google lo que hacen referencia a. Contiene información interesante.

Answer 4

No sé qué plataforma o lenguaje que está utilizando - pero en la plataforma .Net hay un proyecto de investigación de Microsoft llamado ajedrez que se ve muy prometedor en ayudar a aquellos de nosotros haciendo componentes multiproceso - incluyendo sin bloqueo

.

No he utilizado una cantidad enorme, cuenta.

Funciona (explicación crudo) intercalando de manera explícita las discusiones en los caminos más estrechos posible forzar realidad sus errores a cabo en el medio natural. También analiza el código para encontrar errores comunes y patrones malos -. Similares al análisis de código

En el pasado, yo también he construido versiones especiales del código en cuestión (a través de bloques #if etc) que añaden información adicional de seguimiento de estado; recuentos, versiones, etc., que entonces puede sumergir en dentro de una unidad de prueba.

El problema con esto es que se necesita mucho más tiempo para escribir el código, y no siempre se puede añadir este tipo de cosas sin cambiar la estructura subyacente del código que ya existe.

Answer 5

Si desea verificar realmente código libre de frenos (en contraposición a probar exhaustivamente un pequeño ejemplo), puede utilizar VCC ( http://vcc.codeplex.com ), un verificador deductiva para el código C concurrentes que se ha utilizado para verificar algunos algoritmos sin bloqueo interesantes (por ejemplo, listas de bloqueo y sin tablas hash de tamaño variable que utilizan punteros de peligro, optimista transacción multiversión procesamiento, MMU virtualización, varias primitivas de sincronización, etc.). Lo hace la verificación modular, y se ha utilizado para verificar trozos no triviales de código industrial (hasta aproximadamente 20KLOC).

Tenga en cuenta, sin embargo, que VCC es un verificador, no una herramienta de caza de errores; usted tiene que hacer la anotación sustancial en su código para conseguir que se verifique, y la curva de aprendizaje puede ser un poco caro. Tenga en cuenta también que asume la consistencia secuencial (como lo hacen la mayoría de las herramientas).

Por cierto, la revisión por pares no es una buena manera de comprobar un algoritmo concurrente (o incluso uno secuencial). Hay una larga historia de personajes famosos publicación de algoritmos concurrentes en revistas importantes, sólo para que los errores descubiertos años más tarde.