dingo hunter

دنغو هنتر

محلل ثابت للعثور على طريق مسدود

هذا محلل ثابت لنمذجة التزامن وإيجاد مسدود في رمز GO. الغرض الرئيسي من هذه الأداة هو الاستنتاج من رمز Go Source Model الخاص به في أي من التنسيقين:

• توصيل آلات الدولة المحدودة (CFSMS)
• أنواع ميجو

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

ثَبَّتَ

يمكن تثبيت dingo-hunter عن طريق go get ، Go Person go1.7.1 مطلوب.

 $ go get -u github.com/nickng/dingo-hunter

الاستخدام

هناك طريقتان (أنواع CFSMS وأنواع Migo) استنادًا إلى عملين بحثين.

نهج CFSMS

يولد هذا النهج CFSMs كنماذج لجوروتين التي تولد في البرنامج ، ثم يتم تمرير CFSMS إلى أداة التوليف لبناء رقص عالمي والتحقق من الصلاحية (انظر الورق).

قم أولاً بتثبيت Synthesis Tool gmc-synthesis عن طريق التحقق من الجهاز الفرعي:

 $ cd $GOPATH/src/github.com/nickng/dingo-hunter; git submodule init; git submodule update
$ cd third_party/gmc-synthesis

اتبع README لتثبيت وإنشاء gmc-synthesis ، أي

 $ cabal install MissingH split Graphalyze
$ ./getpetrify # and install to /usr/local/ or in $PATH
$ ghc -threaded GMC.hs --make && ghc --make BuildGlobal

لتشغيل توليد CFSMS على example/local-deadlock/main.go :

 $ dingo-hunter cfsms --prefix deadlock example/local-deadlock/main.go

يجب أن يقول الإخراج قناتين ، ثم قم بتشغيل أداة التوليف على CFSMS المستخرجة

 $ cd third_party/gmc-synthesis
$ ./runsmc inputs/deadlock_cfsms 2 # where 2 is the number of channels

يشير خط SMC check إلى ما إذا كان الرسم البياني العالمي يفي SMC (أي آمن) أم لا.

القيود

• تدعم أدائنا حاليًا الاتصالات المتزامنة (القناة غير المقلدة) فقط
• لا ينبغي أن يعتمد goroutines بعد أي عمليات اتصال على تلك التواصل. نموذجنا يفترض أن goroutines تولد مستقلة.

نهج أنواع ميجو

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

يتوفر المدقق لأنواع Migo في Netkng/Gong ، اتبع الإرشادات اللازمة لإنشاء الأداة:

 $ git clone ssh://github.com/nickng/gong.git
$ cd gong; ghc Gong.hs

لتشغيل جيل أنواع migo على example/local-deadlock/main.go :

 $ dingo-hunter migo example/local-deadlock/main.go --no-logging --output deadlock.migo
$ /path/to/Gong -A deadlock.migo

القيود

• القنوات حيث أن قيم الإرجاع غير مدعومة الآن
• قناة RECV ، اختبار موافق لا يمكن تمثيله في MIGO (يتطلب فحص قيمة ولكنه مستخلصها بواسطة الأنواع)

المنشورات البحثية

• اكتشاف قاتل ثابت لتوليف Global Session Graph Synthesis ، Nicholas NG و Nobuko Yoshida ، Int'l Conference on Compiler Construction (CC 2016) ، ACM
• المبارزة GO: LEVING و SANIDY للبرمجة القائمة على القناة ، جوليان لانج ، نيكولاس نغ ، برناردو تونينهو ونوبوكو يوشيدا ، ندوة ACM SIGPLAN على مبادئ لغات البرمجة (POPL 2017) ، ACM

ملحوظات

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

رخصة

يتم ترخيص Dingo-Hunter بموجب ترخيص Apache