CCS

Calculus는 흔히 미적분학으로 번역된다. 그런데 수학에는 두 개의 Calculus가 있다. ‘The Calculus’와 ‘A Calculus’이다. 미적분학은 ‘The Calculus’를 말한다. 그렇다면 ‘A Calculus’란 무엇인가? 이것은 ‘문자나 숫자, 기호 등을 사용하여 계산 혹은 계산 과정을 표현하는 것​§​‘을 의미한다. 예를 들어 우리는 시속 100킬로미터로 달리는 자동차의 주행 거리를 다음과 같이 수학적으로 표현한다.

y = 100 \times x

관계형 데이터베이스에는 관계 논리relational calculus라는 것이 있다. 우리가 관계형 데이터베이스에서 사용하는 질의문query이 사실은 관계 논리에 의해 만들어진 수식이다.

CCS는 Calculus of Communicating Systems의 약자이다. 통신하는 시스템들을 수학적으로 표현하는 것을 의미한다. 왜 굳이 이렇게 수학적으로 표현해야만 할까? 일단 무엇인가가 수학적으로 표현되면 우리는 수학에 존재하는 각종 방법론을 거기에 적용할 수 있게 된다.

밀너가 이 분야에 관심을 가진 시기는 상당히 이르다. 스탠퍼드에서 LCF 시스템을 개발하던 시절에 이미 그는 동시성concurrency에 관심을 가졌다.

그런 와중에 나는 어찌하다 보니 동시성에 관심을 가지게 되었습니다. 특별히 동시성을 검증하겠다고까지 생각한 것은 아니었지만 서로 상호작용을 하는 오토마타에 관해 고민했던 기억이 있습니다. 나는 오토마타 이론이 그 일에 적합하지 못하다는 생각을 했습니다. 왜냐하면 두 개의 오토마타가 서로 상호작용하는 것이 어떤 것인지를 오토마타 이론은 설명하지 못했습니다.​2​

1970년대 말에 그는 CCS 연구에 본격적으로 뛰어들었다. 그는 상호작용하는 복수 개의 기계를 가정했다. 각 기계 자체는 순차적으로 동작한다고 보았다. 따라서 기계 자체의 동작은 기존의 수학적 모델, 예를 들면 λ-calculus에 의해 표현이 가능하지만, 기계 사이의 동작은 새로운 모델이 필요했다. 기계 사이의 상호 작용이란 결국 기계가 뭔가를 주고받는 것이므로 통신communication이었다. 그래서 그가 만드는 모델은 ‘통신하는 시스템communicating system‘을 위한 calculus였다.

CCS에서는 각 기계의 동작을 오토마타로 모델링한 후에 이를 다시 트리 구조로 변환하여 수식으로 표현한다.

그런 후에 기계 사이의 상호 작용을 다루기 위해 아래와 같이 몇 가지 수식 구조를 도입했다.

Summation

두 개의 기계를 하나로 합치는 상황을 표현한다. 예를 들어 P라는 수식으로 표현되는 기계와, Q라는 수식으로 표현되는 기계가 같은 뿌리(root)에서 시작한다면 아래와 같이 표현한다.

P + Q
Action

기계의 뿌리(root)에 전이(transition) 조건을 추가한다. P라는 수식으로 표현되는 기계가 시작되기 위해 α라는 전이 조건이 필요하다면 다음과 같이 표현된다.

αP
Composition

동시적으로 수행되는 상황을 표현한다. 예를 들어 P라는 수식으로 표현되는 기계와, Q라는 수식으로 표현되는 기계가 동시적으로 수행된다고 하면 아래와 같이 표현한다.

P | Q
Restriction

이것은 두 기계 사이의 연결 링크를 감추기 위한 목적이다. 이는 수식을 단순화하기 위해 사용된다. P라는 수식에서 α라는 이름의 링크를 사라지게 하려면 다음과 같이 표현한다.

P \α

기계와 기계 사이의 통신을 묘사하기 위해서 CCS는 label이라는 개념을 사용한다. 이는 기계의 동작에 영향을 주는 외부 입력을 의미한다. Label이라는 이름이 붙은 이유는, 밀너가 오토마타 모형에서 출발했기 때문이다. 오토마타 모형에서 상태의 전이는 화살표로 표현되고 여기에 붙는 label은 외부 입력을 의미한다.

A라는 기계가 B라는 기계에게 영향을 주려면, 기계 B의 label을 통해야 한다. 만약 B의 label이 \alpha라고 한다면 여기에 연관된 A쪽 출력은 \bar\alpha이 된다. 이제 \alpha는 두 기계가 상호작용하는 링크의 이름이 된다. 후에 π-calculus에서는 channel이라고 바뀌었다.

Relabeling

기계에 사용된 label의 이름을 바꿔주는 일을 한다. 다음과 같이 표현된다.

P[S]

S는 label의 이름을 바꿔주는 규칙의 집합이다. 위의 수식이 의미하는 바는, S라는 규칙을 사용해서 P라는 수식에 있는 label의 이름을 바꾸라는 것이다. S의 예로는 b/a 같은 것을 들 수 있는데, a라는 label을 b로 바꾸라는 의미이다.

제각각 모델링된 기계들은 label 즉 port의 이름도 제각각으로 붙였을 가능성이 높다. 그래서 이 기계들끼리 연관된 port끼리 연결하여 링크를 만들려면 이름을 맞추어줄 필요가 생긴다. 이 과정을 수학적으로 묘사하기 위한 도입한 것이 relabeling이다.

CCS를 사용하면 무슨 일을 할 수 있을까? 복수 개의 프로세스들이 서로 통신하면서 동작할 때 이 프로세스들이 어떤 상태에 도달할 수 있는지를 따져볼 수 있다. 만약, 어떤 시작 조건이 발생해서 복수 개의 프로세스들이 동작하게 되었을 때 정상적인 종료 상태에 도달할 수 없는 상황이 발생한다면 곤란하다. CCS를 사용하면 이런 상황이 발생하는지를 판별할 수 있게 된다. 대표적인 예가 교착상태deadlock이다.

1 2 3 4 5 6