diff options
Diffstat (limited to 'docs/design/030-one-path.md')
| -rw-r--r-- | docs/design/030-one-path.md | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/docs/design/030-one-path.md b/docs/design/030-one-path.md new file mode 100644 index 0000000..a9856a3 --- /dev/null +++ b/docs/design/030-one-path.md @@ -0,0 +1,83 @@ +# 030 — 한 실행 경로: 증명이 표현을 고르고, 같은 데이터는 한 모양으로 + +작성일: 2026-10-19. 상태: **설계 확정, 단 하나는 사용자의 결정**(아래 "정할 것"). 코드는 아직 없다. 근거는 029의 원리 1 결과, 045, +046, 047이다. 바깥 피드백 008(실행기 분열 금지)과 009(같은 데이터는 한 바이트 모양)를 따른다. + +## 쉬운 말로 + +UAX #14의 메시지 하나는 오늘 코드 포인트당 기계 명령 40,365개가 든다. 같은 앱을 손으로 바꿔 써서 잰 경로는 813개다. 그 경로에서는 +트리 밖 복사도 역직렬화도 하지 않고, 앱은 aup가 오늘 받는 그대로(키 있는 리스트와 seek)다. 그래서 Vega의 C(같은 페이로드에 +251)의 3.2배이고, 사이클로는 3.7배다(348 대 93). 이 문서는 그 경로를 런타임의 단 하나의 실행 경로로 만드는 설계다. + +## 경로 + +메시지 → 테두리 → 내보낸 처리기 → 커밋 → 복제, 보기. 단계마다 무엇을 하고, 무엇이 그것을 허락하고, 무엇으로 쟀는지 적는다. + +| 단계 | 하는 일 | 허락하는 것 | 잰 것 | +|---|---|---|---| +| 테두리 | 행을 페이로드가 둔 자리에서 읽는다. 검사만 한다(행이 온전한지, 수가 유한한지, 불이 0이나 1인지). 처리기가 바꾸는 상태 하나만 따로 쓰고, 오류 없이 끝나면 그것으로 바꾼다 | 언어의 뜻(입력은 바뀌지 않는다), N2 | 1,595 → 22/점(045). 여러 필드 행은 32행 열 덩어리로 오면 1,318 → 44/행(047) | +| 처리기 | 지역과 스택은 레지스터에 둔다. 부름은 맨 부름이다. 사건의 리스트는 타입 있는 버퍼다. 레코드에 담은 리스트는 복사하지 않고 함께 쓴다. 정수는 정수로 다룬다 | 오늘의 증명(스택 모양, fn마다의 집합), N1, N4, 표현의 결정 | 38,623 → 564–788/점(045) | +| 저장 리스트 읽기 | 메모리의 리프(binary64 열)를 그 자리에서 읽는다. 키로 찾을 때는 안쪽 노드의 키로 내려가 리프의 키 열에서 찾는다. 사건 안에서는 리프를 쥐고 있는다 | N2(사건 안에서 바뀌지 않음), 키 있는 리스트의 선언 | keyed_shared 788, 끝에서 끝 813, 사이클 348(045) | +| 커밋 | 덧붙이기는 마지막 리프의 빈칸에 셀만 그 자리에서 쓰고, 개수는 커밋 레코드에 둔다. 흩어진 갱신은 오늘의 로그 레코드로 쓴다 | 쥔 스냅숏은 제 개수 너머를 읽지 않는다 | 덧붙이기 리스트 바이트 25.9 / 10.9 / 10.0(오늘 65.5 / 15.7 / 12.4), 갱신은 로그 그대로(047) | +| 복제 | 저장소가 제 sync에서 끊은 제 파일 연산을 pure link로 보낸다. 확인은 heard다 | 원리 2 | 바이트 같음, kill -9 90번, 접두 867곳(046) | +| 보기 | 리프를 그 자리에서 읽는다(오늘의 스냅숏이 하는 대로) | 090의 O(1) 스냅숏 | — | + +지우는 것. +- 실행 경로로서의 실행기, 묶음 실행기의 레인(`module-batch.c`), AArch64 기계어 계층(`module-jit.c`). 실행기는 참조로만 남아, 검사가 두 + 경로의 답을 견준다. +- 메시지마다 행을 트리로 다시 짓는 `pure_list_read`. +- 사건마다 상태 54개를 다섯 번 훑기. N2가 바뀌는 것만 알려 준다. +- 뜨거운 길의 범용 리스트 API(폭 고르기, `list_held`, PureCell 바꿈). 참조 경로에는 남는다. +- 통째로만 바뀌는 bytes 상태의 조각 트리. + +## 검증기가 더할 사실 + +오늘 증명하는 것은 스택의 높이와 타입, 반복의 상한, fn마다의 등록기·리스트·바꾸는 집합, 리스트 사이에 별칭이 없음이다. 여기에 더할 +것은 셋이다. 검증기가 스스로 알아낸다. aup가 말한 것을 믿지 않는다. +- **N1 정수임.** `number` 자리(지역, 매개변수, 결과, 리스트의 열)가 정수만 갖는지, 0 이상인지. 0, `.count`, 정수끼리의 `+ - *`, 0 이상 + 정수끼리의 `//`와 `%`, 정수 열에서 읽은 값에서 퍼진다. 처리기에서 1.10배, 정수 버퍼의 전제다. +- **N4 담은 뒤 바뀌지 않음.** `LIST_VALUE` 뒤에 그 리스트도 레코드의 리스트도 바뀌지 않는다. 1.23배다. aup는 담은 뒤 바꾸는 것을 + 허락하므로 지점마다 증명해야 한다. +- **N2 처리기의 변경 집합.** fn에 하는 분석을 처리기로 넓힌다. 테두리의 상태 하나와, 사건 안에서 리프를 쥐는 것을 허락한다. + +경계 안임(N5)은 더하지 않는다. 경계 검사는 남기고, 그 값은 1.12배다. + +## 표현의 결정(증명이 필요 없는 것) + +- 사건의 리스트: 타입 있는 버퍼다(수는 binary64, 정수 열은 N1이면 i64, 불은 u8). 키 없고 인덱스 없는 리스트가 받는 연산을 모두 한다. + 9.43배다. +- 입력의 행: 페이로드 그 자리에서 읽는다. 필드가 하나인 레코드는 행이 곧 열이다. 필드가 여럿인 메시지는 32행의 열 덩어리(메모리 리프의 + 열)로 바꾼다. 메시지 형식을 바꾸는 일이고, 1.0 전이라 깰 수 있다. +- 통째로 바뀌는 bytes 상태: 버퍼 둘을 번갈아 쓴다. +- 메모리 셈: 꼴과 상관없이 정의한다(셀 8바이트, 텍스트는 그 바이트). 지금은 폭으로 압축한 꼴에 따라 정해진다. 계약의 결정이다. +- 앱의 관용구: 정렬된 데이터를 찾는 일은 키 있는 리스트와 seek(`first(x in L where x.key >= v)`)로 쓴다. 손으로 쓴 이분 탐색은 트리가 + 이미 가진 색인을 다시 짓는다. aup의 걸림이 하나 있다. fn 안의 접기가 fn의 매개변수를 읽지 못해서, seek를 처리기에 써야 했다. + 매개변수는 접기 동안 정해진 값이니 받아들이는 것이 맞다(aup의 일). + +## 정할 것(사용자의 결정) + +내보낸 처리기를 제품에서 무엇이 기계어로 바꾸는가. +- **(가) 설치할 때 시스템 C 컴파일러.** 호스트가 검증한 모듈을 C로 옮기고, `cc`로 지어 모듈의 다이제스트로 캐시한다. 잰 것은 이것이다 + (손으로 쓴 C, gcc -O2). `cc`가 런타임의 의존이 된다. 재지 않은 것: 모듈 하나를 짓는 시간(140의 앱 200–2,000줄; Pi에서 몇 초로 본다), + `cc`가 없는 호스트(그때는 실행기, 참조 경로). +- **(나) Pure 자신의 내보내기, 명령어 집합마다.** AArch64부터 시작한다. 의존이 없고 짓는 시간이 짧다. 029는 명령어 집합마다의 뒤끝을 두지 + 않으려 했고, 그것을 피하던 길(이어 붙이기)은 죽었다. 재지 않은 것: 전부다. +- aup가 미리 기계어를 내보내는 길은 없다. 검증기는 바이트코드를 증명하고, 실행되는 코드는 그 증명에서 나와야 한다. + +## 짓는 차례와 차례마다의 깨는 확인 + +1. **표현 먼저, 실행기 안에서.** 입력 행을 그 자리에서 읽기, 사건 리스트를 타입 있는 버퍼로, 리프를 쥐고 읽기, 상태 훑기를 N2로 줄이기. + 내보내기 없이도 140의 모든 명세가 빨라져야 한다. 확인: 140의 검사가 모두 지나고(답이 같다), 041의 셈, 은행 1%, TPC-C 3%를 지킨다. + 이 단계로 얼마나 주는지는 재지 않았다. 먼저 잴 것이다. +2. **검증기의 N1, N2, N4.** 확인: 140의 모듈에서 각 사실이 몇 자리에 서는지 센다. 변이 시험으로, 사실을 거짓으로 세우는 모듈을 + 검증기가 거부하는지 본다. +3. **내보내기((가) 또는 (나)).** 확인: 140의 모든 명세를 두 경로로 돌려 답을 견준다. 041과 은행, TPC-C의 관문을 지킨다. +4. **저장소의 리프 꼬리.** 덧붙이기는 리프에, 흩어진 갱신은 로그에 쓴다(047). 확인: 046의 같음, 이어받기, 찢긴 꼬리를 그대로 다시 돌리고, + 047의 바이트를 실제 저장소에서 다시 잰다. +5. **메시지 형식.** 필드 여럿인 행을 32행 열 덩어리로 보낸다. 확인: 047의 `packet.c`를 실제 테두리에서 다시 잰다. + +## 하지 않는 것 + +- 흩어진 갱신을 리프로 쓰는 것. 047에서 16–55배였다. +- 트리 밖에 열을 복사해 두는 것(009). 045의 stored_flat은 비교로만 남는다. +- 1.0의 마감 선언. |