2025-11-17T23:28:19.912332

Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language

Pedersen, Chalmers
Correct concurrent behaviour is important in understanding how components will act within certain conditions. In this work. we analyse the behaviour of shared communicating channels within a coorporatively scheduled runtime. We use the refinement checking and modelling tool FDR to develop both specifications of how such shared channels should behave and models of the implementations of these channels in the cooperatively scheduled language ProcessJ. Our results demonstrate that although we can certainly implement the correct behaviour of such channels, the outcome is dependant on having adequate resources available to execute all processes involved. We conclude that modelling the runtime environment of concurrent components is necessary to ensure components behave as specified in the real world.
academic

التحقق من صحة القنوات المشتركة في لغة موجهة للعمليات مع جدولة تعاونية

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

  • معرّف الورقة: 2510.11751
  • العنوان: التحقق من صحة القنوات المشتركة في لغة موجهة للعمليات مع جدولة تعاونية
  • المؤلفون: Jan Pedersen (جامعة نيفادا لاس فيغاس)، Kevin Chalmers (جامعة رافنسبورن)
  • التصنيف: cs.PL (لغات البرمجة)
  • تاريخ النشر: 12 أكتوبر 2025 (طبعة arXiv)
  • رابط الورقة: https://arxiv.org/abs/2510.11751

الملخص

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

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

خلفية المشكلة

  1. أهمية صحة البرامج المتزامنة: السلوك الصحيح للأنظمة المتزامنة حاسم لفهم كيفية عمل المكونات في ظروف معينة. على الرغم من أن طرق الاختبار التقليدية تُستخدم على نطاق واسع، إلا أنها قد تفشل في اكتشاف جميع الأخطاء المتزامنة المحتملة.
  2. ضرورة التحقق الرسمي: يستشهد المؤلفون ببرنامج مستكشف المريخ كمثال، موضحين أن خطأ بسيط في الجمود قد يتطلب انتظار 8 ملايين ثانية (أكثر من 90 يوماً) لاحتمالية 50% من اكتشافه عند الاختبار، بينما يمكن للتحقق الرسمي باستخدام CSP و FDR اكتشاف مثل هذه الأخطاء فوراً.
  3. تحديات التحقق من نظام التشغيل: نظراً لأن عدداً كبيراً من البرامج مبنية على أنظمة التشغيل للغات البرمجة، أصبح ضمان خلو نظام التشغيل من الأخطاء والتصرف وفقاً للمواصفات حاسماً.

حدود الطرق الموجودة

  1. إهمال بيئة التنفيذ: لم تقم طرق التحقق التقليدية المستندة إلى أنظمة القنوات بنمذجة نظام التشغيل أو نظام التنفيذ أو الأجهزة وغيرها، بافتراض أن أحداث الجاهزية ستبقى متاحة حتى يتم جدولتها.
  2. افتراض ندرة الموارد: تفترض طرق النمذجة القياسية أن الأحداث يمكن أن تحدث فوراً، مما يعني أن الموارد متاحة عند تنفيذ الحدث، لكن هذا الافتراض المتطرف لا ينطبق في الواقع.
  3. تأثير بيئة الجدولة: يجب على العمليات الانتظار في نهاية قائمة الجاهزية ليتم جدولتها، وأحداثها لن تكون متاحة فوراً، لكن الطرق التقليدية لم تأخذ هذا في الاعتبار.

دافع البحث

ProcessJ هي لغة برمجة موجهة للعمليات تستند إلى دلالات CSP، وتستخدم جدولة تعاونية وتعمل على JVM. تهدف هذه الورقة إلى التحقق من صحة تنفيذ القنوات المشتركة في وقت تشغيل ProcessJ، مع التركيز بشكل خاص على تأثير بيئة الجدولة على سلوك القنوات.

