n-version 시스템을 구축했다. 동일한 중요 함수를 독립적으로 구현한 세 가지 구현체, 다수결 결과를 선택하는 voter, 그리고 단일 장애점을 뛰어넘었다는 따뜻한 만족감까지.

하지만 함수들이 동등하다는 것을 증명한 게 아니다. 컴파일된다는 것만 증명했을 뿐이다.

동등성이 n-version programming의 숨은 기초인 이유

N-version programming은 하나의 구현체에 버그가 있더라도 나머지에는 없을 가능성이 높으므로 voter가 이상치를 버릴 수 있다는 아이디어다. 이는 출력이 비교 가능하다고 가정한다.

함수 A는 float을 반환하고 함수 B는 string을 반환하면 voter는 판단할 근거가 없다. 하지만 타입이 일치하더라도 의미적 차이가 치명적이다. 하나는 오름차순 정렬, 다른 하나는 내림차순 정렬. 하나는 half up 반올림, 다른 하나는 half to even 반올림. voter는 세 가지 다른 답을 보고 원칙에 따라 선택할 방법이 없다.

N-version programming 관련 문헌에는 독립적으로 작성된 프로그램이 상관관계를 가지고 함께 실패하는 경우가 많다는 연구가 가득하다. 프로그래머들은 같은 실수를 한다. 같은 모호한 명세를 오독한다. 명세가 “이 리스트를 정렬하라”이고 한 프로그래머가 quicksort를, 다른 프로그래머가 mergesort를 구현했다고 가정하자. 동등할 것이라고 생각할 수 있다. stability를 따지기 전까지는 맞다. 입력에 NaN이 포함되기 전까지는.

대부분의 팀은 동등성 검사가 추가 작업처럼 느껴진다는 이유로 생략한다. 그렇지 않다. 동등성 검사는 나머지 시스템에 의미를 부여하는 작업이다.

테스트 스위트가 거짓된 자신감을 주는 이유

unit test를 작성한다. 두 함수 모두 통과한다. 승리를 선언한다.

이는 카테고리 오류다. 테스트는 버그의 존재를 증명할 수는 있어도 부재를 증명할 수는 없다. 무한한 입력 공간, 혹은 그냥 큰 유한 공간에서 테스트 커버리지는 반올림 오차에 불과하다. 두 함수는 당신이 생각한 모든 경우에 동의하고, 새벽 3시 프로덕션에서 치명적인 그 한 경우에 달라질 수 있다.

두 개의 JSON parser를 다룬 프로젝트에서 이것을 힘들게 배웠다. 하나는 Python 내장 json.loads를 사용했고, 다른 하나는 성능을 위해 직접 만든 parser를 사용했다. 테스트 스위트에는 50개의 케이스가 있었다. 둘 다 통과했다. 프로덕션에서 한 고객이 중복 키를 가진 JSON 객체를 보냈다. Python의 parser는 마지막 값을 유지했다. 우리의 직접 만든 parser는 첫 번째 값을 유지했다. voter는 두 개의 다른 객체를 보고 panic 상태에 빠졌다.

Property-based testing은 한 걸음 더 다가간다. 입력을 수동으로 고르는 대신, 두 함수가 만족해야 하는 property를 기술하고 generator가 counterexample을 찾도록 한다. Python의 Hypothesis 라이브러리를 사용한 실제 예시다:

from hypothesis import given, strategies as st
import math

def round_half_up(n):
    return math.floor(n + 0.5)

@given(st.floats(allow_nan=False, allow_infinity=False))
def test_rounding_equivalence(n):
    assert round_half_up(n) == round(n)

if __name__ == "__main__":
    test_rounding_equivalence()

이것을 실행하면 Hypothesis는 빠르게 counterexample을 찾아낼 것이다. round_half_up(2.5)는 3을 반환한다. Python 내장 round(2.5)는 2를 반환하는데, 이는 banker’s rounding을 사용하여 가장 가까운 짝수로 반올림하기 때문이다. 어떤 기준으로 보면 두 함수 모두 “올바르다”. 하지만 동등하지는 않다.

Property-based testing은 동등성을 증명하지는 못한다. unit test가 놓친 edge case를 찾아줄 뿐이다. 이는 가치 있지만, 여전히 반증(falsification)일 뿐 검증(verification)은 아니다.

SMT solver가 어떻게 실제로 동등성을 증명할 수 있는가

증명을 원한다면 테스트의 안전지대를 떠나 SMT solver의 영역으로 들어가야 한다. 아이디어는 간단하다. 두 함수를 논리식으로 인코딩하고 solver에 어떤 입력에서든 다른 결과가 나오는지 묻는 것이다.

