pgo

PGO

PGO هو مصدر لمجمول البرمجي الذي يترجم مواصفات PlusCal Modular (التي تستخدم مجموعة Superset of PlusCal) إلى برامج GO.

بالإضافة إلى مترجم PGO ، تتضمن شجرة المصدر هذه:

• مكتبة دعم distsys ، والتي تستخدمها رمز GGO الذي تم إنشاؤه من PGO ، متوفرة في المجلد distsys/ المجلد.
• الأنظمة التي تم تصميمها باستخدام PGO في systems/ المجلد ، بما في ذلك متجر قيمة مفاتيح قائم على الطوافة.
• بناء جملة تسليط الضوء على رمز الاستوديو المرئي والقطار ، المتوفرة في syntax/ المجلد.

يمكنك قراءة المزيد حول الجوانب البحثية لعملنا في ورقة ASPLOS'23 ، والتي يتم تضمين نسخة منها في هذا المستودع. تقييمنا لجائزة PGO المميزة للثقة في هذا المؤتمر؟

لدينا أيضًا بعض مقاطع الفيديو التي يمكنك مشاهدتها:

• PGO TLA+ Conference Talk ، سبتمبر 2022
• PGO Overview Talk ، فبراير 2022.

الغرض والدافع

PlusCal هي لغة لتحديد/نمذجة الأنظمة المتزامنة. تم تصميمه لتسهيل كتابة TLA+. على وجه الخصوص ، يمكن تجميع PlusCal في TLA+، والتي يمكن فحصها مقابل خصائص النظام المفيدة (باستخدام مدقق نموذج TLC). على سبيل المثال ، فيما يلي مستودع من تركيبات PlusCal للحلول لمشكلة الاستبعاد المتبادل.

GO هي لغة قائمة على C تم تطويرها بواسطة Google لبناء أنظمة موزعة. لقد بنيت في الدعم للتزامن مع القنوات ، والغرورات ، مما يجعلها رائعة لتطوير الأنظمة الموزعة.

لا توجد حاليًا أي أدوات تتوافق مع المواصفات PlusCal/TLA+ مع تنفيذ المواصفات. PGO هي أداة تهدف إلى توصيل المواصفات بالتنفيذ عن طريق إنشاء رمز GO استنادًا إلى مواصفات مكتوبة في Modular PlusCal. تأتي البادئة "المعيارية" من الحاجة إلى التمييز بين وصف النظام عن نموذج بيئته ، وهو أمر مطلوب لفحص النماذج. يتيح PGO ترجمة وصف Plus -Plus المعياري للنظام الموزع إلى PlusAcal يمكن التحقق منه ، وكذلك لبرنامج GO المكافئ بشكل دلالي.

الوضع الحالي

بنشاط قيد التطوير. PGO يدعم تجميع جميع بنيات تدفق التحكم PlusCal. يدعم PGO أيضًا الغالبية العظمى من TLA+ على مستوى القيمة المدعومة من TLC. راجع طلبات السحب وقضايا توثيق العمل المستمر.

في حالة التطوير الفعلي ، لا نقدم إصدارات مستقرة. لتشغيل PGO ، فإن أفضل طريقة هي استنساخ المستودع ، وعلى الفرع الرئيسي ، قم بتشغيله عبر أداة بناء SBT:

 $ sbt
> run [command-line arguments]

راجع ملاحظات الاستخدام أدناه لما يقبله البرنامج. ملاحظة: إذا قمت بتشغيله على سطر واحد ، فيجب عليك اقتباس الوسائط ، كما هو الحال في sbt run "[command-line arguments]" .

الاستخدام

لمعرفة كيفية استخدام PGO أثناء التحقق ، راجع صفحة استخدام PGO (تحذير: تحديث قيد التقدم).

للاطلاع على أوضاع تجميع الأداة وأعلامها على مستوى عالٍ ، انظر أدناه.

يقرأ نص مساعدة أداة PGO:

 PGo compiler
  -h, --help   Show help message

Subcommand: gogen
  -o, --out-file  <arg>
  -p, --package-name  <arg>
  -s, --spec-file  <arg>
  -h, --help                  Show help message

Subcommand: pcalgen
  -s, --spec-file  <arg>
  -h, --help               Show help message

جين

