Cleanroom software engineering 은 1,000줄당 0.1개의 defect 를 달성한다. 업계 평균은 10에서 50이다. 문제는 완전한 Cleanroom 을 위해서는 팀을 author 와 verifier 로 분할하고, 모든 module 앞에 formal specification 을 작성하며, 별도의 test team 이 통계적으로 validate 할 때까지 developer 가 자신의 code 를 실행하는 것을 금지해야 한다는 점이다.

대부분의 engineering manager 는 그 process 를 보고 headcount 로 빠르게 계산한 뒤, quality 가 overhead 만큼의 가치가 없다고 판단한다. 반은 맞다. 완전한 Cleanroom process 는 무겁다. 하지만 underlying principles 는 lightweight 하며, verification army 를 고용하거나 cargo test 를 금지하지 않아도 도입할 수 있다.

Cleanroom 이 실제로 무엇인가

Cleanroom 은 1970년대 IBM 의 Harlan Mills 가 개발한 software development process 다. 이름은 반도체 제조에서 유래했다: defect 를 만들어내는 조건을 사전에 차단하고, 사후에 inspect 해서 제거하지 않는다는 뜻이다. core claim 은 code 를 작성하기 전에 bug 가 불가능하도록 충분히 신중하게 설계하면 software 는 construction 에 의해 correct 할 수 있다는 것이다.

method 는 세 가지 practice 에 기반한다: statistical process control 하의 incremental development, box structures 를 이용한 function-theoretic design, 별도의 팀이 수행하는 statistical usage testing. 이 세 가지는 서로 의존적이다. 하나를 깨면 나머지도 힘을 잃는다.

바로 그 interdependency 가 overhead myth 의 원인이다. 팀은 셋 다 도입하거나 아예 안 하거나라고 가정한다. 사실이 아니다. practice 는 서로 보완하지만 각각 단독으로도 value 를 생성한다.

overhead 가 실제로 존재하는 곳

사람들이 두려워하는 80%의 overhead 는 두 가지 구체적인 요구사항에서 비롯된다.

첫째, no-execution rule 이다. 완전한 Cleanroom 에서는 code 를 작성한 developer 가 compile, 실행, unit test 를 하지 않는다. 별도의 verification team 이 모든 실행을 담당한다. 이는 developer 가 타이핑하기 전에 모든 case 를 추론하게 만들고, 그것이 code 가 첫 번째 시도에 동작하는 이유다. 하지만 engineering headcount 를 두 배로 늘리거나 기존 팀을 서로 원망하는 두 그룹으로 나눠야 하기도 한다.

둘째, formal verification step 이다. clear box implementation 을 작성하기 전에 팀은 black box specification 과 state box refinement 를 작성하고, state box 가 black box 와 동등함을 손으로 증명한다. 이는 pencil-and-paper proof 이며 proof assistant 가 아니다. 작동하지만 대부분의 팀이 갖추지 못한 시간과 training 이 필요하다.

세 번째 practice 인 statistical process control 을 통한 incremental development 는 이미 sprint 를 하고 있다면 사실상 무료다. 작은 increment 를 ship 하고 increment 별 defect density 를 측정하며, increment 가 defect target 을 초과하면 process 를 중단해 method 의 어디가 잘못되었는지 파악한다. 이는 단지 “done” 의 더 엄격한 정의를 가진 data-driven retrospective 에 불과하다.

pragmatic subset: 구조는 유지하고 관료주의는 버리기

structural discipline 를 유지하고 organizational mandate 를 버리면 Cleanroom 의 defect reduction 의 대부분을 얻을 수 있다.

유지해야 할 것은 다음과 같다.

code 보다 먼저 contract 를 작성한다. Z notation 의 formal specification 이 아니다. input, output, precondition, postcondition 의 명확한 기술뿐이다. correct 이 무엇을 의미하는지 쓸 수 없다면 correct 한 code 를 작성할 수 없다.

state machine 을 명시적으로 encode 한다. 대부분의 bug 는 developer 가 불가능하다고 가정한 state transition 에 숨어 있다. logic 을 작성하기 전에 state 와 transition 을 table 이나 data structure 로 정의한다.

다른 사람에게 logic 을 test 하게 한다. authorship 과 verification 의 분리는 Cleanroom 의 가장 강력한 idea 다. 별도의 team 이 필요하지 않다. code 를 작성하지 않은 한 사람에게 test case 를 설계하게 하면 된다. 자신의 code 를 test 하면 자신의 assumption 을 test 하는 셈이다.

increment 별 defect density 를 측정한다. 각 phase 에서 몇 개의 bug 가 탈출하는지 추적한다. integration bug 가 계속 빠져나간다면 문제는 careless 한 developer 가 아니다. process 가 integration bug 를 존재하게 만드는 것이 문제다.

버려야 할 것은 다음과 같다.

no-execution rule 을 버린다. developer 가 자신의 code 를 실행하게 한다. 먼저 추론하는 discipline 은 이후 quick sanity check 를 허용하더라도 가치가 있다. 핵심은 compiler 를 돌리기 전에 생각하는 것이지 compiler 가 존재하지 않는 척하는 것이 아니다.

formal hand proof 를 버린다. avionics software 를 작성하는 것이 아니라면 pencil-and-paper proof 는 overkill 이다. property-based tests 와 type-driven design 으로 대체한다. 이들은 동일한 추론의 mechanized version 이며 CI 에서 동작한다.

statistical usage testing 요구사항을 버린다. 완전한 Cleanroom 은 code coverage 가 아닌 usage profile 에 대해 test 한다. 데이터가 있다면 훌륭하다. 없다면 property-based testing 과 mutation testing 으로 이미 사용 중인 tools 로 대부분의 동일한 confidence 를 얻을 수 있다.

