분산 시스템에서 “보상 트랜잭션(compensating transaction)”에 대한 수학·형식 이론 관점 설명 250523

q1: 분산 시스템에서 “보상 트랜잭션(compensating transaction)”에 대한 수학·형식 이론 관점 설명

a1:

해당 예시는 분산 시스템에서 “보상 트랜잭션(compensating transaction)”을 사용한 전형적인 사례입니다. 수학·형식 이론 관점에서 보면 크게 다음 세 가지 축으로 설명할 수 있습니다.

⸻

1. 트랜잭션 이론(Transaction Theory) 및 ACID 성질
• 트랜잭션(transaction) 은 시스템의 상태(state)를 일관성 있게 변화시키기 위한 기본 단위로 정의됩니다.
• ACID 성질
1. 원자성(Atomicity): 트랜잭션 전체가 모두 실행되거나 하나도 실행되지 않아야 함
2. 일관성(Consistency): 트랜잭션 전후에 시스템의 제약 조건(constraint)이 성립해야 함
3. 고립성(Isolation): 동시에 수행되는 트랜잭션 간 간섭이 없어야 함
4. 지속성(Durability): 완료된 트랜잭션의 결과는 영구히 저장되어야 함
 – 좌석 확보(1) → 결제 승인(2) → 알림 발송(3) 과 같이 단계가 진행될 때, 단계 2)에서 실패하면 “원자성”을 보장하기 위해 1)단계에서 이미 확보한 좌석을 해제하는 롤백이 필요합니다.

⸻

2. 보상 트랜잭션과 사가 패턴(Saga Pattern)
• 전통적인 2-Phase Commit(2PC) 방식은 모든 참여 노드(예: 좌석 시스템, 결제 시스템)가 동시에 커밋해야 하므로, 결제 실패 시 전체를 롤백하는 데 오랜 시간이 걸리거나 교착(deadlock)이 발생할 수 있습니다.
• 사가(Saga) 패턴은 이를 해결하기 위해 각 단계마다 “정방향 트랜잭션”과 “보상 트랜잭션(compensation)” 쌍을 정의합니다.

단계1: 좌석 확보    → 보상1: 좌석 해제  
단계2: 결제 승인    → 보상2: 결제 취소(환불)  
단계3: 이메일 발송 → 보상3: 이메일 취소(불가피 시 무시)


• 단계 2에서 실패하면 보상1을 즉시 실행하여 “좌석 확보”를 원상복구합니다.
• 수학적으로는 각 단계가 부분 트랜잭션(partial transaction) 으로, 전체 사가를 하나의 비원자적 트랜잭션으로 보는 모델링을 합니다.

⸻

3. 형식 모델링(Formal Modeling)

이러한 보상 흐름을 엄밀히 분석·검증하기 위해 아래와 같은 수학·형식 모델이 사용됩니다.

유한 상태 머신(FSM)
- 각 단계와 보상 단계를 상태(state)와 전이(transition)로 모델링

Petri 네트(Petri Net)
- 동시성(concurrency)과 비결정성(nondeterminism)을 포함해 트랜잭션 흐름 및 롤백을 그래픽·수식으로 표현

프로세스 대수(Process Algebra)(CSP, π-Calculus 등)
- 프로세스 간 통신·동기화 규칙을 대수적 연산자로 기술, 보상 트랜잭션의 순서·동시 실행 조건 등을 엄밀히 정의


예를 들어 Petri 넷에서는 “좌석 확보” → “결제 승인” 간에 토큰(token)이 흐르도록 하고, “결제 승인 실패” 시 보상 트랜잭션으로 연결된 별도의 전이를 통해 토큰을 원래 장소로 되돌립니다.

⸻

정리
1. 트랜잭션 이론(ACID)으로 원자성을 확보하고,
2. 사가 패턴(Saga)으로 각 단계별 보상 로직을 정의하며,
3. Petri Net / Process Algebra 같은 형식 모델로 전체 흐름을 검증

을 통해 “결제 실패 시 좌석 확보 해제” 같은 보상 시나리오를 수학·형식적으로 설계·검증할 수 있습니다.