Deadlock_Racer ดาวน์โหลด - Deadlock_Racer SORCIDE ดาวน์โหลด

Deadlock_Racer

หมวดหมู่อื่นๆ

v1.0.1

ดาวน์โหลด

การหยุดชะงัก

Deadlock เป็นเครื่องวิเคราะห์แบบคงที่สำหรับการตรวจจับการหยุดชะงักที่อาจเกิดขึ้นในโปรแกรม C ที่ใช้เป็นปลั๊กอินของแพลตฟอร์ม Frama-C

อัลกอริทึมหลักขึ้นอยู่กับเครื่องมือ Racerx ที่มีอยู่ การวิเคราะห์ล็อคเซ็ตที่เรียกว่ากราฟการควบคุมการไหลของการควบคุมและคำนวณชุดของล็อคที่จัดขึ้นที่จุดโปรแกรมใด ๆ เมื่อล็อค B ได้มาพร้อมกับล็อคปัจจุบันที่มีการล็อค A แล้วการพึ่งพา A -> B จะถูกเพิ่มลงใน LockGraph แต่ละรอบในกราฟนี้จะถูกรายงานว่าเป็นการหยุดชะงักที่อาจเกิดขึ้น

ปลั๊กอินใช้ EVA (ปลั๊กอินการวิเคราะห์ค่าของ FRAMA-C) เพื่อคำนวณข้อมูลพฤษภาคมถึงจุดเป็นพารามิเตอร์ของการล็อค เนื่องจาก EVA ไม่สามารถวิเคราะห์โปรแกรมที่เกิดขึ้นพร้อมกันได้เราจึงระบุเธรดทั้งหมดในโปรแกรมก่อนแล้วจึงเรียกใช้สำหรับแต่ละเธรดแยกต่างหากด้วยบริบทของจุดโปรแกรมโดยที่เธรดถูกสร้างขึ้น ผลที่ได้คือการเปลี่ยนแปลงที่ต่ำกว่าซึ่งไม่ได้คำนึงถึง interleavings ของเธรด

ตัวอย่าง

ตัวอย่างนี้แสดงผลลัพธ์สำหรับโปรแกรมด้วยการหยุดชะงักอย่างง่าย ตัวอย่างที่ซับซ้อนมากขึ้นสามารถพบได้ที่นี่

 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 แล้ว การหยุดชะงัก ต้องมีการติดตั้งแพ็คเกจ OPAM ต่อไปนี้:

 ounit2
containers

หลังจากติดตั้งการพึ่งพาและการโคลนนิ่งซ่อมแซมนี้ การหยุดชะงัก สามารถติดตั้งได้ดังนี้:

 cd Deadlock
make setup
make
make install

นอกจากนี้คุณยังสามารถเรียกใช้การหยุดชะงักใน Docker ได้โดยใช้ docker run -it tdacik/deadlock หรือโดยการเรียกใช้ make docker เพื่อสร้างภาพของเวอร์ชันล่าสุด

การใช้งาน

วิธีที่ง่ายที่สุดในการเรียกใช้ปลั๊กอินคือ:

 frama-c -deadlock source_file1.c source_file2.c ...

สำหรับการใช้งานขั้นสูงเพิ่มเติมโปรดดูรายการตัวเลือกบรรทัดคำสั่งสำหรับการปรับแต่งการวิเคราะห์และคู่มือ GUI สำหรับการสร้างภาพผลลัพธ์ในแอปพลิเคชัน GUI ของ Frama-C

เอกสารที่เกี่ยวข้อง

Dacík T. การตรวจจับการหยุดชะงักแบบคงที่ใน frama-c ใน การดำเนินการของ excel@fit'20 มหาวิทยาลัยเทคโนโลยี BRNO คณะเทคโนโลยีสารสนเทศ 2020

Dacík T. การวิเคราะห์แบบคงที่ในสภาพแวดล้อมของ FRAMA-C มุ่งเน้นไปที่การตรวจจับการหยุดชะงักของวิทยานิพนธ์ปริญญาตรี มหาวิทยาลัยเทคโนโลยี BRNO คณะเทคโนโลยีสารสนเทศ 2020-07-10 ดูแลโดย Vojnar Tomáš