런타임 예측 분석

런타임 예측 분석(또는 예측 분석)은 관찰된 실행에서 추론된 프로그램 실행에서 속성 위반을 탐지하기 위한 컴퓨터 과학의 런타임 검증 기술입니다.동시 프로그램에서 동시성 오류(예: 데이터 레이스)를 탐지하기 위해 중요한 클래스의 예측 분석 방법이 개발되었으며, 런타임 모니터는 관찰된 실행에서 발생하지 않았지만 동일한 프로그램의 대체 실행에서 발생할 수 있는 오류를 예측하는 데 사용됩니다.예측 기능은 관찰된 ^[1]실행에서 온라인으로 추출된 추상 모델에 대해 분석이 수행되므로 관찰된 실행 이상의 실행 클래스를 허용합니다.

개요

비공식적으로, $실행{\displaystyle }$ t${displaystyle$t$}$가 주어지면, 예측 분석은$t{displaystyle$ t$\}$의 $재정렬$된 추적${\displaystyle {}^{}}$t$`{$ t$`}$의 오류를 확인합니다.${\displaystyle {}^{}}$$t$${\displaystyle {\text{'}\{}^{}}$displaystyle $t}$를 $생성$할 수 있는 프로그램이 t$'{{$ t$\}$도 $생성$할 수 있는 경우 t${$$displaystyle$$$t}($$또는 t{$displaystyle$t$\}$의 올바른 순서^[2] 변경)에서 실행 가능하다고 합니다.

동시 프로그램의 맥락에서, 예측 기법은 관찰된 추적의 인과 모델의 실현 가능한 실행에서 동시성 오류만 예측하는 경우에 타당합니다.분석이 프로그램의 소스 코드에 대한 지식이 없다고 가정하면, 유추된 실행 클래스에 관찰된 추적의 프로그램 순서 및 통신 순서 접두사가 동일한 모든 실행이 포함된 경우 분석이 완료됩니다(최대라고도^[3][4] 함).

적용들

예측 분석은 다음과 같은 광범위한 동시성 오류를 감지하기 위해 적용되었습니다.

• 데이터 레이스
• 교착 상태^[5][6]
• 원자성 위반^[7]
• 주문 위반(예: 사용 후 무료^[8] 오류)

실행

동적 프로그램 분석의 일반적인 경우와 마찬가지로 예측 분석은 먼저 소스 프로그램을 계측합니다.런타임에 분석을 온라인으로 수행하여 오류를 즉시 탐지할 수 있습니다.또는 계측기는 오프라인 분석을 위해 실행 추적을 덤프하기만 하면 됩니다.후자의 접근 방식은 실행 추적에 대한 랜덤 액세스가 필요하거나 선형 시간 이상이 소요되는 값비싼 정제된 예측 분석에 선호됩니다.

데이터 및 제어 흐름 분석 통합

정적 분석은 먼저 데이터를 수집하고 소스 프로그램에 대한 흐름 의존성 정보를 제어하기 위해 수행될 수 있으며, 이는 온라인 실행 중에 인과 모델을 구성하는 데 도움이 될 수 있습니다.이를 통해 예측 분석을 통해 관찰된 실행을 기반으로 더 큰 클래스의 실행을 추론할 수 있습니다.직관적으로, 읽기가 액세스 실행 여부(제어 종속성)^[9][10]에 영향을 미치지 않는 경우, 실행 가능한 재정렬은 메모리 읽기(데이터 종속성)의 마지막 작성기를 변경할 수 있습니다.

접근법

부분 주문 기반 기술

부분 순서 기반 기술은 온라인 레이스 감지에 가장 많이 사용됩니다.런타임에 추적의 이벤트에 대한 부분 순서가 구성되고, 순서가 지정되지 않은 중요 이벤트 쌍이 레이스로 보고됩니다.인종 감지를 위한 많은 예측 기술은 발생 전 관계 또는 약화된 버전을 기반으로 합니다.이러한 기술은 일반적으로 벡터 클럭 알고리즘을 사용하여 효율적으로 구현될 수 있으며, 생성되는 전체 입력 트레이스 중 하나의 패스만 허용하므로 온라인 배포에 적합합니다.^{[2] [11] [12]}

SMT 기반 기술

SMT 인코딩을 사용하면 분석을 통해 실행 추적에서 (아마도 매우 큰) 수학 공식으로 정제된 인과 모델을 추출할 수 있습니다.또한 제어 흐름 정보를 모델에 통합할 수 있습니다.SMT 기반 기술은 건전성과 완전성(최대 인과^[4] 관계라고도 함)을 달성할 수 있지만 추적 크기와 관련하여 기하급수적인 시간 복잡성을 가집니다.실제로 분석은 일반적으로 실행 추적의 경계 세그먼트에 배포되므로 확장성을 위해 완전성을 거래합니다.^{[9] [13] [14] [15]}

Lockset 기반 접근 방식

잠금 기반 동기화를 사용하는 프로그램에 대한 데이터 레이스 탐지의 맥락에서, 잠금 세트^[16] 기반 기술은 데이터 레이스를 탐지하기 위한 견고하지 않지만 가벼운 메커니즘을 제공합니다.이러한 기술은 주로 잠금 세트 원칙의 위반을 탐지합니다.즉, 주어진 메모리 위치의 모든 액세스는 공통 잠금으로 보호되어야 합니다.이러한 기술은 더 비싼 ^[4]분석에서 후보 경선 보고서를 걸러내는 데도 사용됩니다.

그래프 기반 기술

데이터 레이스 감지의 맥락에서, 건전한 다항 시간 예측 분석은 그래프를 기반으로 한 최대 예측 능력에 가까운 양호한 상태로 개발되었습니다.^[17]

계산 복잡성

k${displaystyle$ k$}$ 스레드에$$ $의해{\displaystyle }$ 실행된 n${displaystyle$ n$}$ 크기의${\displaystyle }$ 입력 추적이 주어지면 일반적인 레이스 예측은 NP-완전이고 k${displaystyle$k$\}$에 $의해{\displaystyle }$ W[1]-하드 매개 변수화되지만 통신 토폴로지가 ^[18]비순환일 때 다항 시간 알고리듬을 허용합니다.O$){displaystyle$ O$(n\cdotk)}$ 시간$$ $내$에 레이스가 감지되기 전에 발생하며, 이 경계가 ^[19]최적입니다.d${displaystyled}$ 변수에$$ $대한{\displaystyle }$ 잠금 세트 레이스는 O${\displaystyle (n}$ ${\displaystyle \cdot }$ d$)$ {{$displaystyle O(n\cdot$ d$)}$ 시간$$ $내$에 감지되며, 이 경계도 ^[19]최적입니다.

도구들

다음은 예측 분석을 사용하여 동시성 오류를 탐지하는 도구의 일부 목록입니다. 이 도구는 알파벳 순으로 정렬되어 있습니다.

• "Rapid".동적 경주 감지 엔진을 구현하기 위한 경량 프레임워크
• 동시 Java 프로그램에 대한 동적 분석을 통해 신속한 프로토타이핑 및 실험을 용이하게 하도록 설계된 동적 분석 "RoadRunner".프레임워크입니다.
• "RV-Predict".SMT 기반 예측 레이스 탐지.
• "UFO".시만텍 기반의 예측 사후 사용 탐지 기능.

참고 항목

• 모델 확인
• 동적 프로그램 분석
• 런타임 검증

레퍼런스