Проблемы верификации при умножении разреженной матрицы на вектор в высокопроизводительных вычислениях: Часть I

Основная информация

• ID статьи: 2510.13427
• Название: Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I
• Автор: Junchao Zhang (Argonne National Laboratory)
• Классификация: cs.LO cs.DC cs.MS
• Конференция: International Workshop on Verification of Scientific Software (VSS 2025)
• Информация о публикации: EPTCS 432, 2025, стр. 98–105
• Ссылка на статью: https://arxiv.org/abs/2510.13427

Аннотация

Умножение разреженной матрицы на вектор (SpMV) является фундаментальным ядром в научных кодах, использующих итеративные решатели. В первой части нашей работы мы представляем как последовательную, так и базовую MPI параллельную реализацию SpMV с целью предоставить задачу-вызов для сообщества верификации научного программного обеспечения. Реализации описаны в контексте библиотеки PETSc.

Исследовательский контекст и мотивация

Определение проблемы

Данное исследование посвящено проблемам верификации программного обеспечения для умножения разреженной матрицы на вектор (SpMV) в высокопроизводительных вычислениях. SpMV является основной операцией при решении разреженных систем линейных уравнений Ax=b и широко применяется в научных вычислительных кодах, основанных на итеративных решателях, особенно в методах подпространства Крылова большого масштаба.

Значимость

1. Фундаментальность: SpMV является базовым алгоритмом научных вычислений, и его корректность напрямую влияет на надежность приложений более высокого уровня
2. Сложность: Несмотря на простоту математического определения (yi = Σ(aij·xj)), форматы хранения, распределение данных, параллелизация и оптимизация делают реализацию сложной
3. Проблемы верификации: Существующие высокооптимизированные реализации создают значительные трудности для верификации программного обеспечения

Ограничения существующих подходов

• Библиотека PETSc содержит высокооптимизированные MPI параллельные реализации SpMV, но их сложность затрудняет верификацию
• Отсутствуют стандартизированные задачи-вызовы, специально разработанные для сообщества верификации программного обеспечения

Исследовательская мотивация

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

Основные вклады

1. Предоставление стандартизированной задачи верификации: Разработаны стандартные тестовые случаи SpMV для сообщества верификации научного программного обеспечения
2. Реализация двух алгоритмов SpMV различной сложности:
   • Последовательная реализация (seq.c)
   • Базовая MPI параллельная реализация (mpibasic.c)
3. Установление полной структуры верификации: Включая генерацию входных данных, проверку корректности и механизмы обнаружения ошибок
4. Четкое определение целей верификации: Предоставление конкретных требований верификации и вызовов для каждой реализации

Подробное описание методологии

Определение задачи

Входные данные:

• Разреженная матрица A (M×N, NNZ ненулевых элементов), хранящаяся в формате CSR
• Вектор x (N-мерный)
• Ожидаемый результат z = Ax (M-мерный)

Выходные данные:

• Вычисленный результат y = Ax
• Проверка корректности: ||y-z||² должна быть равна 0 (с учетом ошибок округления с плавающей точкой)

Ограничения:

• Использование сжатого формата разреженных строк (CSR)
• Поддержка распределенных вычислений MPI

Проектирование структур данных

Представление в формате CSR

Разреженная матрица A представляется тремя массивами:

• a[nnz]: хранит значения ненулевых элементов
• j[nnz]: хранит индексы столбцов ненулевых элементов
• i[m+1]: указатели строк, ik указывает на начальную позицию k-й строки в массивах a и j

Определение типов данных

// Последовательная версия
typedef struct {
    int m, n;        // размеры матрицы
    int *i, *j;      // индексы формата CSR
    double *a;       // значения ненулевых элементов
} Mat;

// MPI параллельная версия
typedef struct {
    int m, n, M, N;  // локальные и глобальные размеры
    int rstart, cstart; // начальные индексы строк и столбцов
    int *i, *j;
    double *a;
} Mat;

Реализация алгоритмов

Последовательная реализация

for (i = 0; i < A.m; i++) {
    y.a[i] = 0.0;
    for (j = A.i[i]; j < A.i[i + 1]; j++)
        y.a[i] += A.a[j] * x.a[A.j[j]];
}

MPI параллельная реализация

1. Стратегия распределения данных:
   • Матрица распределяется по блокам строк: m = M/size + (M%size > rank ? 1 : 0)
   • Вектор x распределяется по столбцам: n = N/size + (N%size > rank ? 1 : 0)
2. Модель коммуникации:
   • Использование MPI_Allgather или MPI_Allgatherv для сбора полного вектора x
   • Использование MPI_Allreduce для вычисления глобальной нормы
3. Вычислительный процесс:
   • Вычисление локального расположения матрицы (rstart, cstart)
   • Извлечение локальных данных из глобальных массивов
   • Сбор распределенного вектора x в локальную полную копию X
   • Выполнение локального вычисления SpMV
   • Вычисление локальной нормы ошибки и глобальная редукция

Технические инновации

1. Проектирование прогрессивной сложности: От простой последовательной реализации к базовой параллельной, облегчая прогрессивное тестирование инструментов верификации
2. Стандартизированный интерфейс верификации: Предоставление единого формата входных/выходных данных и механизма проверки корректности
3. Контекст реальных приложений: Основано на реальных моделях реализации библиотеки PETSc с практической значимостью
4. Расширяемая структура: Закладывает основу для более сложных оптимизированных версий (Часть II)

Экспериментальная установка

Наборы данных

