동시성 모델과 형식 기법 (Concurrency Models & Formalism)

1. Overview

동시성 모델과 형식(Concurrency Models & Formalism)은 여러 연산이 "동시에" 진행되는 병렬·비동기 시스템에서 경쟁 조건(Race Condition), 교착 상태(Deadlock), 데이터 불일치를 방지하는 다양한 동시성 추상화 모델을 수학적·실용적으로 분석합니다.

학습자는 공유 메모리(Shared Memory) 방식의 뮤텍스(Mutex)/세마포어(Semaphore) 잠금 기반 동시성이 어떤 위험을 내포하는지 살펴봅니다. 나아가 액터 모델(Actor Model, Erlang/Akka), CSP(Communicating Sequential Processes, Go Channel), STM(Software Transactional Memory, Haskell), **async/await 코루틴(Coroutine)**의 네 가지 현대 동시성 모델을 비교합니다. 마지막으로 피터슨 알고리즘(Peterson's Algorithm), 아므달의 법칙, 린드 메이어 시스템 같은 동시성 형식(Formalism)을 통해 병렬 시스템 설계의 이론적 기반을 확보합니다.

2. Scope & Boundaries

In-Scope

• 공유 메모리 동시성 (Shared Memory): Mutex/Semaphore, 임계 구역(Critical Section), Race Condition, Deadlock, 피터슨 알고리즘.
• 메시지 전달 모델 (Message Passing): 액터 모델(Actor Model, 상태 격리 + 메시지), CSP(Channel 기반 동기화), Go Goroutine/Channel.
• 비동기 I/O 모델 (Async I/O): 이벤트 루프(Event Loop), Callback Hell, Promise/Future, async/await 코루틴.
• STM과 동시성 형식 (STM & Formalism): Software Transactional Memory, 선형 논리(Linear Logic), 프로세스 대수(CCS/π-Calculus 개요).

Out-of-Scope

• CPU 스케줄링 알고리즘: OS 커널의 태스크 스케줄링 정책 → 03-02. Process & Concurrency Mechanics 영역.
• 분산 시스템 합의 알고리즘(Raft/Paxos): 분산 노드 간 합의 → 05-04. Distributed Systems 영역.

Boundaries

• 동시성(Concurrency) vs 병렬성(Parallelism): 동시성은 "한 번에 여러 일을 처리하는 구조(Structure)"이며 단일 코어에서도 가능합니다(시분할). 병렬성은 "여러 일이 물리적으로 동시에 실행(Execution)"되며 다중 코어가 필요합니다. Go Goroutine은 동시성(단일 스레드에서 수천 Goroutine 전환 가능)이며, 실제 병렬성은 GOMAXPROCS 코어 수에 의존합니다.

3. Counterexample

• 락 순서 역전과 교착 상태 (Lock-order Deadlock): 스레드 A가 락 L1을 잡고 L2를 기다리고, 동시에 스레드 B가 락 L2를 잡고 L1을 기다리는 고전적 교착 상태(Deadlock). 두 스레드가 서로 상대방이 잡은 락을 기다리며 영원히 멈추는 시나리오입니다. 락 획득 순서를 전역적으로 일관되게 정의(항상 L1 → L2 순서)하거나, 타임아웃(Timeout) 락 획득으로 회피해야 합니다.
• Double-Checked Locking의 메모리 순서 함정 (DCLP Bug): 싱글턴(Singleton) 패턴에서 if instance is None: lock.acquire(); if instance is None: instance = Singleton() 같은 이중 확인 잠금(DCLP). CPU의 명령어 재순서(Instruction Reordering)나 컴파일러 최적화로 인해, instance에 객체 주소가 먼저 쓰여지고 __init__()이 아직 완료되지 않은 상태를 다른 스레드가 읽어 반쯤 초기화된 객체를 얻는 버그가 발생합니다. C++11의 std::atomic, Java의 volatile 메모리 순서(Memory Ordering) 보장이 필수입니다.

4. Prerequisites

• 스레드와 프로세스 (Basic): 스레드가 공유 메모리를 사용하는 실행 단위임을 이해해야 합니다. (03-02 Process & Concurrency Mechanics)
• 세마포어와 뮤텍스 (Basic): 임계 구역 보호의 기본 메커니즘. (03-02-02 Mutex & Synchronization)

5. Learning Map

6. Learning Topics

Basic

Core Topic 01: 공유의 위험과 잠금의 철학, 공유 메모리 동시성 위험 (Shared Memory Perils)

• Why to Learn: "멀티스레드 프로그램을 짰는데 가끔 이상한 결과가 나와요"라는 비재현성 버그(Heisenbug)의 근본 원인이 공유 변수에 대한 비원자적 접근(Race Condition)일 수 있음을 진단하고, 올바른 잠금 설계로 줄이기 위해서입니다.
• What to Learn:
  • Concepts: 임계 구역(Critical Section), 상호 배제(Mutual Exclusion), 경쟁 조건(Race Condition), 교착 상태(Deadlock), 기아(Starvation), 피터슨 알고리즘(소프트웨어 뮤텍스 증명).
  • Skills: 락 그래프(Lock Graph)로 교착 상태 탐지, 타임아웃 락 획득.
  • Tools: Python threading.Lock, Java synchronized, Linux pthread_mutex.
• How to Learn:
  • 1단계: Race Condition 재현. Python counter = 0; [Thread: counter += 1] × 1000. 실제 실행하면 GIL 없이는 1000 미만의 결과가 나오는 비원자적 접근 문제(load-increment-store 3단계 사이에 스레드 전환)를 분석합니다.
  • 2단계: 피터슨 알고리즘: 소프트웨어 뮤텍스 구현(락 하드웨어 없이 두 스레드 상호 배제). flag[i]=True; turn=j; while flag[j] and turn==j: pass 패턴으로 두 스레드가 동시에 임계 구역에 들어가지 못함을 증명합니다.
• Implement: 파이썬 threading.Lock() 보호 카운터. Lock 없는 버전 vs Lock 있는 버전의 1000 스레드 실행 결과 비교. 교착 상태 시뮬레이션: 스레드 A(L1→L2), 스레드 B(L2→L1) 락 획득 후 서로 대기하여 프로그램이 영구 정지하는 데모.

Recommended

Core Topic 02: 고립된 상태와 메시지만, 액터와 CSP 모델 (Actor Model & CSP)

• Why to Learn: Erlang의 99.9999999% 가용성(Ericsson AXD301 교환기), Go의 수십만 Goroutine 서버, Akka의 분산 액터 시스템이 공통적으로 "공유 상태 없음(No Shared State) + 메시지 전달(Message Passing)"을 동시성의 핵심 원칙으로 채택한 이유를 이해하기 위해서입니다.
• What to Learn:
  • Concepts: 액터 모델(Actor: 자체 상태 + 메일박스 + 동작 핸들러), CSP(Communicating Sequential Processes, Go Channel), Goroutine + Channel.
  • Skills: Go go func(){}() + chan int, 채널 방향(chan<-, <-chan), select 멀티플렉싱.
  • Trade-offs: 액터 모델은 위치 투명성(Location Transparency, 같은 코드로 로컬/원격 액터 메시지 전송)을 제공하여 분산 시스템에 자연스럽지만, 비동기 메시지 처리로 응답 순서 보장이 어렵습니다. CSP는 동기 채널로 명시적 핸드쉐이크가 가능하지만 분산 시스템에서 채널이 네트워크를 넘을 수 없습니다.
• How to Learn:
  • 1단계: Go CSP: ch := make(chan int). go func(){ ch <- 42 }(). val := <-ch. 채널을 통해 두 Goroutine이 동기화(전송 측은 수신 측이 받을 때까지 대기)하는 CSP 동작을 분석합니다.
  • 2단계: Go select: 여러 채널 중 준비된 채널 우선 처리. select { case v := <-ch1: ... case v := <-ch2: ... case <-time.After(1s): ... }. Timeout 구현에 사용하는 방식을 살펴봅니다.
• Implement: 파이썬 asyncio.Queue로 액터 모델 시뮬레이션. Actor 클래스는 asyncio.Queue 메일박스를 가지고 async def run() 루프에서 메시지 처리. PingActor ↔ PongActor 메시지 왕복 10회 후 종료. Go 채널 패턴: 파이썬 asyncio Channel 기반 팬아웃(Fan-out, 1 생산자 → N 소비자) 구현.

Practical

Core Topic 03: 단일 스레드 비동기 처리, 이벤트 루프와 async/await (Async/Await & Event Loop)

• Why to Learn: Node.js가 싱글 스레드로 초당 10만 요청을 처리하고, Python asyncio가 수천 개의 동시 HTTP 연결을 관리하는 비동기 I/O의 핵심인 이벤트 루프(Event Loop)와 코루틴(Coroutine)의 동작을 이해하기 위해서입니다.
• What to Learn:
  • Concepts: 이벤트 루프(Event Loop), 코루틴(Coroutine, 일시 정지/재개 가능한 함수), async/await, Future/Promise, Callback Hell → Promise → async/await 진화.
  • Skills: async def, await, asyncio.gather(), asyncio.create_task(), I/O 바운드 vs CPU 바운드 차이.
  • Trade-offs: asyncio(단일 스레드 이벤트 루프)는 I/O 바운드 작업(네트워크, DB)에 효율적이지만, CPU 바운드 작업(이미지 처리, 암호화)은 이벤트 루프를 블록(Block)하여 다른 코루틴 실행을 지연시킬 수 있습니다. CPU 바운드는 ProcessPoolExecutor로 별도 프로세스에서 처리해야 합니다.
• How to Learn:
  • 1단계: async def fetch_url(url): await asyncio.sleep(1). asyncio.gather(fetch_url(url1), fetch_url(url2), fetch_url(url3)). 세 함수가 각각 1초 걸리지만 gather로 병렬 실행 시 총 1초 만에 완료되는 비동기 동시성 동작을 분석합니다.
  • 2단계: 이벤트 루프의 내부 순환: 이벤트 큐에서 완료된 I/O 이벤트를 꺼내 해당 콜백(코루틴)을 재개. CPU 연산 없이 I/O 대기 중에는 이벤트 루프가 다른 코루틴을 처리하는 협력적 멀티태스킹 방식을 살펴봅니다.
• Implement: 파이썬 asyncio 실습. asyncio.sleep(0.1)으로 I/O 시뮬레이션. 10개 URL 동시 fetch 시뮬레이션: 순차 실행(10 × 0.1s = 1s) vs asyncio.gather 병렬(≈0.1s) 시간 비교 측정. asyncio.Semaphore(5)로 동시 연결 수 제한하는 속도 조절(Rate Limiting) 구현.

Advanced

Core Topic 04: 메모리 트랜잭션과 프로세스 대수, STM과 동시성 형식 (STM & Formal Concurrency)

• Why to Learn: 락(Lock)을 직접 다루지 않고 데이터베이스 ACID 트랜잭션처럼 메모리 쓰기를 원자적으로 커밋/롤백하는 STM(Software Transactional Memory)과, 동시 프로세스를 수학으로 기술하는 π-Calculus를 이해하여 고급 동시성 시스템 설계 역량을 확보하기 위해서입니다.
• What to Learn:
  • Concepts: STM(Optimistic Concurrency, TVar, atomically, retry/orElse), 락-프리 프로그래밍(CAS, Compare-And-Swap), π-Calculus(프로세스 대수, 채널 이름 전달).
  • Skills: Haskell STM 패키지, Java AtomicInteger.compareAndSet(), 락-프리 스택 구현.
  • Tools: Haskell stm 라이브러리, Java java.util.concurrent.atomic.
• How to Learn:
  • 1단계: STM 철학: 락 없이 낙관적(Optimistic)으로 트랜잭션 실행. atomically(account.deduct(100), account2.add(100)) 실행 중 다른 트랜잭션이 동일 계좌 수정 시 자동 롤백 + 재시도. 충돌이 드문 경우(Contention Low) 락보다 높은 처리량을 낼 수 있는 이유를 분석합니다.
  • 2단계: CAS(Compare-And-Swap): AtomicInteger.compareAndSet(expected, update). 현재 값이 expected와 같으면 update로 교체(원자적으로). 실패하면 재시도 루프. 락 없이 원자적 카운터 증가(++)를 구현하는 락-프리 동시성 방식을 살펴봅니다.
• Implement: 파이썬 TVar + atomically STM 시뮬레이션. TVar(value) 클래스로 트랜잭션 변수. atomically(lambda: [a.set(a.get()-100), b.set(b.get()+100)]) 로 원자적 계좌 이체. 동시 10개 스레드 이체 시 총 잔액 보존 검증. Python threading CAS 시뮬레이터: compare_and_set(expected, update) 메서드로 락-프리 카운터 증가 구현.

7. Terminology

8. References

Primary

• [P1] CS2023 - Parallel and Distributed Computing (PDC) - Concurrency Models
• [P5] SFIA - Software Design (SWDN) - Concurrent Architecture

Secondary

• [Seven Concurrency Models in Seven Weeks] Paul Butcher - Actor, CSP, STM overviews
• [Communicating Sequential Processes] C.A.R. Hoare - The theoretical foundation of CSP

Industry

• [Go Documentation] - Goroutines and Channels (CSP Implementation)
• [Erlang/Akka Documentation] - Actor Model and Fault Tolerance

9. Final Checklist

Primary

• 공유 메모리(Shared Memory) 모델에서 뮤텍스(Mutex) 락을 잘못 사용했을 때 발생하는 데드락(Deadlock)과 데이터 레이스(Data Race)의 차이를 설명할 수 있는가?
• 동시성(Concurrency)은 논리적 작업 분할이고, 병렬성(Parallelism)은 물리적 동시 실행이라는 코어와 스레드 관점의 차이를 구분할 수 있는가?

Secondary

• Actor 모델(Erlang/Akka)이 내부 상태를 은닉하고 오직 메일박스(큐)의 비동기 메시지 패싱만으로 락-프리(Lock-free) 동시성을 달성하는 구조를 증명할 수 있는가?
• CSP 모델(Go 언어)에서 버퍼 없는 채널(Unbuffered Channel)이 통신과 동시에 스레드 동기화(Rendezvous) 락을 어떻게 대체하는지 설명할 수 있는가?

Industry

• STM(Software Transactional Memory)이 낙관적 동시성(Optimistic Concurrency)을 사용해 뮤텍스 직접 관리를 줄이지만, 왜 극심한 경합 시 재시도(Retry) 성능 병목을 일으키는지 논증할 수 있는가?
• 비동기 콜백 지옥(Callback Hell)을 해결하기 위한 Promise/Future와, 이를 언어 차원에서 동기 코드처럼 작성하게 해주는 async/await 코루틴(Coroutine) 상태 머신의 변환 과정을 아키텍처링 할 수 있는가?