선형화가능성
선형화가능성(Linearizability)은 병행 프로그래밍에서 어떤 연산이 즉시 효과가 나타나는 것처럼 보이는 성질을 가리킨다. 사용자는 구현 세부 사항을 무시해도 좋지만, 성능에는 영향이 있다. 반대로 어떤 연산이 원자적이지 않으면, 병행 연산(들)이 끼치는 추가적이고 돌발적인 영향을 이해하고 대처해야 한다. 그리고 당연히 이런 문제는 재현하기 힘들고 디버그하기 힘들다.
데이터베이스의 ACID 속성에 익숙한 경우에 병행 프로그래밍에서 원자성은 분리 수준에 관련된 것이며, 직렬화보다 더 강력하다는 점에 주의하자. 데이터베이스에서는 원자성에 관해 다른 정의를 가진다.
역사
[편집]선형화가능성은 1987년에 Herlihy와 Wing은 무모순성 모델로써 도입되었다. 원자성은 "원자적인 연산은 다른 병행 연산에 의해 중단되지 않는 연산이다"와 같이 연산이 언제 시작되고 종료되는지 모호하다. 선형화 가능성은 이 정의를 더 제한한다.
원자적 객체는 그 순차 정의로 즉시 완벽히 이해 가능하며, 병렬로 실행된 연산들이 언제나 하나씩 차례대로 효과가 나타난다. 어떤 모순성도 나타나지 않는다. 특히 선형화 가능성은 모든 연산에서 시스템의 불변량을 볼 수 있으며 이를 유지한다. 모든 연산이 개별적으로 불변량을 보존하면, 시스템 전체로 봐서도 그러하다.
수학적 정의
[편집](실행) 이력은 일군의 스레드가 만들어낸 일련의 메서드 호출(invocation)과 응답(response)의 수열이다. 각 메서드 호출은 그에 해당하는 응답을 가지며, 이를 이용하여 임의의 객체의 사용을 모델링한다.
예를 들어 스레드 A, B가 어떤 락을 잡으려 시도하고, 실패하면 백오프하는 경우를 생각해보자. 이는 두 스레드가 락 연산을 호출하고, 한 스레드는 "성공" 응답을, 다른 한 스레드는 "실패" 응답을 받는 것으로 모델링된다.
| A lock 메서드 호출 | B lock 메서드 호출 | A 실패 응답 | B 성공 응답 |
순차 이력은 모든 메서드 호출이 즉시 응답이 따른 형태의 이력이다. 순차 이력의 경우 어떤 병행성도 가지고 있지 않으며, 뭔가 추론할 것도 없다. 그렇지만 직전에 든 예는 순치 실행이 아니며(즉 순차 이력도 아니며), 이에 따라 추론할 만한 부분이 생긴다. 이를 위해 선형화 가능성이 존재한다.
어떤 이력은 다음 조건을 만족할 때 선형화가능이다.
- 메서드 호출과 응답의 순서를 재배치해서 순차 이력이 나올 수 있으며
- 그 순차 이력이 해당 객체의 순차 정의에 어긋나지 않고
- 원래의 이력(병행해서 실행한 이력)에서 어떤 응답이 다른 어떤 메서드 호출에 선행했다면, 재배치된 이력에서도 그 순서가 유지되어야 한다.
이 중 처음 두 조건은 직렬화가능성을 정의한다. 다만 직렬화가능성에선 응답 순서가 어떤 순서여도 된다. 세 번째 조건은 선형화 가능성에만 해당한다. 이 부분이 Herilhy와 Wing이 기여한 부분이다.
위에서 예로 든 순서를 두 가지 순서로 재배치 해보겠다.
| A lock 메서드 호출 | A 실패 응답 | B lock 메서드 호출 | B 성공 응답 |
여기서는 객체가 잠기지도 않았는데 A의 lock이 실패하기 때문에, 위에서 언급한 규칙 중 두 번째에 위배된다. 다시 이를 재배치해서,
| B lock 메서드 호출 | B 성공 응답 | A lock 메서드 호출 | A 실패 응답 |
처럼 만들면 정확한 순차 이력이 된다. 여기서는 응답 뒤에 메서드 호출이 있는 경우가 없기 때문에, 그냥 lock을 호출한 순서는 재배치했다.
선형화가능성 vs. 직렬화가능성
[편집]두 개의 스레드가 하나의 락을 통해 상호작용하는 이력을 예로 설명하겠다.
다음과 같은 실행 이력이 있다.
| A lock 호출 시작 | A 성공 응답(lock) | B unlock 호출 시작 | B 성공 응답(unlock) | A unlock 호출 시작 | A 성공 응답(unlock) |
이 이력은 선형화가능하지 않다. 응답의 순서를 유지하면서 이를 동등한 다른 순차 이력으로 바꿀 방법이 없기 때문이다. 그러나 직렬화 가능성만 놓고 보면, B의 unlock을 맨 앞으로 옮기고, 객체가 이력 시작에 이미 잠긴 상태라고 가정하여 재배치할 수 있다. 그러면 다음과 같은 순서가 된다.
| B unlock 호출 시작 | B 성공 응답(unlock) | A lock 호출 시작 | A 성공 응답(lock) | A unlock 호출 시작 | A 성공 응답(unlock) |
A, B 사이에 다른 의미의 통신이 없다면, 이는 말이 된다.
이런 문제로 인해, 개별 객체를 별도로 생각하려면 선형화 가능성을 따르는게 좋다. 재배치 규칙 3번째 때문에 개별 객체가 선형화가능하면, 전체 시스템도 선형화 가능해지기 때문이다.
선형화 지점
[편집]선형화 가능성을 다음과 같이 정의할 수도 있다:
- 모든 함수 호출은 함수 시작과 응답 사이의 어느 지점에 선형화 지점을 가진다.
- 모든 함수 호출은 선형화 지점에서 즉시 효과를 내는걸로 보이며, 이는 순차 정의에 따른 동작을 한다.
이 정의는 훨씬 증명에 용이하다. 또한 매우 직관적이다. 그리고 즉시 효과가 나타난다는 속성 혹은 나눌 수 없다는 점 때문에 '선형화가능성' 대신 원자적이란 용어를 쓰게 만들기도 한다.