• Размер матрицы: Матрица 32×36 с 50 ненулевыми элементами
• Генерация данных: Использование сопроводительного скрипта Python csr.py для генерации тестовых данных
• Жестко закодированные входные данные: Для упрощения использования тестовые данные встроены непосредственно в исходный код
• Настраиваемость: Пользователи могут изменять параметры скрипта Python для генерации различных тестовых случаев

Метрики оценки

• Проверка корректности: Вычисление квадратной нормы ||y-z||²
• Критерий успеха: Норма ≤ 1e-6 (с учетом ошибок округления с плавающей точкой)
• Коды возврата: Возврат 0 при корректности, ненулевое значение при ошибке

Детали реализации

• Язык программирования: C
• Параллельная структура: MPI
• Требования компиляции: Требуется только компилятор C или компилятор MPI
• Доступность кода: Открыто опубликовано в репозитории GitHub

Результаты экспериментов

Целевые показатели верификации

Требования верификации последовательной реализации

Проверка того, что вычисленный результат y удовлетворяет: yi = Σ(aij·xj), где aij, не хранящиеся в представлении CSR, рассматриваются как 0

Требования верификации MPI параллельной реализации

1. Корректность расположения: Проверка Σm = M, Σn = N
2. Корректность локальных вычислений: Проверка того, что y на каждом процессе является корректным результатом произведения соответствующей локальной подматрицы на полный вектор x

Тестовые случаи

Статья предоставляет конкретные тестовые данные:

• Входная матрица: разреженная матрица 32×36 (50 ненулевых элементов)
• Входной вектор: 36-мерный вектор
• Ожидаемый выход: 32-мерный результирующий вектор
• Все данные предоставлены в виде целочисленных и вещественных массивов

Связанные работы

Смежные области исследований

1. Методы подпространства Крылова: SpMV является основным компонентом итеративных решателей
2. Библиотека PETSc: Предоставляет богатый набор методов Крылова и реализаций SpMV
3. Верификация научного программного обеспечения: Проверка корректности высокопроизводительного научного вычислительного программного обеспечения

Позиционирование данной работы

• Заполняет пробел в отсутствии стандартизированных задач верификации SpMV в сообществе верификации научного программного обеспечения
• Предоставляет базовую справку для верификации сложных оптимизированных реализаций
• Связывает теоретические методы верификации с практическими потребностями приложений HPC

Выводы и обсуждение

Основные выводы

1. Успешно установлена стандартизированная задача-вызов для верификации программного обеспечения SpMV
2. Предоставлены две реализации различной сложности, подходящие для прогрессивного тестирования инструментов верификации
3. Основано на реальных моделях библиотеки PETSc с практической ценностью приложений

Ограничения

1. Ограничение масштаба: Текущие тестовые случаи имеют небольшой размер (матрица 32×36)
2. Отсутствие оптимизаций: Базовая MPI реализация не включает сложные оптимизации, присутствующие в производственной среде
3. Область верификации: Охватывает только базовую корректность, не затрагивает верификацию производительности и численной стабильности

Направления будущих исследований

1. Разработка Части II: Планируется предоставить более сложные оптимизированные MPI реализации в последующих работах
2. Расширение тестовых случаев: Добавление тестовых матриц большего размера и с различными моделями разреженности
3. Интеграция инструментов верификации: Интеграционное тестирование с существующими инструментами верификации

Глубокая оценка

Преимущества

1. Высокая практическая ценность: Решает реальные потребности сообщества верификации научного программного обеспечения
2. Рациональное проектирование: Проектирование прогрессивной сложности облегчает разработку и тестирование инструментов верификации
3. Высокая степень стандартизации: Предоставляет полные спецификации входных/выходных данных и механизм проверки корректности
4. Сильная воспроизводимость: Код открыто доступен, тестовые данные встроены, легко воспроизводится
5. Практический контекст: Основано на широко используемой библиотеке PETSc с реальной ценностью приложений

Недостатки

1. Недостаток теоретического анализа: Отсутствует анализ сложности алгоритма или обсуждение теоретических свойств
2. Ограниченное покрытие тестами: Предоставляется только один тестовый случай, недостаточное разнообразие
3. Глубина верификации: Основное внимание уделяется функциональной корректности, отсутствует анализ численной точности и граничных условий
4. Рассмотрение производительности: Не затрагивает проблемы верификации производительности

Влияние

1. Вклад в область: Предоставляет важную стандартизированную платформу тестирования для верификации научного программного обеспечения
2. Практическая ценность: Может быть непосредственно использована для разработки и оценки инструментов верификации
3. Расширяемость: Закладывает основу для последующих более сложных реализаций
4. Ценность для сообщества: Способствует сотрудничеству между сообществами HPC и верификации программного обеспечения

Применимые сценарии

1. Разработка инструментов верификации: Использование в качестве стандартных тестовых случаев для проверки эффективности инструментов
2. Применение в образовании: Подходит в качестве учебного примера для параллельных вычислений и верификации программного обеспечения
3. Тестирование производительности: Может служить эталонной базой для корректности реализаций SpMV
4. Исследовательская платформа: Предоставляет стандартизированную платформу для исследований связанных алгоритмов и оптимизаций

Библиография

1. S Balay et al. (2025): PETSc/TAO Users Manual. Technical Report ANL-21/39 - Revision 3.23, Argonne National Laboratory
2. Yousef Saad (2003): Iterative Methods for Sparse Linear Systems, second edition. Society for Industrial and Applied Mathematics

Общая оценка: Это практически ценная работа, которая, хотя и имеет ограниченный вклад в теоретические инновации, предоставляет срочно необходимую стандартизированную задачу-вызов для сообщества верификации научного программного обеспечения. Статья имеет четкую структуру, полную реализацию, хорошую воспроизводимость и расширяемость, имея значительную ценность для развития области верификации программного обеспечения HPC.