Deadlock_Racer
v1.0.1
يعد Deadlock محللًا ثابتًا للكشف عن مصلتملة على البرامج المحتملة التي تم تنفيذها كمكون إضافي لمنصة Frama-C.
تعتمد الخوارزمية الأساسية على Racerx للأدوات الموجودة. يعبر تحليل القفل المزعوم الرسم البياني لتدفق التحكم ويحسب مجموعة الأقفال المحتفظ بها في أي نقطة برنامج. عند الحصول على القفل B باستخدام Lockset الحالي الذي يحتوي بالفعل على القفل A ، تتم إضافة التبعية A -> B إلى Lockgraph. ثم يتم الإبلاغ عن كل دورة في هذا الرسم البياني باعتبارها مدويًا محتملاً.
يستخدم البرنامج المساعد EVA (البرنامج المساعد لتحليل القيمة من FRAMA-C) لحساب معلومات مايو إلى المعلمات من عمليات القفل. نظرًا لأن EVA لا يمكنه تحليل البرامج المتزامنة أصليًا ، فإننا نتعرف أولاً على جميع مؤشرات الترابط في برنامج ما ، ثم نديرها لكل مؤشر ترابط بشكل منفصل مع سياقات نقاط البرنامج ، حيث تم إنشاء مؤشر الترابط. والنتيجة هي بعد ذلك التقليل من الجبهة ، والتي لا تأخذ في الاعتبار بين المتداولات.
يوضح هذا المثال الإخراج للبرنامج مع adadlock البسيطة. يمكن العثور على مثال أكثر تعقيدًا هنا.
void * thread1 ( void * v )
{
pthread_mutex_lock ( & lock1 );
pthread_mutex_lock ( & lock2 );
...
pthread_mutex_unlock ( & lock2 );
pthread_mutex_unlock ( & lock1 );
}
void * thread2 ( void * v )
{
pthread_mutex_lock ( & lock2 );
pthread_mutex_lock ( & lock1 );
...
pthread_mutex_unlock ( & lock1 );
pthread_mutex_unlock ( & lock2 );
} [kernel] Parsing simple_deadlock.c (with preprocessing)
[Deadlock] Deadlock analysis started
[Deadlock] === Assumed threads: ===
[Deadlock] main
[Deadlock] thread1
[Deadlock] thread2
[Deadlock] === Lockgraph: ===
[Deadlock] lock1 -> lock2
[Deadlock] lock2 -> lock1
[Deadlock] ==== Results: ====
[Deadlock] Deadlock between threads thread1 and thread2:
Trace of dependency (lock2 -> lock1):
In thread thread2:
Lock of lock2 (simple_deadlock.c:20)
Lock of lock1 (simple_deadlock.c:21)
Trace of dependency (lock1 -> lock2):
In thread thread1:
Lock of lock1 (simple_deadlock.c:10)
Lock of lock2 (simple_deadlock.c:11)
الإصدار الحالي متوافق مع Frama-C Vanadium ، يمكن العثور على دليل التثبيت المفصل في دليل المستخدم ويتطلب إصدار OCAML على الأقل 4.12. إلى جانب Frama-C ، يتطلب Deadlock متابعة حزم Opam لتثبيت:
ounit2
containers
بعد تثبيت التبعيات واستنساخ هذه إعادة التثبيت ، يمكن تثبيت Deadlock على النحو التالي:
cd Deadlock
make setup
make
make install
يمكنك أيضًا تشغيل Deadlock في Docker إما باستخدام docker run -it tdacik/deadlock أو عن طريق تشغيل make docker لإنشاء صورة لأحدث إصدار.
أبسط طريقة لتشغيل البرنامج المساعد هي:
frama-c -deadlock source_file1.c source_file2.c ...
للحصول على مزيد من الاستخدام المتقدم ، راجع قائمة خيارات سطر الأوامر لضبط التحليل ودليل واجهة المستخدم الرسومية لتصور النتائج في تطبيق واجهة المستخدم الرسومية لـ FRAMA-C.
Dacík T. اكتشاف قاتم ثابت في Frama-C في وقائع excel@fit'20 . جامعة برنو للتكنولوجيا ، كلية تكنولوجيا المعلومات. 2020
ركز التحليل الثابت في Dacík T. في بيئة Frama-C على أطروحة البكالوريوس في الكشف عن طريق المسدود. جامعة برنو للتكنولوجيا ، كلية تكنولوجيا المعلومات. 2020-07-10. تحت إشراف Vojnar Tomáš.
إذا كان لديك أي أسئلة ، فلا تتردد في الاتصال بأداة/مؤلفي الأداة:
المكون الإضافي متاح بموجب ترخيص معهد ماساتشوستس للتكنولوجيا.
