형식 정제(Formal Refinement)를 통한 프로듀서 주도 스트림 프로토콜 설계

코루틴은 제너레이터와 비동기 함수, 그리고 파이프를 통해 통신하는 프로세스의 형태로 동시성 프로그래밍 관행 전반에 걸쳐 광범위하게 확산되었습니다. 우리는 Python에서 코루틴을 사용하여 단일 스레드 Unix 스타일의 파이프라인을 만들고자 했습니다. 하지만 현재 Python에서 사용 가능한 솔루션들은 사용하기가 번거롭습니다. JavaScript push-stream 프로토콜이 좋은 대안처럼 보였습니다. 그러나 이 프로토콜의 명세는 불완전하고 모호합니다. 우리는 TLA$^{+}$와 TLC 모델 체커를 사용하여 이 프로토콜을 재도출하고, 프로토콜별 검증 도구를 얻었습니다. 본 논문에서 우리는 다음 기능을 갖춘 push-stream 프로토콜에 대한 형식적 명세를 제시합니다: 1) 동기식(synchronous) 및 비동기식(asynchronous) 모듈을 원활하게 결합하여 각 모듈 내에서 선택 사항을 캡슐화하고; 2) 유한 버퍼를 사용하지 않고 흐름 제어(flow control)를 제공하며; 3) 우아하고 명확하게 종료되고; 4) 힙(heap)에 객체를 동적으로 할당할 필요가 없습니다. 예상되는 동작을 완전히 설명하는 것 외에도, 우리의 명세는 다음을 통해 원래의 설계를 개선합니다: 1) 중간 파이프라인 모듈의 입력과 출력이 독립적으로 종료될 수 있도록 허용하고; 2) 잘못된 재개(resuming)를 방지하기 위해 모듈이 실행 환경에 보류 중일 때 명시적으로 보고합니다. 우리는 이 프로토콜을 일련의 정제 단계(refinement steps)로 명세하고, 동치성(equivalence)을 통해 추상적인 모듈이 수행할 수 있는 것에 대한 명세를 도출합니다. 그런 다음 후자를 적합성을 검증할 수 있는 모듈 체커(module checker)로 정제합니다. 우리는 TLC를 사용하여 모든 명세의 핵심 속성과 정제 단계의 유효성을 검증했습니다. 보충 자료에는 모든 TLA$^{+}$ 명세가 제공되며, 이 프로토콜이 원래 JavaScript 모듈 전체 집합(superset)을 구현하기에 충분히 표현력이 있다는 점과 Python 대안 및 Unix 파이프와의 성능 비교를 보여줍니다.