요청을 받은 프로그램이 언젠가 응답한다는 것을 어떻게 증명할까요?

프린터가 종이를 잘못 출력하지는 않지만, 대기 화면에서 영원히 머문다고 합시다. 잘못된 출력은 없으나 요청한 문서를 받지는 못합니다. 프로그램을 검사할 때는 이 두 문제를 따로 물어야 합니다.

하나는 실행 내내 지켜야 할 조건이고, 다른 하나는 요청 뒤 끝내 일어나야 할 사건입니다. 프누엘리의 1977년 논문은 상태의 순서와 사건의 관계를 논리식으로 적어, 계속 실행되는 프로그램의 정확성도 다룹니다.

상태는 한 단계에서 프로그램의 위치와 자료값을 기록한 것입니다. 다음 단계로 바뀌는 것을 전이라고 합니다. 아래 프린터 모형은 시작, 대기, 처리를 상태로 둡니다. 처리에서 대기로 돌아가는 이동에서 한 요청이 완료됩니다. 따라서 이 그림에서 완료는 이동 중 일어나는 사건입니다.

모든 상태를 S, 허용된 이동 관계를 R, 시작 상태를 s₀로 씁니다. 실행은 이 이동을 따라 나열한 상태의 순서입니다. 아래 모형은 대기에서 처리로 갈 수도 있고 계속 대기할 수도 있습니다.

카운터 n이 2라고 합시다. “n을 하나 줄일 차례”와 “n이 0인지 검사할 차례”에서는 다음에 할 일이 다릅니다. 따라서 숫자만 기록하면 실행을 정확히 추적할 수 없습니다.

원문은 프로그램 위치 π와 자료값 u를 함께 적습니다. 다음 표는 한 단계씩 실행할 때 위치와 값이 함께 바뀌는 예입니다.

두 작업 A와 B가 카운터에 1씩 더한다고 합시다. 각 작업이 값을 읽고, 1을 더하고, 저장하는 단계로 나뉘면 그 사이에 다른 작업이 끼어들 수 있습니다. 두 작업 모두 0을 먼저 읽으면 둘 다 1을 저장해 최종값이 1이 됩니다.

어떤 동작을 더 나눌 수 없는 한 단계로 볼지 정하는 것이 원자 단계의 설정입니다. 논문의 병행 모형은 여러 작업의 현재 위치와 공유 자료를 함께 기록합니다.

“항상 카운터가 0 이상이다”는 모든 실행 단계에서 검사할 조건입니다. 처음부터 끝까지 유지되는 성질을 불변성이라고 부릅니다. 반면 “요청이 오면 언젠가 완료된다”는 요청 시점과 그 뒤의 완료 시점을 연결하는 조건입니다.

논문은 뒤의 시간적 요구를 언젠가 성립할 조건라고 부릅니다. 이 글에서는 언젠가 성립해야 하는 조건으로 풀어 읽겠습니다. 대기만 영원히 반복하는 실행은 카운터의 불변성을 지키면서 요청 완료 조건에는 실패할 수 있습니다.

총정확성은 시작 조건이 성립하면 언젠가 종료 조건과 결과를 만족한다는 특수한 언젠가 성립할 조건로 볼 수 있습니다. 계속 도는 시스템에서는 요청이 들어오면 언젠가 처리된다는 같은 꼴을 반복해 씁니다.

아래 활동은 속성 문장을 불변성과 언젠가 성립할 조건로 나눕니다.

n은 자연수이고 처음 값이 2라고 합시다. n>0일 때만 1을 빼며, n=0이면 그대로 둡니다. 먼저 시작값 2는 0 이상입니다. 이어 어떤 허용된 이동에서도 0 이상이 유지되는지 확인합니다.

n>0인 자연수는 적어도 1이므로 n−1도 0 이상입니다. n=0일 때는 그대로 0입니다. 시작과 모든 이동을 확인했으므로 아무리 많은 단계를 거쳐도 n≥0이 유지됩니다. 이것이 실행에 대한 귀납 논증입니다.

앞의 카운터에서 n>0일 때 매번 반드시 1을 뺀다고 합시다. 2에서 시작하면 2, 1, 0으로 진행합니다. 일반적인 자연수에서 시작해도 양의 자연수를 계속 줄이는 과정은 끝없이 이어질 수 없습니다.

이 증명에는 실제로 줄어든다는 조건이 중요합니다. 2에서 그대로 대기하는 이동을 무제한 허용하면 n≥0은 유지되지만 0에 도달한다는 결론은 따라오지 않습니다. 원문은 이런 감소 논증과 필연적인 중간 사건을 연결하는 시간 추론을 비교합니다.

