고루틴
노트
이 예제는 원래 내 블로그에 게시했던 것으로, 여기서는 약간 수정해서 옮겼다.
Chris Siebenmann은 Go에서도 동시성은 여전히 쉽지 않다(Even in Go, concurrency is still not easy)에서 데드락(deadlock)에 빠지는 Go 코드 예시를 든다:
1 func FindAll() []P { //P = process data
2 pss, err := ps.Processes()
3 [...]
4 found := make(chan P)
5 limitCh := make(chan struct{}, concurrencyProcesses)
6
7 for _, pr := range pss {
8 limitCh <- struct{}{}
9 pr := pr
10 go func() {
11 defer func() { <-limitCh }()
12 [... get a P with some error checking ...]
13 found <- P
14 }()
15 }
16 [...]
17
18 var results []P
19 for p := range found {
20 results = append(results, p)
21 }
22 return results
23 }
그의 말을 빌리면 이렇다:
버그는, 고루틴(goroutine)들이 결과를 버퍼 없는 found 채널(channel)로 보낸 뒤에야 limitCh에서 수신해 토큰을 반납하는 반면, 메인 코드는 루프 전체를 다 돈 뒤에야 found에서 수신을 시작하며, 게다가 메인 코드가 루프 안에서 토큰을 가져가다가 남은 토큰이 없으면 블록된다는 점이다.
설계만 검증하는 대신 TLA+ 스펙으로 코드를 직접 검증하는 좋은 예다.
미리 계획하기
이 문제에 어떻게 접근할지 먼저 좀 생각해 두고 시작하는 게 좋다. 무언가를 정형적으로 명세하는 일에는 두 부분이 있다: 시스템을 기술하는 것과 시스템의 속성(property)을 기술하는 것이다. 이번에는 데드락만 찾으면 되므로 두 번째 부분은 무시해도 된다. 타입 불변식(type invariant) 같은 온전성 검사용 속성을 추가하는 것이 좋은 모델링 습관이겠지만, 꼭 필요하지는 않다.
먼저 TLA+로 모델링할지 PlusCal로 할지 골라야 한다. Go 코드가 매우 순차적이므로 나는 PlusCal을 쓰겠다. 나중에 버퍼 없는 채널에서 임피던스 불일치가 조금 생기겠지만, 전체적으로는 이득이다.
Chris의 코드 예시에는 “복잡한 부분”이 세 가지 있다: go, defer, 그리고 Go 채널의 성질이다. defer는 고루틴 실행이 끝났을 때 정리 코드를 실행한다. 일단은 지연된 코드를 별도의 레이블(label)로 옮기는 식으로 표현하겠지만, 더 정확하게 하려면 PlusCal 프로시저(procedure)를 쓸 수도 있다. go는 새 고루틴을 띄운다. PlusCal에서는 모든 프로세스(process)를 미리 정의해야 하므로, 새 고루틴을 “띄울” 수는 없다. 대신 각 프로세스를 정의해 두되 실행되지 못하게 막을 수 있다. 그런 다음, 행동(behavior)에서 그 고루틴이 이미 초기화됐는지 아닌지를 나타내는 플래그를 추가한다. 대략 이런 모양이 된다:
variables
initialized = [w \in Routines |-> FALSE];
\* ...
process goroutine \in Routines
begin
Work:
await initialized[self];
\* ...
즉 각 고루틴은 무언가를 하기 전에 메인 프로세스가 자신을 초기화해 주기를 기다린다(awaits). 이렇게 해서 새 프로세스를 띄우는 것을 흉내 낼 수 있다.
이제 채널이 남았는데, 명세하기 가장 복잡한 부분이다. Go 채널에는 두 종류가 있다: 버퍼 있는(buffered) 채널과 버퍼 없는(unbuffered) 채널이다. 버퍼 있는 채널로의 송신은 채널이 가득 차 있으면 블록된다. 버퍼 있는 채널에서의 수신은 채널이 비어 있으면 블록된다. 둘 다 PlusCal 매크로(macro)로 표현할 수 있다:
macro send_buffered(chan) begin
await channels[chan] < buffered[chan];
channels[chan] := channels[chan] + 1;
end macro;
macro receive_buffered(chan) begin
await channels[chan] > 0;
channels[chan] := channels[chan] - 1;
end macro;
버퍼 있는 채널은 이걸로 해결된다. 반면 버퍼 없는 채널은 송신자와 수신자가 둘 다 있지 않으면 항상 블록된다. 순수 TLA+라면 명세하기가 그리 까다롭지 않겠지만, PlusCal은 행동의 각 스텝(step)이 프로세스 하나가 한 가지 일을 하는 것이라고 가정한다. 한 프로세스가 “먼저” 블록되게 해야 하므로, 버퍼 없는 채널은 성가신 장부 관리를 좀 추가하지 않고는 PlusCal에서 자연스럽게 표현할 수 없다. 이를 위해 프로시저를 쓸 수 있다.
자, 대략적인 접근법과 골치 아플 만한 지점을 알았으니 스펙을 작성해 보자.
스펙
먼저 부분별로 뜯어보고, 그다음 전체 스펙을 보자.
---- MODULE channels ----
EXTENDS Integers, TLC, Sequences
CONSTANTS NumRoutines, NumTokens
Routines == 1..NumRoutines
(* --algorithm channels
variables
channels = [tokens |-> 0, found |-> {}];
buffered = [tokens |-> NumTokens];
initialized = [w \in Routines |-> FALSE];
channels는 각 채널의 현재 내용물이다. 버퍼 있는 채널은 내용물을 숫자 하나로 취급하고, 최대 용량은 별도의 buffered 변수에 저장한다. 버퍼 없는 채널은 대신 수신자를 기다리는 송신자들의 집합(set)을 저장한다. initialized는 고루틴을 흉내 내기 위한 것이다.
macro go(routine) begin
initialized[routine] := TRUE;
end macro
Go 문법에 더 가깝게 맞추려고 추가한 매크로다.
macro write_buffered(chan) begin
await channels[chan] < buffered[chan];
channels[chan] := channels[chan] + 1;
end macro;
macro receive_channel(chan) begin
if chan \in DOMAIN buffered then
await channels[chan] > 0;
channels[chan] := channels[chan] - 1;
else
await channels[chan] # {};
with w \in channels[chan] do
channels[chan] := channels[chan] \ {w}
end with;
end if;
end macro;
버퍼 있는 채널과 버퍼 없는 채널을 모두 처리하므로 예전의 read_buffered와는 달라졌다. 버퍼 있는 채널은 예상대로 동작한다. 버퍼 없는 채널의 경우, 블록된 쓰기 쪽(writer)들의 집합이 비지 않을 때까지 기다렸다가, 그중 하나에서 읽었다고 비결정적으로(nondeterministically) 선언한다.1
procedure write_unbuffered(chan) begin
DeclareSend:
channels[chan] := channels[chan] \union {self};
Send:
await self \notin channels[chan];
return;
end procedure
버퍼 없는 채널을 모델링하려면 상태를 송신자 쪽에 두거나 수신자 쪽에 둘 수 있다. Go는 버퍼 없는 채널 여러 개에서 한꺼번에 읽는 것을 허용하기 때문에, 나는 송신자 쪽에 두기로 했다.2 시간상 분리된 두 스텝에 걸쳐 1) 프로세스를 채널 송신자 집합에 추가하고 2) 수신자가 그 집합에서 자신을 제거해 주기를 기다린다.
process goroutine \in Routines
begin
A:
await initialized[self];
call write_unbuffered("found");
B:
receive_channel("tokens");
end process;
goroutine 프로세스는 Go 코드를 있는 그대로 옮긴 것이다. 먼저 고루틴이 초기화되기를 기다리는데, 10번 줄에 해당한다. 그다음 found 채널에 쓴다(13번 줄). 더 충실하게 하려 했다면 defer 전용 의미론을 작성했겠지만, 여기서는 프로세스 끝의 레이블에 붙여 두는 것으로 만족한다.
process main = 0
variables i = 1;
begin
Main:
while i <= NumRoutines do
write_buffered("tokens");
go(i);
i := i + 1;
end while;
Get:
while i > 1 do
i := i - 1;
receive_channel("found");
end while;
end process;
end algorithm; *)
우리 에뮬레이션은 고루틴 하나를 초기화할 때마다 토큰을 하나씩 쓴다. write_channel에는 await가 들어 있으므로, 토큰보다 고루틴이 많으면 블록된다. 그러고 나면 어떤 고루틴이 토큰을 반납할 때까지 계속 블록된 채로 있다.3 최종 스펙은 다음과 같다:
---- MODULE channels ----
EXTENDS Integers, TLC, Sequences
CONSTANTS NumRoutines, NumTokens
Routines == 1..NumRoutines
(* --algorithm channels
variables
channels = [limitCh |-> 0, found |-> {}];
buffered = [limitCh |-> NumTokens];
initialized = [w \in Routines |-> FALSE];
macro send_buffered(chan) begin
await channels[chan] < buffered[chan];
channels[chan] := channels[chan] + 1;
end macro;
macro receive_channel(chan) begin
if chan \in DOMAIN buffered then
await channels[chan] > 0;
channels[chan] := channels[chan] - 1;
else
await channels[chan] # {};
with w \in channels[chan] do
channels[chan] := channels[chan] \ {w}
end with;
end if;
end macro;
macro go(routine) begin
initialized[routine] := TRUE;
end macro
procedure send_unbuffered(chan) begin
DeclareSend:
channels[chan] := channels[chan] \union {self};
Send:
await self \notin channels[chan];
return;
end procedure
process goroutine \in Routines
begin
A:
await initialized[self];
call send_unbuffered("found");
B:
receive_channel("limitCh");
end process;
process main = 0
variables i = 1;
begin
Main:
while i <= NumRoutines do
send_buffered("limitCh");
go(i);
i := i + 1;
end while;
Get:
while i > 1 do
i := i - 1;
receive_channel("found");
end while;
end process;
end algorithm; *)
====
이제 전체 스펙이 있으니, 모델 체커(model checker)인 TLC로 스펙이 어떤 속성을 만족하는지 볼 수 있다. 속성은 하나도 명시하지 않았지만, TLC는 기본적으로 데드락을 검사한다.
데드락 찾기
데드락을 일으키려고 NumRoutines <- 3, NumTokens <- 2로 검사했다. {{TODO state space}}. 놀랍지도 않게, 데드락이 난다:5
State 1: <Initial predicate>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 0, found |-> {}]
/\ i = 1
/\ pc = (0 :> "Main" @@ 1 :> "A" @@ 2 :> "A" @@ 3 :> "A")
/\ initialized = <<FALSE, FALSE, FALSE>>
State 2: <Main line 128, col 9 to line 137, col 48 of module base>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 1, found |-> {}]
/\ i = 2
/\ pc = (0 :> "Main" @@ 1 :> "A" @@ 2 :> "A" @@ 3 :> "A")
/\ initialized = <<TRUE, FALSE, FALSE>>
State 3: <Main line 128, col 9 to line 137, col 48 of module base>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 2, found |-> {}]
/\ i = 3
/\ pc = (0 :> "Main" @@ 1 :> "A" @@ 2 :> "A" @@ 3 :> "A")
/\ initialized = <<TRUE, TRUE, FALSE>>
State 4: <A line 106, col 12 to line 114, col 64 of module base>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 2, found |-> {}]
/\ i = 3
/\ pc = (0 :> "Main" @@ 1 :> "A" @@ 2 :> "DeclareSend" @@ 3 :> "A")
/\ initialized = <<TRUE, TRUE, FALSE>>
State 5: <A line 106, col 12 to line 114, col 64 of module base>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 2, found |-> {}]
/\ i = 3
/\ pc = (0 :> "Main" @@ 1 :> "DeclareSend" @@ 2 :> "DeclareSend" @@ 3 :> "A")
/\ initialized = <<TRUE, TRUE, FALSE>>
State 6: <DeclareSend line 92, col 22 to line 95, col 77 of module base>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 2, found |-> {1}]
/\ i = 3
/\ pc = (0 :> "Main" @@ 1 :> "Send" @@ 2 :> "DeclareSend" @@ 3 :> "A")
/\ initialized = <<TRUE, TRUE, FALSE>>
State 7: <DeclareSend line 92, col 22 to line 95, col 77 of module base>
/\ buffered = [limitCh |-> 2]
/\ channels = [limitCh |-> 2, found |-> {1, 2}]
/\ i = 3
/\ pc = (0 :> "Main" @@ 1 :> "Send" @@ 2 :> "Send" @@ 3 :> "A")
/\ initialized = <<TRUE, TRUE, FALSE>>
Chris가 겪은 것과 같은 문제다. 고루틴은 found 채널에 수신자가 있어야만 토큰을 반납할 수 있는데, 그 채널의 유일한 수신자는 main이고, main은 모든 고루틴을 초기화한 뒤에야 읽으며, 토큰보다 고루틴이 많으면 main은 블록된다. 모든 고루틴이 초기화되기 전에는 고루틴들이 토큰을 반납할 수 없고, 일부 고루틴이 토큰을 반납하기 전에는 main이 모든 고루틴을 초기화할 수 없다.
고치기
Chris는 이를 고칠 수 있는 방법 세 가지를 제안한다. 스펙을 수정해서 셋을 하나씩 테스트해 볼 수 있다:
메인 for 루프가 하는 대신 고루틴들이
limitCh로 송신해서 토큰을 가져갔다면 버그는 없었을 것이다;
process goroutine \in Routines
begin
A:
await initialized[self];
+ write_buffered("limitCh");
\* ...
while i <= NumRoutines do
- write_buffered("limitCh");
initialized[i] := TRUE;
i := i + 1;
end while;
이것은 모델 체킹을 통과한다.
고루틴들이
found로 송신하기 전에limitCh에서 수신해서 토큰을 반납했다면 버그는 없었을 것이다(다만 에러 처리 때문에, 수신은 defer에서 하는 편이 더 간단하고 믿을 만하다).
process goroutine \in Routines
begin
A:
await initialized[self];
+ receive_channel("limitCh");
- call write_unbuffered("found");
B:
- receive_channel("limitCh");
+ call write_unbuffered("found");
end process;
이것은 모델 체킹을 통과한다.
그리고 for 루프 전체가 별도의 고루틴 안에 있었다면…
이건 조금 더 복잡하다. 루프를 위한 새 프로세스를 만들고, 그 식별자를 initialized에 추가한다. for 루프를 나타내는 데는 -1을 쓰겠다.
initialized = [w \in Routines \union {-1} |-> FALSE];
\* After goroutines
process for_loop = -1
variables i = 1;
begin
Loop:
while i <= NumRoutines do
write_buffered("limitCh");
go(i);
i := i + 1;
end while;
end process;
그런 다음 main이 루프를 직접 도는 대신 이 프로세스를 초기화하도록 수정한다:
process main = 0
variables i = NumRoutines;
begin
Main:
go(-1);
Get:
while i > 0 do
i := i - 1;
receive_channel("found");
end while;
end process;
이것은 모델 체킹을 통과한다.
논의
결국 Go 코드 20줄을 테스트하려고 명세를 75줄쯤 썼다. 스펙의 절반 이상은 채널 로직인데, 이제 다른 스펙에서 재사용할 수 있다. 그 부분을 빼면 격차가 조금 줄어드는데, 물론 실제 TLA+ 스펙이라면 온전성 검사용 속성을 훨씬 더 많이 작성할 테니 훨씬 길어질 것임은 인정한다. 그렇더라도 TLA+ 버전을 작성하는 데 원래 버전을 작성하는 것보다 수고가 크게 더 들지는 않을 것이고, 프로덕션 전에 데드락을 잡아낸다면 결과적으로 시간을 아껴 줄 수 있다.
- 1
with는 집합이 비어 있으면 블록되므로, 그 위의await문은 사실 불필요하다. 순전히 명확성을 위해 넣었다.- 2
select로 여러 채널에 송신할 수도 있지만, 그건 덜 흔하지 않나 싶다. 바로 이런 데서 날것의 TLA+ 액션(action)을 직접 쓸 수 있으면 정말 도움이 된다.- 3
Get은range안의 채널 수신이 동작하는 방식을 부정확하게 표현한 것이다: 원래는 채널이 닫힐 때까지 루프를 돌아야 한다. 스펙의 나머지 부분이 채널 닫기에 의존하지 않고, 이 예제에 복잡도를 더 얹고 싶지 않아서 여기서는 뺐다.- 5
트레이스를 조금 더 알아보기 쉽게 하려고
stack과chan변수를 뺐다.