المساهمات الأساسية

  1. التحقق من صحة تنفيذ القنوات المشتركة في ProcessJ: أثبتت أن تنفيذ القنوات المشتركة في ProcessJ باستخدام جدولة تعاونية موجودة صحيح، من خلال التحقق من تحسين الترجمة CSP والنموذج المشترك للقنوات المشتركة.
  2. تطوير إثبات جبري موسع لمواصفات القنوات المشتركة: توفير إثبات رسمي بأن مواصفات القنوات المشتركة تتصرف بالفعل كقنوات مشتركة CSP.
  3. إثبات إضافي للعلاقة بين الموارد والعمليات النشطة: إظهار مرة أخرى العلاقة بين الموارد المتاحة وعدد العمليات النشطة لتحقيق المواصفات، مما يثبت أن عدد جدولات العمليات المتاحة يجب أن يكون مساوياً أو أكبر من عدد العمليات في النظام.

شرح الطريقة

تعريف المهمة

المهمة الأساسية لهذه الورقة هي التحقق من صحة تنفيذ القنوات المشتركة في لغة ProcessJ. يتضمن ذلك بشكل محدد:

  • المدخلات: كود تنفيذ Java للقنوات المشتركة في ProcessJ ومواصفات CSP
  • المخرجات: نتائج التحقق، التي تثبت ما إذا كان التنفيذ يتوافق مع المواصفات
  • القيود: الأخذ في الاعتبار حدود الموارد في بيئة جدولة تعاونية

معمارية النموذج

1. إطار نمذجة CSP

استخدام العمليات المتسلسلة المتصلة (CSP) كلغة نمذجة رسمية:

  • العمليات: مكونات مجردة، يتم تعريفها من خلال الأحداث التي تنفذها
  • الأحداث: عمليات اتصال ذرية وتزامنية وفورية
  • القنوات: وسيط الاتصال بين العمليات

2. نمذجة نظام الجدولة

SCHEDULER = 
  rqdequeue?p → -- إزالة عملية من قائمة الانتظار
  run.p → -- تشغيلها
  yield.p → -- انتظار الاستسلام
  SCHEDULER -- تكرار

SCHEDULE_MANAGER = 
  schedule?pid → -- انتظار حدث الجدولة
  rqenqueue!pid → -- وضع العملية في قائمة التشغيل
  SCHEDULE_MANAGER -- تكرار

3. نمذجة بيانات وصف العملية

تحتاج كل عملية إلى مراقب وعلم تشغيل وعلم جاهزية:

PROCESS(p) = 
  VARIABLE(ready.p, true)
  ||| VARIABLE(running.p, false)
  ||| MONITOR(claim_process.p, release_process.p)

4. نمذجة القنوات المشتركة

  • قنوات متعدد-إلى-واحد: عمليات كتابة متعددة، عملية قراءة واحدة
  • قنوات واحد-إلى-متعدد: عملية كتابة واحدة، عمليات قراءة متعددة
  • قنوات متعدد-إلى-متعدد: عمليات كتابة متعددة، عمليات قراءة متعددة

نقاط الابتكار التقني

1. طريقة التحقق مع الأخذ في الاعتبار بيئة الجدولة

بخلاف الطرق التقليدية، تقوم هذه الورقة بنمذجة صريحة لجدولة تعاونية، مما يسمح باكتشاف المشاكل التي تظهر فقط في ظروف جدولة معينة.

2. فحص التحسين تحت قيود الموارد

من خلال تغيير عدد جدولات العمليات، تم دراسة التغييرات في سلوك النظام تحت تكوينات موارد مختلفة، واكتشاف العلاقة بين كفاية الموارد والصحة.

3. الترجمة ثنائية الاتجاه من التنفيذ إلى المواصفات

  • كود ProcessJ → كود Java → نموذج CSP
  • إنشاء سلسلة ترجمة كاملة لضمان موثوقية نتائج التحقق

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

أدوات التحقق

  • FDR (فحص التحسين الفشل-الاختلاف): أداة فحص تحسين CSP
  • CSPM: نسخة قابلة للقراءة من قبل الآلة من CSP

نماذج التحقق

استخدام ثلاثة نماذج دلالية للتحليل:

  1. نموذج الآثار: بناءً على السلوك المرصود خارجياً
  2. نموذج الفشل المستقر: التعامل مع الأحداث التي قد ترفضها العملية
  3. نموذج الفشل-الاختلاف: التعامل مع سيناريوهات الجمود المحتملة

