Как я могу проверить алгоритмы блокировки?

Ответ 1

Вам обязательно нужно попробовать Spin model checker.

Вы пишете программную модель на простом C-подобном языке под названием Promela, который Spin внутренне переводит в конечный автомат. Модель может содержать несколько параллельных процессов.

Что тогда делает Spin - это проверка каждого возможного чередования инструкций от каждого процесса для любых условий, которые вы хотите проверить - как правило, отсутствие условий гонки, свобода от тупиков и т.д. Большинство этих тестов можно легко написать с помощью операторов assert(). Если существует какая-либо возможная последовательность выполнения, которая нарушает утверждение, последовательность распечатывается, в противном случае вам предоставляется "все-ясно".

(Ну, на самом деле для этого используется гораздо более быстрый и быстрый алгоритм, но это эффект. По умолчанию проверяются все доступные состояния программ.)

Это невероятная программа, она выиграла в 2001 году Премия ACM System Software Award (другие победители включают Unix, Postscript, Apache, TeX). Я начал использовать его очень быстро, и через пару дней смог реализовать модели функций MPI MPI_Isend() и MPI_Irecv() в Promela. Спин нашел несколько сложных условий гонки в одном сегменте параллельного кода, который я преобразовал в Promela для тестирования.

Ответ 2

Спин действительно превосходный, но также рассмотрите Relacy Race Detector от Дмитрия Вюкова. Он предназначен для проверки параллельных алгоритмов, включая неблокирующие (ожидающие/блокирующие) алгоритмы. Это открытый и свободно лицензированный.

Relacy предоставляет примитивы синхронизации POSIX и Windows (мьютексы, переменные условий, семафоры, критические разделы, события win32, блокированные * и т.д.), поэтому ваша фактическая реализация на С++ может быть передана в Relacy для проверки. Не нужно разрабатывать отдельную модель вашего алгоритма, как с Promela и Spin.

Relacy предоставляет С++ 0x std::atomic (явное упорядочение памяти для выигрыша!), поэтому вы можете использовать предварительный процессор #defines для выбора между реализацией Relacy и собственной реализацией атома на платформе (tbb:: atomic, boost:: atomic и т.д.).

Планирование управляемо: возможен случайный, контекстно-зависимый и полный поиск (все возможные перемежения).

Здесь приведен пример программы Relacy. Несколько замечаний:

• $ - это макрос Relacy, который записывает информацию о выполнении.
• rl::var<T> содержит флажки "нормальные" (неатомические) переменные, которые также должны рассматриваться как часть проверки.

Код:

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

Скомпилируйте свой обычный компилятор (Relacy только для заголовка) и запустите исполняемый файл:

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)

Недавние версии Relacy также предоставляют модели памяти Java и CLI, если вы занимаетесь такими вещами.

Ответ 3

Я не знаю, какую платформу или язык вы используете, но на платформе .NET есть проект Microsoft Research под названием Chess, который выглядит очень многообещающим, помогая тем, кто из нас работает с многопоточными компонентами, включая блокировку.

Я не использовал это огромное количество, разум.

Он работает (грубое объяснение), явно чередуя потоки самым жестким способом, чтобы на самом деле заставить ваши ошибки выходить в дикую природу. Он также анализирует код, чтобы найти распространенные ошибки и плохие шаблоны - аналогично анализу кода.

В прошлом я также создавал специальные версии рассматриваемого кода (через блоки #if и т.д.), которые добавляют дополнительную информацию отслеживания состояния; количества, версии и т.д., после чего я могу окунуться в unit test.

Проблема заключается в том, что для написания кода требуется намного больше времени, и вы не можете всегда добавлять этот материал без изменения базовой структуры кода, который уже существует.

Ответ 4

Обнаружение гонки данных является трудной задачей NP [Netzer & Miller 1990]

Я слышал о инструментах Lockset и DJit + (они научить его в курсе CDP). Попробуйте прочитать слайды и пойдите в Google, на что они ссылаются. Он содержит интересную информацию.

Ответ 5

Если вы действительно хотите проверить код без блокировки (в отличие от исчерпывающего тестирования небольшого экземпляра), вы можете использовать VCC (http://vcc.codeplex.com), дедуктивный верификатор для параллельного кода C, который использовался для проверки некоторых интересных алгоритмов без блокировки (например, списки без блокировки и изменяемые по размеру хэш-таблицы с использованием указателей опасности, оптимизация многопользовательской транзакции, виртуализация MMU, различные примитивы синхронизации и т.д.), Он выполняет модульную проверку и используется для проверки нетривиальных фрагментов промышленного кода (до 20KLOC).

Обратите внимание, однако, что VCC является верификатором, а не средством поиска ошибок; вам нужно будет сделать существенную аннотацию на свой код, чтобы проверить его, и кривая обучения может быть немного крутой. Также обратите внимание, что он предполагает последовательную согласованность (как и большинство инструментов).

BTW, экспертная оценка не является хорошим способом проверки параллельного алгоритма (или даже последовательного). Там долгая история известных людей, публикующих параллельные алгоритмы в важных журналах, только для обнаружения ошибок, обнаруженных спустя годы.