Python 에서의 lightweight Cleanroom workflow

단일 module 에 대해 실제로 어떻게 보이는지. contract 부터 시작한다.

"""
Black Box: Token Bucket Rate Limiter

Stimuli: request(n), add_tokens(k)
Precondition: n > 0, k >= 0, capacity > 0
Postcondition:
  - request(n) grants iff available tokens >= n
  - request(n) reduces available tokens by n if granted
  - add_tokens(k) increases available tokens by k, capped at capacity
  - available tokens never negative, never exceeds capacity
"""

다음으로 state machine 을 encode 한다.

from enum import Enum, auto

class RateLimitState(Enum):
    READY = auto()      # tokens >= 1, requests may grant
    DEPLETED = auto()   # tokens == 0, requests deny

# Transitions depend on token count, not external events
# READY -> DEPLETED when tokens reach 0
# DEPLETED -> READY when tokens added above 0

다음으로 implementation 을 작성한다.

import time
from dataclasses import dataclass

@dataclass
class TokenBucket:
    capacity: int
    tokens: int
    refill_rate: float
    last_refill: float

    def _refill(self) -> None:
        now = time.monotonic()
        elapsed = now - self.last_refill
        added = int(elapsed * self.refill_rate)
        if added > 0:
            self.tokens = min(self.capacity, self.tokens + added)
            self.last_refill = now

    def request(self, n: int) -> bool:
        if n <= 0:
            raise ValueError("request must be positive")
        self._refill()
        if self.tokens >= n:
            self.tokens -= n
            return True
        return False

    def add_tokens(self, k: int) -> None:
        if k < 0:
            raise ValueError("cannot add negative tokens")
        self.tokens = min(self.capacity, self.tokens + k)

contract 는 docstring 에 있다. state machine 은 명시적이다. implementation 은 짧고 inspection 으로 verifiable 하다. 이는 완전한 Cleanroom 이 아니다. cowboy coding 도 아니다.

실제로 할 수 있는 verification step

완전한 Cleanroom 에서는 별도의 팀이 usage profile 에 기반해 statistical test 를 작성한다. pragmatic 버전에서는 property-based tests 를 작성하고 동료가 review 하게 한다.

from hypothesis import given, strategies as st

@given(
    capacity=st.integers(min_value=1, max_value=1000),
    initial=st.integers(min_value=0, max_value=1000),
    requests=st.lists(st.integers(min_value=1, max_value=100), max_size=50),
)
def test_token_bucket_never_overdrafts(capacity, initial, requests):
    bucket = TokenBucket(
        capacity=capacity,
        tokens=min(initial, capacity),
        refill_rate=0.0,
        last_refill=time.monotonic(),
    )

    for n in requests:
        granted = bucket.request(n)
        assert bucket.tokens >= 0
        if granted:
            # tokens were deducted, so pre-request balance was sufficient
            pass
        else:
            # request denied, current tokens insufficient
            assert bucket.tokens < n

이 test 는 특정 output 을 check 하지 않는다. invariant 를 check 한다: bucket 은 가진 token 보다 더 많이 grant 하지 않는다. 이는 Cleanroom proof 의 property-based version 이다. 자동으로 동작하고 생각하지 못했던 edge case 를 찾으며 별도의 verification team 을 필요로 하지 않는다.

trade-off 는 현실적인 것이다

pragmatic Cleanroom 은 공짜가 아니다. code 전에 contract 를 작성하려면 discipline 이 필요하다. 명시적인 state machine 은 code 가 “자명” 할 때 boilerplate 처럼 느껴진다. 다른 사람에게 logic 을 test 하게 하려면 조율이 필요하다.

실제 것만큼 강력하지도 않다. 완전한 Cleanroom 의 no-execution rule 은 REPL 이 한 keystroke 거리에 있을 때 재현할 수 없는 깊이의 추론을 강제한다. formal proof 는 properties 가 잘못되어 property-based tests 가 놓칠 수 있는 logical error 를 잡는다.

하지만 비교 대상은 pragmatic Cleanroom 대 완전한 Cleanroom 이 아니다. 비교 대상은 pragmatic Cleanroom 대 지금 하고 있는 것이다. 현재 process 가 1KLOC 당 20 defect 를 내고 pragmatic Cleanroom 이 5로 만들어준다면, 그것은 overhead 의 일부로 4배 개선이다.

가치가 있는 시점

모든 utility function 에 이것을 쓰지 마라. bug 가 비싸게 드는 code 에 써라: authorization, billing, distributed protocol, 3개 이상의 state 를 가진 state machine, production incident 를 두 번 이상 일으킨 것.

이것이 필요한 신호는 complexity 가 아니다. repeated surprise 이다. 팀이 test 나 production 에서 같은 category 의 bug 를 반복해서 찾는다면 문제는 developer 가 careless 하다는 것이 아니다. code 의 contract 가 정의되지 않아 “correct” 가 specified 되지 않은 것이 문제다.

한 개의 module 부터 시작하기

management 승인이나 process overhaul 이 필요하지 않다. 이전에 피해를 본 module 하나를 고른다. implementation 에 손대기 전에 docstring 에 contract 를 작성한다. state 와 transition 을 정의한다. 동료에게 code 를 보지 않고 test 를 작성하게 한다. CI 에서 property-based tests 를 돌린다.

그게 다다. 별도의 team 도, formal notation 도, 자신의 code 를 실행하는 금지도 없다.

Cleanroom 의 1KLOC 당 0.1 defect 는 magic 이 아니었다. 사람들이 build 하기 전에 correct 를 정의하도록 강제한 process 의 output 이었다. 그 효과의 대부분은 docstring 과 state machine table, 그리고 code 가 아닌 assumption 을 test 해주는 동료로 얻을 수 있다.