تكوينات الاختبار

  • تكوينات العمليات: مجموعات متنوعة من 1-2 عملية كتابة و1-3 عمليات قراءة
  • عدد جدولات العمليات: من 1 إلى 4 جدولات
  • أنواع القنوات: قنوات مشتركة واحد-إلى-متعدد، متعدد-إلى-واحد، متعدد-إلى-متعدد

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

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

| نوع القناة | تكوين العمليات | إجمالي العمليات | عدد جدولات العمليات ||||| |----------|----------|----------|--|--|--|--| | | | | 1| 2| 3| 4| | واحد-إلى-متعدد | 1 كتابة-2 قراءة | 3 | ✓| ✓| ✗| ✗| | واحد-إلى-متعدد | 1 كتابة-3 قراءة | 4 | ✓| ✓| ✓| ✗| | متعدد-إلى-واحد | 2 كتابة-1 قراءة | 3 | ✓| ✓| ✗| ✗| | متعدد-إلى-واحد | 3 كتابة-1 قراءة | 4 | ✓| ✓| ✓| ✗| | متعدد-إلى-متعدد | 2 كتابة-2 قراءة | 4 | ✓| ✓| ✓| ✗|

شرح الرموز:

  • ✓ = نجح فحص تحسين الآثار
  • ✗ = نجح فحص تحسين الفشل
  • ✗✗ = فشل فحص التحسين

الاكتشافات الرئيسية

  1. نظرية كفاية الموارد: عندما يكون عدد جدولات العمليات مساوياً أو أكبر من إجمالي عدد العمليات، يمكن تحقيق التحسين في كلا الاتجاهين في نموذج الفشل.
  2. تأثير نقص الموارد:
    • عندما تكون جدولات العمليات غير كافية، يمكن الحصول على تحسين الآثار فقط وليس تحسين الفشل
    • هذا لا يعني أن النظام سيتعطل، بل أن بعض الآثار لن تكون قابلة للتنفيذ
  3. تأثير قائمة الجدولة: تفرض قائمة التشغيل ترتيباً طبيعياً على العمليات، وعندما تكون جدولات العمليات غير كافية، قد لا تتضمن مجموعة القبول الكلية للنظام مجموعات قبول بعض العمليات.

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

مجال التحقق الرسمي

  • التحقق من CSO و JCSP: أعمال سابقة تحقق من أنظمة التشغيل الأخرى، لكنها أهملت بيئة التنفيذ
  • فحص نموذج SPIN: تستخدم أنظمة أخرى طرق تحقق مماثلة، لكنها عادة ما تفترض جدولة استباقية

أبحاث الجدولة التعاونية

  • جدولة occam-π: جدولة ProcessJ مشابهة لجدولة متعددة المعالجات التعاونية في occam-π
  • أنماط غير متزامنة/انتظار: تصبح المهام المتعددة التعاونية شائعة بشكل متزايد في JavaScript و Python و C++ و Rust

مزايا هذه الورقة

  1. أول من يأخذ بيئة الجدولة في الاعتبار: نمذجة صريحة لجدولة تعاونية في التحقق
  2. اكتشاف المشاكل المتعلقة بالجدولة: القدرة على اكتشاف مشاكل مثل الجمود التي تظهر فقط في ظروف جدولة معينة
  3. التحقق الذي يدرك الموارد: تحديد كمي للعلاقة بين احتياجات الموارد والصحة

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

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

  1. صحة التنفيذ: تنفيذ القنوات المشتركة في ProcessJ صحيح في حالة توفر جدولات عمليات كافية.
  2. الاعتماد على الموارد: يعتمد السلوك الصحيح على توفر موارد جدولة كافية لتنفيذ جميع العمليات ذات الصلة.
  3. ضرورة النمذجة: نمذجة بيئة التشغيل ضرورية لضمان أن تتصرف المكونات وفقاً للمواصفات في العالم الحقيقي.

