Deadlock_Racer

이중 자물쇠

교착 상태는 FRAMA-C 플랫폼의 플러그인으로 구현 된 C 프로그램의 잠재적 교착 상태를 감지하기위한 정적 분석기입니다.

핵심 알고리즘은 기존 도구 Racerx를 기반으로합니다. 소위 잠금 세트 분석은 제어 흐름 그래프를 가로 지르고 모든 프로그램 지점에서 고정 된 잠금 세트를 계산합니다. 잠금 B가 이미 잠금 a를 포함하는 현재 잠금장으로 획득하면 종속성 a -> b가 lockgraph에 추가됩니다. 이 그래프의 각주기는 잠재적 교착 상태로보고됩니다.

플러그인은 EVA (Frama-C의 값 분석 플러그인)를 사용하여 잠금 작업의 매개 변수에 대한 May-Point-to 정보를 계산합니다. EVA는 기본적으로 동시 프로그램을 분석 할 수 없기 때문에 먼저 프로그램의 모든 스레드를 식별 한 다음 스레드가 생성 된 프로그램 포인트의 컨텍스트와 별도로 각 스레드에 대해이를 실행합니다. 결과는 실증적 인 발사로, 이는 실의 인터리빙을 고려하지 않습니다.

예

이 예제는 간단한 교착 상태로 프로그램의 출력을 보여줍니다. 더 복잡한 예는 여기에서 찾을 수 있습니다.

 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 run -it tdacik/deadlock 사용하거나 make docker 에서 교착 상태를 실행할 수도 있습니다.

용법

플러그인을 실행하는 가장 간단한 방법은 다음과 같습니다.

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

보다 고급 사용량은 Frama-C의 GUI 응용 프로그램에서 결과를 시각화하기위한 분석 조정 및 GUI 설명서를위한 명령 줄 옵션 목록을 참조하십시오.

관련 서류

Excel@fit'20의 절차 에서 Frama-C의 Dacík T. 정적 교착 상태 감지. BRNO 기술 대학교, 정보 기술부. 2020

Frama-C 환경의 Dacík T. 정적 분석은 교착 상태 탐지 학사 논문에 중점을 두었습니다. BRNO 기술 대학교, 정보 기술부. 2020-07-10. Vojnar Tomáš의 감독.

연락하다

질문이 있으시면 주저하지 말고 도구/방법 저자에게 문의하십시오.

• Tomáš dacík <[email protected]>
• Tomáš vojnar <[email protected]>

특허

플러그인은 MIT 라이센스에서 사용할 수 있습니다.