강한 직렬 가능성

URL: https://jepsen.io/consistency/models/strong-serializable

Title: Strong Serializability

비공식적으로, 강한 직렬 가능성(Strong Serializability, 일명 엄격한 직렬 가능성 Strict Serializability, Strict PL-SS, Strong 1SR 등)은 연산들이 어떤 순서로 발생한 것처럼 보이되, 그 순서가 해당 연산들의 실시간 순서와 일치해야 함을 의미한다. 예를 들어, 연산 A가 완료된 뒤 연산 B가 시작한다면, 직렬화(serialize) 순서에서 A가 B보다 앞서야 한다.

엄격한 직렬 가능성은 트랜잭션 모델이다. 연산(보통 “트랜잭션”이라 부름)은 순서대로 수행되는 여러 개의 원시(primitive) 연산을 포함할 수 있다. 엄격한 직렬 가능성은 연산이 원자적으로 일어남을 보장한다. 즉, 한 트랜잭션의 하위 연산들이 다른 트랜잭션의 하위 연산들과 서로 끼어들어(interleave) 실행되는 것처럼 보이지 않는다.

또한 이는 다중 객체 성질이다. 연산은 시스템 내 여러 객체에 작용할 수 있다. 실제로, 엄격한 직렬 가능성은 트랜잭션에 포함된 특정 객체들에만 적용되는 것이 아니라, _시스템 전체_에 적용된다. 연산은 “모든 고양이들의 집합” 같은 술어(predicate)에도 작용할 수 있다.

엄격한 직렬 가능성은 완전 가용(total availability)하거나 스티키 가용(sticky availability)일 수 없다. 네트워크 분할이 발생하면 일부 또는 모든 노드가 진행을 하지 못하게 된다.

엄격한 직렬 가능성은 직렬 가능성과 선형화 가능성을 함의한다. 엄격한 직렬 가능성을 “트랜잭션 다중-객체 연산들에 대한 직렬 가능성의 전순서(total order)”에 “선형화 가능성의 실시간 제약”을 더한 것으로 생각할 수 있다. 또는 엄격 직렬 가능 데이터베이스를, 객체의 상태가 전체 데이터베이스인 하나의 선형화 가능 객체로 볼 수도 있다.

형식적으로

Herlihy와 Wing이 선형화 가능성(linearizability)을 소개했을 때, 그들은 엄격한 직렬 가능성을 실시간 순서와 양립(compatible)하는 직렬 가능 시스템으로 정의했다.

히스토리는 트랜잭션들이 순차적으로 실행되는 것처럼, 즉 서로 끼어들지 않고 실행되는 히스토리와 동등하다면 직렬 가능하다. (부분) 선행(precedence) 순서는 서로 겹치지 않는 트랜잭션 쌍에 대해 자명한 방식으로 정의될 수 있다. 히스토리는 순차 히스토리에서의 트랜잭션 순서가 그들의 선행 순서와 양립한다면 엄격히 직렬 가능하다.

“자명한 방식”이란 트랜잭션 A가 트랜잭션 B보다 앞선다는 것을, A가 완료된 후 B가 시작하는 경우로 정의한다는 뜻이다. 이는 선형화 가능성에서의 실시간 제약이다.