algorithm - tarjetas - ¿Cómo puedo verificar los algoritmos sin bloqueo?

luhn algorithm

Question

En teoría, debería ser posible al menos forzar brutalmente una verificación de un algoritmo sin bloqueo (solo hay tantas combinaciones de funciones que se intersecan). ¿Existen herramientas o procesos de razonamiento formal disponibles para probar que un algoritmo sin bloqueo es correcto (idealmente, también debería poder verificar las condiciones de la carrera y el problema ABA)?

Nota: si conoce una forma de probar solo un punto (p. Ej., Solo pruebe que está a salvo del problema ABA) o un problema que no he mencionado, publique la solución de todos modos. En el peor de los casos, cada método se puede hacer a su vez para verificarlo completamente.

Answer 1

Definitivamente deberías probar el verificador de modelos Spin .

Escribe un modelo similar a un programa en un lenguaje simple tipo C llamado Promela, que Spin se traduce internamente en una máquina de estados. Un modelo puede contener múltiples procesos paralelos.

Lo que Spin luego hace es verificar cada posible intercalación de instrucciones de cada proceso para las condiciones que desee probar : por lo general, la ausencia de condiciones de carrera, la ausencia de puntos muertos, etc. La mayoría de estas pruebas se pueden escribir fácilmente utilizando declaraciones de aseveración assert() . Si hay una posible secuencia de ejecución que viola una aserción, la secuencia se imprime, de lo contrario se le da el "todo claro".

(Bueno, en realidad utiliza un algoritmo mucho más elegante y más rápido para lograr esto, pero ese es el efecto. De manera predeterminada, se verifican todos los estados de programa accesibles).

Este es un programa increíble , ganó el Premio al Software del Sistema ACM 2001 (otros ganadores incluyen Unix, Postscript, Apache, TeX). Comencé a usarlo muy rápidamente, y en un par de días pude implementar modelos de las funciones MPI MPI_Isend() y MPI_Irecv() en Promela. Spin encontró un par de difíciles condiciones de carrera en un segmento de código paralelo que convertí en Promela para las pruebas.

Answer 2

La detección de carreras de datos es un problema difícil de NP [Netzer & Miller 1990]

Escuché sobre las herramientas Lockset y DJit + (lo enseñan en el curso CDP). Intenta leer las diapositivas y buscar en Google a qué se refieren. Contiene alguna información interesante.

Answer 3

No sé qué plataforma o idioma está utilizando, pero en la plataforma .Net hay un proyecto de Microsoft Research llamado Chess que parece muy prometedor para ayudar a los que hacemos componentes de subprocesamiento múltiple, incluido el bloqueo.

No lo he usado una gran cantidad, mente.

Funciona (explicación cruda) al intercalar explícitamente los hilos de la manera más ajustada posible para forzar a sus insectos a salir de la naturaleza. También analiza el código para encontrar errores comunes y patrones malos, similar al análisis de código.

En el pasado, también he creado versiones especiales del código en cuestión (mediante #if bloques, etc.) que agregan información adicional de seguimiento de estado; recuentos, versiones, etc., que luego puedo sumergir en una prueba unitaria.

El problema con eso es que toma mucho más tiempo escribir su código, y no siempre puede agregar este tipo de cosas sin cambiar la estructura subyacente del código que ya está allí.

Answer 4

Si realmente desea verificar el código sin bloqueo (en lugar de probar exhaustivamente una pequeña instancia), puede usar VCC ( http://vcc.codeplex.com ), un verificador deductivo para el código C concurrente que se ha utilizado para verificar algunos algoritmos sin bloqueo interesantes (por ejemplo, listas sin bloqueo y tablas hash de tamaño variable que utilizan punteros de peligro, procesamiento de transacciones multiversión optimista, virtualización MMU, varias primitivas de sincronización, etc.). Realiza la verificación modular y se ha utilizado para verificar fragmentos no triviales de código industrial (hasta aproximadamente 20KLOC).

Sin embargo, tenga en cuenta que VCC es un verificador, no una herramienta de búsqueda de errores; Tendrá que hacer anotaciones sustanciales en su código para verificarlo, y la curva de aprendizaje puede ser un poco pronunciada. Tenga en cuenta también que asume consistencia secuencial (como lo hacen la mayoría de las herramientas).

Por cierto, la revisión por pares no es una buena manera de verificar un algoritmo concurrente (o incluso uno secuencial). Hay una larga historia de personas famosas que publican algoritmos concurrentes en revistas importantes, solo para tener errores descubiertos años más tarde.

Answer 5

Spin es realmente excelente, pero también considera Relacy Race Detector de Dmitriy V''jukov. Está diseñado específicamente para verificar algoritmos concurrentes, incluidos los algoritmos de no bloqueo (espera / bloqueo). Es de código abierto y licencia generosamente.

Relacy proporciona primitivas de sincronización POSIX y Windows (exclusión mutua, variables de condición, semáforos, CriticalSections, eventos win32, Enclavado *, etc.), por lo que su implementación real de C ++ se puede enviar a Relacy para su verificación. No es necesario desarrollar un modelo separado de su algoritmo como con Promela y Spin.

Relacy proporciona C ++ 0x std::atomic (¡ordenamiento de memoria explícito para el ganador!) Para que pueda usar #programas preprocesadores para seleccionar entre la implementación de Relacy y su propia implementación atómica específica de la plataforma ( tbb::atomic , boost::atomic , etc).

La programación es controlable: búsqueda aleatoria, vinculada al contexto y completa (todos los posibles entrecruzamientos) disponibles.

Aquí hay un ejemplo del programa Relacy. Algunas cosas a tener en cuenta:

• El $ es una macro Relacy que registra información de ejecución.
• rl::var<T> marca las variables "normales" (no atómicas) que también deben considerarse 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>();
}

Compile con su compilador normal (Relacy es solo de cabecera) y ejecute el 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 Java y CLI si te gusta ese tipo de cosas.