تطلب اللجنة الفرعية gogen أن تقوم PGO بإنشاء ملف GO من وحدة TLA+ تحتوي على MPCAL. يجب إجراء معظم تخصيص هذه المرحلة عن طريق اختيار معلمات محددة عند الاتصال برمز GO الذي تم إنشاؤه ، لذلك لا يوجد سوى بعض الخيارات التي يجب مراعاتها.

• --out-file المسار إلى ملف الإخراج GO ، مثل -o في GCC.
• --spec-file يحدد المسار إلى ملف الإدخال TLA+
• -يتيح --package-name Package تخصيص اسم حزمة ملف الإخراج GO. هذا الافتراضات إلى نسخة مرققة من اسم خوارزمية MPCAL.

pcalgen

تطلب اللجنة الفرعية pcalgen أن تقوم PGO بإعادة كتابة ملف إدخال TLA+ المحتوي على MPCAL ، بحيث يحتوي على ترجمة زائدة لخوارزمية MPCAL. الخيار الوحيد ، --spec-file ، هو المسار إلى ملف المواصفات ، والذي سيتم إعادة كتابته.

لإدخال ترجمة PlusCal ، سوف يبحث PGO عن تعليقات مثل أو إعطاء أو أخذ مساحة بيضاء:

 * BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION

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

كيف تعمل

PGO هو مصدر لمجمول البراميل المكتوب في سكالا. يقوم بتجميع المواصفات المكتوبة في امتداد PlusCal ، والتي تسمى Modular PlusCal (انظر صفحة PlusCal Modular لمزيد من التفاصيل) ، للذهاب إلى البرامج.

كيفية البناء (للتنمية)

يتم إنشاء رمز Scala من PGO عبر مشروع SBT ، مع تبعياته التي تديرها Maven. بالإضافة إلى ذلك ، توفر PGO مكتبة دعم وقت التشغيل لرمز GO الذي تم إنشاؤه ، والذي يعيش في distsys/ Subiled. رمز GO هذا هو وحدة GO قياسية ، والتي يمكن استيرادها عبر عنوان URL https://github.com/distcompiler/pgo/distsys.

البرنامج النصي الرئيسي للبناء هو build.sbt من المستوى الأعلى. للبناء من Terminal ، قم بتشغيل sbt في دليل الجذر واستخدم الأوامر القياسية التي توفرها وحدة التحكم SBT. وتشمل هذه run <command-line args> إلى (إعادة) تجميع وتشغيل PGO ، test تشغيل جميع الاختبارات ، بما في ذلك اختبارات GO (TODO: أضف Runner لاختبارات GO القائمة المجانية ؛ هذا واحد ، على وجه التحديد ، مفقود).

يمكن أيضًا أن يتم بناء بناء SBT تلقائيًا بواسطة المكون الإضافي لـ Intellij Scala ، وكذلك على الأرجح أي IDE مع دعم Scala.

تمكنت رمز Scala من PGO تبعية على مجموعة صغيرة من مكتبات المرافق:

• الأسقلوب لحالة سطر الأوامر تحليل الوسيطة
• المبتدئون في Scala-parser for tla+/pcal/mpcal parser
• OS-LIB للمعالجة المبسطة للملف والعملية (يتم استخدام معالجة العملية أثناء الاختبارات)

بالإضافة إلى ذلك ، تعتمد أجنحة اختبار PGO على:

• go قابلة للتنفيذ. ستحاول الاختبارات العثور على هذا ، ربما على $PATH أو ما يعادلها ، عبر عملية البحث الافتراضية لـ JVM.
• Scalatest كإطار اختبار
• Scalacheck لتنفيذ اختبارات الزغب
• java-diff-utils لتوليد الاختلافات عندما تقارن الاختبارات الكتل الكبيرة من النص

تعتمد مكتبة وقت تشغيل PGO على:

• غير قابل للتغيير للتطبيقات غير القابلة للتغيير للقوائم والخرائط في نموذج بيانات TLA+. على سبيل المثال ، يجب أن يستغرق إنشاء خريطة معدلة مع زوج مختلف قيمة المفاتيح وقتًا ثابتًا ، بدلاً من نسخ الهيكل الموجود بأكمله.
• multierr للجمع بين الأخطاء.

يتم اختبار PGO باستخدام OpenJDK من 1.11 إلى 1.16 ، وذهب 1.18. هناك حاجة إلى OpenJDK 1.11+ بسبب استخدام API القياسي. GO> = 1.18 مطلوب بسبب الأدوية الجيلية.