여러 처리기의 실행이 갈라지고 섞이므로 한 줄짜리 중간 사건 사슬만으로는 자연스러운 논증을 담기 어렵습니다. 프누엘리는 tense logic Kb를 고쳐 만든 더 풍부한 체계를 제안합니다.

이 체계는 실제 시계 값을 모든 명제에 붙이지 않고도 미래의 언젠가와 계속을 표현합니다. 시간의 필요한 구조만 논리에 넣으려는 선택입니다.

ER은 “한 사건 뒤에 다른 사건이 언젠가 온다”는 단언을 이어 쓰는 형식 체계입니다. Kb를 바탕으로 한 체계는 여러 작업이 섞인 실행의 시간 조건을 더 풍부하게 다룹니다. 여러 실행이 가능하다는 사실과, 한 실행 안에서 F·G를 읽는 일은 구별해야 합니다.

Fq는 현재를 포함해 앞으로 q가 성립하는 단계가 하나라도 있다는 뜻입니다. Gq는 현재와 그 뒤의 모든 단계에서 q가 성립한다는 뜻입니다. 아래에서는 q를 “출력이 완료된 상태”로 정합니다.

대기, 처리, 완료, 대기, 대기…라는 실행에서는 시작 시점의 Fq가 참이고 Gq는 거짓입니다. 완료 시점이 한 번 있지만 모든 시점이 완료 상태인 것은 아니기 때문입니다. G(p→Fq)는 요청 p가 발생하는 각 시점마다 그 시점 이후에 완료 q가 있다는 조건입니다.

작업 A와 B가 모두 계속 실행 가능한데 A만 영원히 선택한다면 B는 기다리기만 합니다. B의 코드만 검사해서는 이 지연을 막을 수 없습니다. 어느 작업을 다음에 실행할지 정하는 장치를 스케줄러라고 합니다.

공정성은 실행 가능한 작업을 끝없이 미루지 않도록 정하는 조건입니다. 아래에서는 두 작업이 계속 실행 가능한 단순한 상황을 가정합니다. 공정성을 어떤 의미로 요구하는지에 따라 허용되는 실행이 달라집니다.

원문은 producer-consumer 프로그램을 예로 들어 자료 관계와 제어 위치를 포함한 불변식으로 정확성을 증명합니다. 지역별 경우를 낱낱이 쓰는 대신 전역 불변식을 세워 검증 조건을 줄입니다.

이 사례는 시간 논리가 진행 성질만 다루는 도구가 아니라 기존 불변식 증명과 함께 쓰인다는 점을 보여 줍니다.

생산자는 자료를 만들어 버퍼에 넣는 작업이고, 소비자는 버퍼에서 자료를 꺼내 쓰는 작업입니다. 버퍼는 둘 사이의 임시 저장 공간입니다. 버퍼가 비어 있는데 꺼내지 않는다는 조건과, 들어간 자료가 언젠가 처리된다는 조건을 각각 확인할 수 있습니다. 이 설명은 원문 프로그램의 전체 증명을 대신하지 않습니다.

상태가 유한한 모형에서는 같은 상태를 반복하는 순환을 살펴볼 수 있습니다. 요청 이후 완료 상태를 한 번도 지나지 않고 계속 돌 수 있는 경로가 있다면, 언젠가 완료한다는 주장에 반례가 될 수 있습니다.

다만 그 경로가 처음 상태에서 도달 가능하고, 정해 둔 공정성 조건에도 맞아야 합니다. 그림의 대기 순환도 이 조건까지 확인해야 유효한 반례가 됩니다. 순환이 보인다는 이유만으로 곧바로 실패라고 판정하지 않습니다.

직선적이고 종료하는 프로그램에서는 한 위치를 지나기 전후가 비교적 분명합니다. 순환·비결정·병행 프로그램은 같은 위치를 여러 번 방문하고 서로 다른 처리기 단계가 섞입니다.

이때 제어 위치만으로 첫 방문과 다음 방문을 구분할 수 없습니다. 실행과 독립된 시간 순서를 논리적으로 유지해야 언젠가 성립할 조건를 정확히 말할 수 있습니다.

가능합니다. 프로그램을 상태 전이 시스템으로 보고 F와 G가 들어간 시간 명제를 쓰면, 멈추지 않는 프로그램에도 “항상 안전”과 “요청 뒤 언젠가 응답”을 증명할 수 있습니다.

다만 진행 결론은 전이 모형, 원자 단계, 초기 상태, 스케줄 공정성에 의존합니다. 오늘날의 선형시간논리 전체와 동일시하기보다 이 1977년 논문이 제시한 두 형식 체계와 범위를 정확히 읽어야 합니다.