1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
# 114 — 다른 기계에서: x86_64의 WSL2와 M3의 macOS
2026-10-01–02. Pure와 aup를 Pi 밖의 두 기계에서 빌드하고, 검사하고, 같은 입력에 같은 것을 내는지 견준다. 완료 조건은 아니다
(검증 기기는 Pi다). Pure가 약속한 "같은 앱과 같은 입력이면 어느 기기에서나 같은 사건이 같은 이유로 거절된다"(017의 원칙)를 Pi 한
대로만 확인해 왔기 때문에 한 번 본다.
| | Pi(기준) | WSL2 | Mac |
|---|---|---|---|
| CPU, 아키텍처 | Cortex-A76, AArch64 | i5-12400F, x86_64 | Apple M3, arm64 |
| OS | Linux 6.18(Debian) | Ubuntu 24.04, Linux 6.18(WSL2) | macOS 27.0.1 |
| 페이지 | 16 KiB | 4 KiB | 16 KiB |
| 컴파일러 | gcc 14.2 | gcc 13.3(`_FORTIFY_SOURCE` 기본) | Apple clang 21 |
| OpenSSL, Node | 3.5.7, 24.21.0 | 같은 판을 사용자 공간에(시스템의 3.0은 HPKE가 없다) | 3.6.4(Homebrew), 26.9 |
## 쉬운 말로
- **같은 입력에 같은 것을 낸다.** aup의 검사가 돌리는 `pure-run` 1,053번(모듈 667개)의 출력, 오류, 종료 코드가 세 기계에서 모두
같다. 같은 사건으로 만든 저장소는 세 기계에서 파일까지 바이트 하나 다르지 않다. 한 기계에서 만든 저장소를 다른 기계가 열고
이어 쓴 결과도 같다.
- **다른 컴파일러가 버그 하나를 찾았다.** 목록의 칸을 읽는 함수가 인자 둘을 한 호출에 넘겼는데, 하나가 다른 하나를 채우는 함수의
호출이었다. C는 인자를 읽는 순서를 정하지 않는다. Pi의 gcc 14는 우연히 채우는 쪽을 먼저 불렀고, x86_64의 gcc 13은 "채워지기 전에
읽힐 수 있다"고 멈췄다(`418cd21`).
- **macOS에서 다시 빌드된다.** 코어와 저장소, 그 테스트가 clang에서 막혀 있었다. 그 판의 C17에 맞지 않는 열거값, 쓰이지 않던
변수, 문자열에 정수를 더하는 꼴 같은 것들이었다. 고친 뒤 Mac에서 코어와 저장소의 테스트가 모두 지난다(`17c5dc1`). 호스트
(`pure-serve`)는 리눅스의 것이다(epoll, recvmmsg, UDP GSO).
- **WSL2의 벽시계는 뛴다.** 약 32초마다 2초쯤 뒤로 간다. 타이머 검사가 20번에 1–3번 실패했다. 실패마다 그 창 안에 시계의 뜀이
있었다. 벽시계와 단조 시계가 어긋난 창은 다시 재게 했다(`a904a8f`). Pure의 대기와 타이머는 단조 시계로 세므로 Pure의 문제는
아니다(`server_clocks`가 이미 본다).
- **Pi가 두 번 멈췄다. 측정 도구 탓이다.** 저장소를 만드는 도구가 `pure-run`의 출력을 메모리에 모았다. 출력은 사건마다 상태 전체라
사건 수의 제곱으로 자란다(목록 사건 2만 개면 13 GB). 8 GiB에 OOM 데몬이 없는 Pi는 죽이기 전에 모든 프로그램의 코드를 내보내고
응답을 멈췄다. 출력을 흘려 요약하게 고쳤다(최고 56 MiB). 실험을 메모리 한도 아래에서 돌리는 `research/guard.py`도 두었다
(`a300512`).
## 결과
원시 결과와 명령은 [029-across-machines](../../research/experiments/029-across-machines/)에 있다(`runs.sh`의 단계 `ship`,
`setup`, `record`, `checks`, `units`, `clock`, `stores`, `compare`).
**빌드와 검사.**
| | WSL2 | Mac |
|---|---|---|
| Pure 전부(`make`) | 통과(`418cd21` 뒤) | 코어, 저장소, `pure-run`(`17c5dc1` 뒤). `pure-serve`와 링크는 리눅스의 것 |
| 코어·저장소의 테스트(ASAN 포함) | 통과 | 통과(ASAN은 돌리지 않았다) |
| 링크·JSON의 테스트 | 통과 | — |
| Pure의 `tests/check.py`(검사 36개) | 36개 모두(하나씩, `each_check.py`, 112초) | — |
| aup의 검사 | 통과 | 통과 |
| Vega | 돌리지 않았다(FreeType, HarfBuzz, EGL의 개발 패키지가 시스템에 없다) | 돌리지 않았다 |
Pi에서도 같은 것을 clang 19로 빌드했다. Pure 전부, 프로토타입, aup, Vega가 경고 없이 빌드되고 코어와 저장소의 테스트가 지난다.
gcc 14에 `-D_FORTIFY_SOURCE=3`을 주면 WSL2에서 본 프로토타입의 오류(`write`의 결과를 버림)가 Pi에서도 난다(`be9f474`).
Mac의 기본 SDK(27.0)는 링커(ld-1267)가 모르는 아키텍처(`arm64e.x1`)를 적고 있어 아무것도 링크되지 않았다. `runs.sh`는 링크되는
가장 새 SDK(26.5)를 고른다. 그 Mac의 도구 사이의 어긋남이고 Pure와 상관없다.
**같은 입력, 같은 출력**(`record`, `compare`). aup의 검사를 돌리며 `pure-run`을 감싼 `recorded-pure-run`이 실행마다 모듈의 해시,
인자, 입력, 출력, 오류, 종료 코드를 적는다(임시 디렉터리의 경로는 지운다). aup의 검사는 무작위 프로그램 600개, 대조 실행,
저장소를 오가는 재시작, 텍스트 모델 등을 시드로 만든다.
| 비교 | 실행 | 모듈 | 같음 |
|---|---:|---:|---:|
| Pi 대 Pi(두 번) | 1,053 | 667 | 1,053 |
| Pi 대 WSL2 | 1,053 | 667 | 1,053 |
| Pi 대 Mac | 1,053 | 667 | 1,053 |
aup의 검사가 내는 요약(29개 항목)도 세 기계에서 같다. 컴파일러가 만든 모듈도 같다(실행의 열쇠에 모듈의 해시가 들어 있다).
**저장소**(`stores`, Pi와 Mac은 2026-10-02, WSL2는 10-04). aup의 예제 `tasks.aup`(목록)와 `notes.aup`(텍스트)를 트리 저장소 위에서 시드의 사건으로 돌린다
(목록 2,000개, 텍스트 4,000개, 64개마다 저장). 저장소의 형식은 페이지 크기와 상관없다(제자리로 읽을 때의 매핑에만 쓴다). 그래서
16 KiB 페이지 여럿에 걸치는 이 크기로 충분하다.
| | tasks | notes |
|---|---|---|
| 저장소 | 8,659,104 B, 파일 6개 | 468,180 B, 파일 4개 |
| Pi, Mac, WSL2의 파일 | 바이트까지 같다 | 바이트까지 같다 |
| 스냅숏 2,000개 / 4,000개 | 같다 | 같다 |
그다음 각 기계가 다른 기계의 저장소를 복사해 열고, 보이기, 사건 300개, 보이기를 한다. 만든 기계와 연 기계의 짝 일곱(Pi와
Mac 사이의 넷, Pi와 WSL2 사이의 셋)의 스냅숏 302개가 모두 같다. Mac과 WSL2 사이는 따로 하지 않았다. 두 기계의 저장소가 Pi의
것과 바이트까지 같기 때문이다.
**WSL2의 시계**(`clock.py`: 20 ms마다 벽시계와 단조 시계를 읽어, 어긋남이 20 ms를 넘는 걸음을 적는다).
| | 잰 시간 | 뜀 | 벽시계 − 단조 시계 |
|---|---:|---:|---:|
| Pi | 120 s | 0 | 0.0 ms |
| WSL2 | 180 s | 10 | −7,235 ms |
| WSL2(타이머 검사 동안) | 150 s | 4 | −7,986 ms |
WSL2는 약 32.5초마다 벽시계를 1.2–2.2초 뒤로 놓는다(처음에는 ±1.6–1.9초의 쌍도 있었다). 게스트의 시계가 호스트보다 4–5% 빨리
가는 것을 시간 동기화가 계단으로 되돌리는 모습이다. `server_timers`는 앱이 본 시각을 요청 전후의 벽시계와 견준다. 0.6초의 창에
뜀이 들면 실패한다.
| 타이머 검사 20번 | 지남 | 실패 | 실패한 창에 뜀 | 다시 잰 창 |
|---|---:|---:|---:|---:|
| 고치기 전, 첫 번째 | 19 | 1 | 1 | — |
| 고치기 전, 두 번째 | 17 | 3 | 3 | — |
| 고친 뒤(`a904a8f`) | 20 | 0 | — | 3(뜀이 든 셋) |
**Pi가 멈춘 일.** 첫 `stores.py`는 목록 사건 2만 개, 텍스트 사건 6만 개를 `capture_output`으로 돌렸다. 작은 크기로 재면 출력은
목록 사건 250, 500, 1,000개에 2.1, 8.4, 33 MB, 텍스트 사건에 0.18, 0.60, 2.1 MB다. 제곱으로 자라니 2만 개와 6만 개는 13 GB와
7.7 GB다. Pi는 8 GiB, 스왑은 zram 2 GiB, OOM 데몬이 없고, 사용자의 systemd에는 메모리 컨트롤러가 없다(`MemoryMax`가 무시된다).
저널도 휘발성이라 앞 부팅의 기록이 남지 않는다. 지금은 출력을 흘리며 해시하고 첫 줄과 마지막 8 MiB만 쥔다. 사건 수도 줄였다.
`guard.py`는 명령을 제 세션에서 돌리고, 세션의 상주 메모리가 `--most`(3,072 MiB)를 넘거나 기계의 가용 메모리가 `--floor`
(1,024 MiB)보다 적어지면 세션을 통째로 죽인다(tmpfs에 쓴 것도 가용 메모리에서 빠진다). 0.25초마다 본다. 손자 프로세스가 커지는
경우, 남겨진 프로세스, 종료 코드를 확인했다.
## 판정
- **Pure의 실행은 기계를 타지 않는다.** 아키텍처(AArch64, x86_64), 페이지(16, 4 KiB), 컴파일러(gcc 13·14, clang 21), OS(Linux,
macOS)가 달라도 같은 모듈, 같은 입력이면 같은 출력, 같은 실패, 같은 저장소 바이트다. 이번에 본 범위는 `pure-run`이 닿는
곳(코어, 실행, 저장소)이다. 호스트와 링크는 리눅스에서만 봤다(Pi와 WSL2).
- 고친 것 넷은 모두 Pi에서는 드러나지 않던 것이다. 하나(목록 칸의 인자 순서)는 다른 컴파일러에서 틀린 값을 읽을 수 있는
코드였다.
## 다음
- 검사에 clang 빌드를 더할지. Pi에 clang 19가 있다. `make CC=clang-19`가 지나게 됐으니, 이것이 다시 깨지지 않게 하는 데는 그
한 줄이면 된다. 검사 시간이 늘어나는 것과 견준다.
- macOS의 호스트. 보내는 루프는 `link/sending.c` 한 파일(kqueue)이지만, 받기(recvmmsg, GRO)와 보내기(GSO)는 대체가 필요하다.
필요가 생길 때 한다.
|