Bounded domain에 대해서는 이것이 기계적으로 가능하다. Z3를 사용하여 두 정수 max 구현이 동등함을 증명하는 예시다:

from z3 import Int, Solver, If, Abs

x = Int('x')
y = Int('y')

# Standard max implementation
max_standard = If(x > y, x, y)

# Algebraic max: (x + y + abs(x - y)) / 2
max_algebraic = (x + y + Abs(x - y)) / 2

solver = Solver()
solver.add(max_standard != max_algebraic)
result = solver.check()
print(result)  # unsat

Z3는 unsat을 반환하는데, 이는 counterexample이 존재하지 않음을 의미한다. 이 함수들은 Z3 모델의 모든 정수에 대해 동등하다. 이는 Z3가 추론하는 이론 내에서 bounded된 실제 증명이다.

더 복잡한 함수에도 이것을 적용할 수 있다. 핵심은 함수를 논리식으로 표현하는 것이다. loop는 unroll하고, array는 Z3의 array theory를, floating point는 Z3의 FP theory를 사용하며 복잡한 표현식에서 solver가 timeout될 수 있음을 받아들여야 한다.

“기계적”과 “쉬운” 사이의 간극이 대부분의 팀이 막히는 지점이다. Python 함수를 Z3 언어로 번역하려면 둘 다 이해해야 한다. 하지만 번역이 완료되면 solver가 어려운 작업을 대신한다.

아무도 공개하고 싶어 하지 않는 trade-off 표

모든 가능한 입력과 모든 IEEE 754 edge case에 대한 동등성을 증명하는 완전한 formal verification은 가능하다. 사람들은 암호학적 기본 요소와 항공 전자 시스템을 위해 이를 수행한다. 이는 전문가의 수 주 또는 수 개월의 시간이 들며 Coq나 Isabelle 같은 도구가 필요하다.

Property-based testing은 몇 분이면 되고 실제 버그를 잡지만 어떤 보장도 제공하지 않는다.

SMT solver를 사용한 bounded verification은 그 중간에 위치한다. 잘 정의된 범위에 대해 보장을 제공한다. 그 범위는 프로덕션 입력의 99.9%를 커버할 수 있다. 이것이 충분한지는 실패의 비용에 따라 달라진다.

공짜 점심은 없다. 위험 허용 범위와 팀의 전문성에 맞는 도구를 선택하라.

언제 포기해야 할지 아는 voter

대부분의 n-version 시스템은 단순한 다수결 voter를 구현한다: 가장 흔한 결과를 반환하거나, 다수결을 이루지 못하면 실패한다. 더 나은 voter는 자신의 무지를 안다.

from collections import Counter

def naive_voter(results):
    if not results:
        raise ValueError("No results to vote on")
    counts = Counter(results)
    winner, count = counts.most_common(1)[0]
    if count > len(results) / 2:
        return winner
    raise ValueError("No majority found")

def informed_voter(results, input_sample=None):
    if not results:
        raise ValueError("No results to vote on")

    distinct = set(results)
    if len(distinct) == 1:
        return results[0]

    # Log disagreement for later analysis
    if input_sample is not None:
        print(f"Disagreement on input {input_sample}: {distinct}")

    counts = Counter(results)
    winner, count = counts.most_common(1)[0]
    if count > len(results) / 2:
        return winner

    raise ValueError("No majority found")

voter가 특정 입력 클래스에서 지속적인 불일치를 발견하면, 이것은 신호다. 동등성 가정이 틀렸거나, 혹은 한 구현체에서 버그를 찾은 것이다. 둘 다 알 가치가 있다.

voter는 단순히 승자를 고르기 위해 있는 것이 아니다. 동등성에 대한 가정이 틀렸을 때 당신에게 알려주기 위해 있는 것이다.

실제로 다음에 해야 할 일

Property-based testing부터 시작하라. 비용이 적게 들고 버그를 찾아주며, 당신의 도메인에서 “동등성”이 무엇을 의미하는지 명확히 하도록 강요한다. bitwise 동일한 출력인가? 어떤 epsilon 범위 내의 출력인가? 동일한 postcondition을 만족하는 출력인가?

동등성을 정확히 정의한 후, 도메인이 유한하고 stakes가 높다면 bounded verification으로 넘어가라. Z3, CBMC, 또는 유사한 도구를 사용하여 bounded 범위에 대한 기계적 증명을 얻어라.

완전한 formal verification은 버그가 말 그대로 사람을 죽이는 부분에만 남겨두라. 나머지 모든 것에 대해서는 증명의 한계를 인식하고 프로덕션에서 불일치를 모니터링하라. 가장 좋은 n-version 시스템은 자신이 모르는 것을 아는 시스템이다.