기술 요약: PaSTTeL

문제 정의

프로그램의 종료(termination) 또는 비종료(non-termination)를 증명하는 것은 컴퓨터 과학에서 근본적이면서도 결정 불가능한 문제이다. 실용적인 접근 방식은 명시적인 인자(argument)를 찾는 것이다. 종료 인자(예: 선형 랭킹 함수)는 종료를 의미하며, 비종료 인자(예: 선형 재귀 집합 또는 기하학적 비종료 인자)는 비종료를 의미한다. 이러한 분석은 주로 **라소 프로그램(lasso programs)**에 적용된다. 라소 프로그램은 직선형 코드(straight-line code) 뒤에 단일 while 루프가 이어지는 실행 궤적으로, CEGAR 기반의 종료 합성 과정에서 추출된 후보 무한 경로를 나타낸다.

특정 종료 또는 비종료 인자는 결정 가능하지만, 일반적인 문제는 여전히 도전적인 과제로 남아 있다. 기존의 최첨단 도구들은 종종 순차적인 전략을 사용하는 경면이 있으며, 다양한 분석 알고리즘을 통합하고, 이를 병렬로 실행하며, 외부 검증 도구의 모듈형 구성 요소로 기능할 수 있는 통합 프레임워크가 필요하다.

방법론: PaSTTeL 프레임워크

저자들은 C++17로 구현된 모듈식, 범용 및 병렬 포트폴리오 프레임워크인 PaSTTeL(Parallel analysiS framework for Termination and non-Termination of Lasso programs)을 제시한다. 이 아키텍처는 다양한 종료 및 비종료 접근 방식을 동시 실행 모델 내에서 통합하도록 설계되었다.

핵심 아키텍처

프레임워크는 모듈형 설계로 설명되는 세 가지 주요 구성 요소를 중심으로 구조화되어 있다:

1. SMT 엔진 (SMTSolverInterface): 교체 가능한 SMT 솔버를 허용하는 추상화 계층이다. 현재 구현은 Z3와 CVC5를 지원한다. 솔버 인스턴스는 제약 조건 기반 기법을 사용하는 순차적 분석기(sequential analyzers)로 전달된다.
2. 순차적 분석기 (AnalysisInterface): 개별 종료 또는 비종료 전략의 인터페이스를 정의하는 어댑터이다. 주요 메서드는 다음과 같다:
   • analyze(): 분석을 실행하고 결과(TERMINATING, NON_TERMINATING, 또는 UNKNOWN)를 반환한다.
   • getProof(): 평문(plain text) 형태의 증명 인증서를 반환한다.
3. 병렬화 계층 (PortfolioAnalyzer): 동일한 라소 프로그램 입력에 대해 등록된 여러 전략의 동시 실행을 관리한다. 이는 스레드 배치, 전략 등록 및 결과 집계를 처리한다.

인스턴스화 및 통합

PaSTTeL은 독립형 라이브러리로 설계되었다. 사용자가 init-PaSTTeL 함수(알고리즘 1)를 적응시켜 프레임워크를 인스턴스화할 수 있는데, 이 함수는 다음을 수행한다:

• 원하는 유형(Z3 또는 CVC5)에 따라 여러 SMT 솔버 인스턴스를 생성한다.
• 라소 프로그램과 스레드 수를 사용하여 PortfolioAnalyzer를 초기화한다.
• 특정 분석 기법(예: 종료 합성, 비종료 인자)을 포트폴리오에 등록한다.
• solve()를 통해 동시 탐색을 시작하고, 결론적인 결과가 나오거나 시간 제한(join())에 도달할 때까지 대기한다.

개념 증명: P-ULR

프레임워크의 범용성을 검증하기 위해, 저자들은 Ultimate LassoRanker (ULR)—SV-COMP 2025의 수상작이자 최첨단 도구—의 핵심 역량을 재현하도록 PaSTTeL을 인스턴스화하였다. P-ULR이라 명명된 이 구현은 다음을 포함한다:

• 입력 처리: SMT-LIB 표준을 따르며 단일 정적 할당(SSA)을 지원하는 JSON 기반 입력 형식이다. 필요한 경우 라소 프로그램을 선형화한다.
• 종료 전략: 선형 랭킹 템플릿을 사용하는 제약 조건 기반 합성, 구체적으로 아핀(affine) 및 중첩(nested) 템플릿을 사용한다.
• 비종료 전략: 고정점 체크(fixpoint checking) 및 **기하학적 비종료 인자(GNTA)**를 포함한 제약 조건 기반 합성을 포함한다.

참고 (제한 사항): 현재 P-ULR 구현에는 특정 제약이 있다: 비선형 사례(예: 복잡한 배열 연산)를 완전히 다루지 못하며, 대부분의 전략에서 선형 공식에 의존한다. 또한 현재 종료를 위해서는 QF_LRA를, GNTA를 위해서는 QF_LIA만을 지원한다.

실험 결과

프레임워크는 SV-COMP 2025, TermCOMP 2025, Ultimate 저장소에서 유래한 4,619개의 라소 프로그램을 대상으로 평가되었다. 실험은 16 Intel Core i5-14400T 프로세서와 30GB 메모리를 갖춘 머신에서 수행되었으며, 인스턴스당 600초의 타임아웃을 설정하였다.

성능 비교

연구에서는 세 가지 구성을 비교하였다:

1. ULR-Baseline: 전략을 순차적으로 실행하는 기존 ULR 도구.
2. P-ULR-Seq: 공정한 비교를 위해 동일한 전략을 순차적으로 실행하는 PaSTTeL.
3. P-ULR-Par4: 4개의 동시 스레드(Fixpoint, GNTA, Affine, Nested)로 실행되는 PaSTTeL.

주요 결과:

• 순차적 효율성: P-ULR-Seq는 ULR-Baseline보다 우수한 성능을 보였으며, 총 862초(약 14분)의 시간을 절감하였다. 특히, 비종료 합성을 위한 누적 시간이 47.13초에서 1.78초로 감소했다(26배 단축).
• 종료 분석: P-ULR-Seq는 랭킹 함수를 찾는 시간을 크게 단축했다. 그러나 ULR-Baseline은 P-ULR가 현재 결여하고 있는 내부 분할(partitioning) 단계 덕분에 가끔 더 단순한 랭킹 함수를 생성하기도 했다.
• 비종료 분석: P-ULk-Seq는 베이스라인과 비교하여 복잡한 비종료 증명(GNTA)을 처리하는 데 있어 명확한 우위를 입증했다.
• 병렬 실행: P-ULR-Par4는 ULR-Baseline에 비해 전체 실행 시간을 2.8배 감소시켰다. 그러나 P-ULR-Seq 대비 속도 향상은 미미했다. 저자들은 이를 벤치마크 구성 때문이라고 설명한다. 즉, **98%**의 라소 프로그램이 아핀 랭킹 함수를 수용하며, P-ULR-Seq는 이를 순차적 순서에 따라 즉시 해결하므로, 이 특정 데이터셋에서 성능을 개선할 병렬 전략의 여지가 거의 없었다.

의의 및 기여

본 논문은 PaSTTeL이 모듈식 및 범용 프레임워크가 성능을 저하시키지 않으면서 최첨단 종료 및 비종료 기법을 성공적으로 통합할 수 있음을 입증했다고 주장한다. 주요 기여는 다음과 같다:

1. 모듈성: 새로운 분석 알고리즘을 통합된 포트폴리오에 통합하기 용이한 설계.
2. 동시성: 등록된 전략을 동시에 실행하여 분석을 가속화하는 능력.
3. 재사용성: 외부 프로젝트가 내부 설계를 이해할 필요 없이 (비)종료 분석 기능을 임베딩할 수 있는 자가 포함된 C++ 라이브러리 구성 요소.
4. 경쟁력 있는 성능: 구현체(P-ULR)는 비종료 합성과 전체 실행 시간에서 상당한 속도 향상을 달와내며 기존 ULR 도구와 경쟁력 있게 성능을 발휘하여 프레임워크의 효율성을 검증하였다.

저자들은 현재 구현이 비선형 산술 및 특정 최적화 단계와 관련하여 제한 사항이 있지만, 프itek가 워크가 향후 재귀 집합 합성을 통합하고 비선형 산술(QF_NRA/QF_NIA)을 지원하는 등의 확장을 위한 견고한 토대를 제공한다고 결론짓는다.