2025-11-10T02:34:56.080990

Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I

Zhang
Sparse matrix vector multiplication (SpMV) is a fundamental kernel in scientific codes that rely on iterative solvers. In this first part of our work, we present both a sequential and a basic MPI parallel implementations of SpMV, aiming to provide a challenge problem for the scientific software verification community. The implementations are described in the context of the PETSc library.
academic

تحديات التحقق من صحة ضرب المصفوفة المتفرقة بالمتجه في الحوسبة عالية الأداء: الجزء الأول

المعلومات الأساسية

  • معرّف الورقة: 2510.13427
  • العنوان: Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I
  • المؤلف: Junchao Zhang (مختبر أرغون الوطني)
  • التصنيف: cs.LO cs.DC cs.MS
  • المؤتمر المنشور فيه: ورشة العمل الدولية للتحقق من صحة البرامج العلمية (VSS 2025)
  • معلومات النشر: EPTCS 432, 2025, pp. 98–105
  • رابط الورقة: https://arxiv.org/abs/2510.13427

الملخص

ضرب المصفوفة المتفرقة بالمتجه (SpMV) هو نواة أساسية في الأكواد العلمية التي تعتمد على المحللات التكرارية. في هذا الجزء الأول من عملنا، نقدم تطبيقات متسلسلة وأساسية متوازية MPI لـ SpMV، بهدف توفير مشكلة تحدٍ لمجتمع التحقق من صحة البرامج العلمية. يتم وصف التطبيقات في سياق مكتبة PETSc.

الخلفية البحثية والدافع

تعريف المشكلة

يتناول هذا البحث تحديات التحقق من صحة البرامج لعملية ضرب المصفوفة المتفرقة بالمتجه (SpMV) في الحوسبة عالية الأداء. تعتبر عملية SpMV العملية الأساسية لحل أنظمة المعادلات الخطية المتفرقة Ax=b، وتُستخدم على نطاق واسع في أكواد الحوسبة العلمية التي تعتمد على المحللات التكرارية، خاصة في طرق فضاء Krylov الفرعي واسعة النطاق.

الأهمية

  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||² مساوية للصفر (مع تجاهل أخطاء التقريب العددي)

القيود:

  • استخدام صيغة الصفوف المتفرقة المضغوطة (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. إطار عمل قابل للتوسع: يضع الأساس للإصدارات المحسّنة الأكثر تعقيداً (الجزء الثاني)

إعداد التجارب

مجموعات البيانات

  • حجم المصفوفة: مصفوفة 32×36 تحتوي على 50 عنصر غير صفري
  • توليد البيانات: استخدام سكريبت Python المرفق csr.py لتوليد بيانات الاختبار
  • الإدخال المدمج: لتبسيط الاستخدام، يتم دمج بيانات الاختبار مباشرة في الكود المصدري
  • القابلية للتخصيص: يمكن للمستخدمين تعديل معاملات سكريبت Python لتوليد حالات اختبار مختلفة

مؤشرات التقييم

  • التحقق من الصحة: حساب معيار النطاق المربع ||y-z||²
  • معايير النجاح: المعيار ≤ 1e-6 (مع الأخذ في الاعتبار أخطاء التقريب العددي)
  • رموز الإرجاع: إرجاع 0 عند الصحة، وقيمة غير صفرية عند الخطأ

تفاصيل التطبيق

  • لغة البرمجة: لغة C
  • إطار العمل المتوازي: MPI
  • متطلبات الترجمة: يتطلب فقط مترجم C أو مترجم MPI
  • توفر الكود: منشور علناً في مستودع GitHub

نتائج التجارب

أهداف التحقق

متطلبات التحقق من التطبيق المتسلسل

التحقق من أن النتيجة المحسوبة y تحقق: yi = Σ(aij·xj)، حيث يتم اعتبار aij التي لم يتم تخزينها في تمثيل CSR كصفر

متطلبات التحقق من التطبيق المتوازي MPI

  1. صحة التخطيط: التحقق من أن Σm = M, Σn = N
  2. صحة الحساب المحلي: التحقق من أن y على كل عملية هي نتيجة الضرب الصحيحة للمصفوفة الفرعية المحلية بالمتجه الكامل x

حالات الاختبار

توفر الورقة بيانات اختبار محددة:

  • مصفوفة الإدخال: مصفوفة متفرقة 32×36 (50 عنصر غير صفري)
  • متجه الإدخال: متجه بحجم 36
  • الإخراج المتوقع: متجه نتيجة بحجم 32
  • يتم توفير جميع البيانات في شكل مصفوفات أعداد صحيحة وأرقام عشرية

الأعمال ذات الصلة

مجالات البحث ذات الصلة

  1. طرق فضاء Krylov الفرعي: تعتبر عملية SpMV المكون الأساسي للمحللات التكرارية
  2. مكتبة PETSc: توفر مجموعة غنية من طرق Krylov وتطبيقات SpMV
  3. التحقق من صحة البرامج العلمية: موجهة للتحقق من صحة برامج الحوسبة العلمية عالية الأداء

موضع هذه الورقة

  • ملء الفراغ في نقص مشاكل التحدي الموحدة للتحقق من SpMV في مجتمع التحقق من صحة البرامج العلمية
  • توفير مرجع أساسي للتحقق من التطبيقات المحسّنة المعقدة
  • ربط طرق التحقق النظرية باحتياجات تطبيقات HPC الفعلية

الخلاصة والمناقشة

الاستنتاجات الرئيسية

  1. تم بنجاح إنشاء مشكلة تحدٍ موحدة للتحقق من صحة برامج SpMV
  2. توفير تطبيقات بدرجات تعقيد مختلفة، مناسبة للاختبار التدريجي لأدوات التحقق
  3. بناءً على أنماط مكتبة PETSc الحقيقية، ذات قيمة تطبيقية عملية

القيود

  1. قيود الحجم: حالات الاختبار الحالية بحجم صغير نسبياً (مصفوفة 32×36)
  2. غياب التحسينات: التطبيق المتوازي الأساسي لا يتضمن التحسينات المعقدة في بيئات الإنتاج الفعلية
  3. نطاق التحقق: يغطي فقط الصحة الأساسية، ولا يتناول التحقق من الأداء والاستقرار العددي

الاتجاهات المستقبلية

  1. تطوير الجزء الثاني: يُخطط لتوفير تطبيقات 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. التقرير الفني ANL-21/39 - المراجعة 3.23، مختبر أرغون الوطني
  2. Yousef Saad (2003): طرق تكرارية للأنظمة الخطية المتفرقة، الطبعة الثانية. جمعية الرياضيات الصناعية والتطبيقية

التقييم الإجمالي: هذا عمل عملي قوي جداً، وعلى الرغم من أن مساهمته في الابتكار النظري محدودة، إلا أنه يوفر مشكلة تحدٍ موحدة مطلوبة بشدة لمجتمع التحقق من صحة البرامج العلمية. تتمتع الورقة بهيكل واضح وتطبيق شامل وقابلية جيدة للإعادة والتوسع، وتتمتع بقيمة مهمة في تعزيز تطور مجال التحقق من صحة برامج HPC.