TLA+가 검증할 수 없는 것들
What TLA+ can and can't check
TLA+는 동시성 시스템 설계와 검증에 강력하지만, 모든 속성을 표현할 수 있는 것은 아니다. 불변식, 액션 속성, 라이브니스 등은 잘 다루지만, 도달 가능성(reachability)이나 하이퍼프로퍼티(hyperproperty)처럼 여러 실행 경로나 실행 집합에 걸친 속성은 TLA+로 직접 표현할 수 없다. 보조 변수나 자기 합성 같은 우회 기법이 있으나 모델을 복잡하게 만들고 한계가 있다. TLA+의 실제 적용 가능 범위를 이해하는 것이 중요하다.
우리가 관심 있는 많은 중요한 속성들이 이 범주에 속한다. 새를 인간이 인식하는 개념을 형식화할 수 없다면, 앱이 새를 인식한다는 것을 증명할 수 없다.
HN 토론
31- sourdecor
HN에서 이 댓글[1]을 보고 Quint[0]를 알게 됐다. Quint는 "JavaScript에서 동작하는 실행 가능한 명세 언어로, TLA(temporal logic of actions)에 기반한 멋진 툴링을 갖춘" 언어다. 정말 훌륭하다고 생각하며, TLA+에 관심 있는 사람이라면 누구나 한번 살펴보길 권한다.
- singron
이 글 정말 좋다. TLA+를 어딘가에 활용하려는 사람이라면 읽어보면 아주 유익할 것이다.
조금 다른 이야기지만, TLA+가 잘 못하는 또 다른 영역은 atomics, 특히 weak-memory semantics나 sequentially consistent하지 않은 것들을 모델링하는 것이다. 알고리즘을 pcal로 옮기면 마치 sequentially consistent한 것처럼 실행된다. non-sequential-consistency를 모델링해야 한다면 TLA+에 명시적인 로직으로 일일이 풀어 써야 하는데, 손으로 하기에는 아마 너무 복잡하고 실수하기 쉬울 것이다. C/C++/Rust 메모리 모델은 정말 별의별 기상천외한 것들을 허용한다. 각 변수마다 read cache와 writeback buffer를 추가하고 적절한 지점에 cache-flushing 명령을 넣어야 할 것 같은데, 어쩌면 더 우아한 방법이 있을지도 모르겠다.
Rust를 쓴다면 miri와 loom 둘 다 일부 non-sequentially-consistent 동작을 검사할 수 있는 분석기를 갖고 있다(그리고 loom은 실제로 sequential-consistency를 전혀 구현하지 않는다).
- adamddev1
좋은 글이다. 사람들은 계속 "그냥 테스트를 작성하면 된다"거나 최근에는 "형식 검증을 쓰면 된다"고 말하면서, 이것들이면 충분한 안전장치니까 구현은 전부 LLM에 맡겨도 된다고 생각한다. 하지만 사실 확률적으로 추측하는 기계가 그들을 구해주지는 못한다. 사람들은 자기가 만드는 것을 실제로 이해해야 한다는 필요성에서 도망칠 수 없다.
- rrook
내 생각에 이 문제의 일부는 우리 프로그래밍 언어의 한계다. 일반적으로 언어들은 부분 그래프(partial graph)를 표현할 수 있게 해주는데, 이 때문에 검증 문제가 기술적으로 까다로워진다. 내 견해로는 폐쇄 그래프(closed-graph) 의미론만 노출하는 언어라면, 완전하지는 않더라도 모델과 구현 사이의 간극을 좁히는 데 도움이 될 수 있다.
- metabagel
인라인 각주 정말 좋다!