القيود

  1. استخدام الأقفال: يستخدم التنفيذ الحالي بكثرة الأقفال/المراقبين، مما قد يؤثر على التزامن والأداء.
  2. متطلبات جدولة العمليات: قد يكون الحاجة إلى عدد جدولات عمليات مساوٍ لعدد العمليات غير عملي في التطبيقات الفعلية.
  3. تعقيد التحقق: ينمو فضاء الحالة للتحقق بسرعة مع زيادة عدد العمليات.

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

  1. تنفيذ خالٍ من الأقفال:
    • استخدام متغيرات ذرية بدلاً من الأقفال
    • تنفيذ هياكل قائمة الانتظار الخالية من الانتظار
    • تطوير نماذج CSP تدعم عمليات المقارنة والتبديل
  2. تبسيط المواصفات:
    • تطوير طرق بناء نماذج CSP خفيفة الوزن
    • دراسة سلوك ProcessJ تحت ظروف جدولة مختلفة
  3. تحسين جدولة العمليات:
    • البحث عما إذا كان يمكن تحقيق تحسين الفشل بعدد جدولات عمليات أقل من عدد العمليات
    • تحليل متطلبات جدولة العمليات لبرامج مختلفة

التقييم المتعمق

المزايا

  1. الابتكار في الطريقة:
    • أول من يأخذ بيئة الجدولة التعاونية في الاعتبار في التحقق الرسمي
    • إنشاء سلسلة تحقق كاملة من التنفيذ إلى المواصفات
  2. المساهمات النظرية:
    • توفير إثبات جبري صارم لمواصفات القنوات المشتركة
    • تحديد كمي للعلاقة بين احتياجات الموارد والصحة
  3. القيمة العملية:
    • التحقق من صحة نظام التشغيل الفعلي
    • توفير طريقة تحقق لأنظمة جدولة تعاونية أخرى
  4. كفاية التجربة:
    • اختبار تكوينات قنوات متعددة وأعداد جدولات عمليات
    • استخدام طريقة تحقق صارمة من CSP/FDR

أوجه القصور

  1. مشاكل قابلية التوسع:
    • تنمو تعقيدية التحقق بشكل أسي مع عدد العمليات
    • قد تحد الحاجة إلى عدد كبير من جدولات العمليات من التطبيقات العملية
  2. اعتبارات الأداء غير كافية:
    • قد يؤثر الاستخدام الكثيف للأقفال على أداء النظام
    • لم يتم مناقشة تكاليف التحقق بشكل كافٍ
  3. قيود نطاق التطبيق:
    • موجهة بشكل أساسي نحو لغة ProcessJ
    • تحتاج قابلية التطبيق على أنظمة جدولة تعاونية أخرى إلى مزيد من التحقق

التأثير

  1. المساهمة الأكاديمية:
    • توفير أفكار تحقق جديدة لمجالات لغات البرمجة والطرق الرسمية
    • دفع تطور طرق التحقق التي تأخذ بيئة التنفيذ في الاعتبار
  2. القيمة العملية:
    • تحسين موثوقية وقت تشغيل ProcessJ
    • توفير مرجع لتحقق وقت التشغيل للغات أخرى
  3. قابلية التكرار:
    • توفير كود CSP كامل وسكريبتات اختبار
    • يمكن تكرار عملية التحقق والنتائج بشكل مستقل

السيناريوهات المناسبة

  1. لغات البرمجة الموجهة للعمليات: مناسبة بشكل خاص للتحقق من وقت التشغيل للغات المستندة إلى دلالات CSP
  2. أنظمة الجدولة التعاونية: يمكن تطبيقها على أنظمة متزامنة أخرى تستخدم جدولة تعاونية
  3. تطوير الأنظمة الحرجة: مناسبة لتطوير أنظمة متزامنة تتطلب درجة عالية من الصحة

المراجع

تستشهد هذه الورقة بـ 51 مرجعاً ذا صلة، تتضمن بشكل أساسي:

  1. نظرية أساسيات CSP: الأعمال الكلاسيكية لـ Hoare حول CSP والنظرية ذات الصلة
  2. أدوات التحقق الرسمي: أداة FDR وطرق التحقق ذات الصلة
  3. لغات البرمجة المتزامنة: الأبحاث المتعلقة بلغات JCSP و occam-π و Go و Erlang وغيرها
  4. خوارزميات الجدولة: الأعمال ذات الصلة بخوارزميات الاستبعاد المتبادل والخوارزميات المتزامنة
  5. الأعمال السابقة للمؤلفين: سلسلة من الأبحاث حول التحقق من وقت تشغيل ProcessJ

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