패턴 정규 언어를 위한 예측 모니터링

현재 동시 소프트웨어를 위한 버그 탐지 기술은 데이터 레이스나 교착 상태와 같은 저수준 문제를 찾아내는 데 집중하고 있지만, 이러한 저수준 문제가 없을 때에도 발생할 수 있는 더 복잡한 시간적 행동을 발견하는 데는 종종 실패합니다. 본 논문에서는 LTL과 같은 고수준 시간적 사양에 대해 동적으로 동시 소프트웨어를 분석하는 문제에 주목합니다. 이러한 사양에 대한 런타임 모니터링을 위한 기존 기술은 주로 순차 소프트웨어를 위해 설계되었으며 동시성의 존재에서는 부족합니다. 위반은 복잡한 스레드 인터리빙에서만 관찰될 수 있으며, 분석과 함께 기본 소프트웨어를 여러 번 재실행해야 합니다. 이를 위해 최근 널리 연구된 예측 데이터 레이스 탐지의 유사한 문제에서 영감을 받아 예측 런타임 모니터링 문제를 연구합니다. 예측 런타임 모니터링 문제는 실행 σ 가 사양의 위반을 노출하기 위해 안전하게 재배치할 수 있는지를 묻습니다. 일반적으로 이 문제는 사양이나 사용하는 재배치 개념이 복잡할 때 쉽게 다룰 수 없게 됩니다. 본 논문에서는 정규 언어로 주어진 사양에 주목합니다. 우리의 재배치 개념은 추적 동등성으로, 실행은 인접한 독립적 행동을 반복적으로 교환하여 후자의 행동으로부터 얻을 수 있는 경우 다른 행동의 재배치로 간주됩니다. 우리는 첫째, 이 단순한 설정에서도 예측 모니터링 문제는 O(n^α)라는 초선형 하한을 인정함을 보여줍니다. 여기서 n은 실행에서 사건의 수이며, α는 교환성의 정도를 설명하는 매개변수로 일반적으로 실행에서 스레드의 수에 해당합니다. 그 결과, 이 설정에서조차 예측 런타임 모니터링은 효율적으로 해결될 가능성이 낮습니다. 비예측적 설정에서는 결정론적 유한 오토마타를 사용하여 문제를 확인할 수 있습니다(따라서 상수 공간 스트리밍 선형 시간 알고리즘이 가능합니다). 이를 위해 우리는 패턴 언어라고 불리는 정규 언어의 하위 클래스를 식별합니다(그리고 그 확장을 일반화된 패턴 언어라고 합니다). 패턴 언어는 특정 수의(라벨이 붙은) 사건의 특정 순서를 자연스럽게 표현할 수 있으며, '작은 버그 깊이' 가설과 같은 많은 동시성 버그 탐지 접근 방식의 기초가 되는 인기 있는 경험적 가설에서 영감을 받았습니다. 더 중요한 것은, 패턴(및 일반화된 패턴) 언어에 대해 예측 모니터링 문제를 상수 공간 스트리밍 선형 시간 알고리즘을 사용하여 해결할 수 있음을 보여줍니다. 우리는 문헌의 벤치마크에서 우리의 알고리즘인 PatternTrack을 구현하고 평가하며 대규모 응용 프로그램을 모니터링하는 데 효과적임을 보여줍니다.