aboutsummaryrefslogtreecommitdiffstats
path: root/docs/design
diff options
context:
space:
mode:
Diffstat (limited to 'docs/design')
-rw-r--r--docs/design/029-past-one-node.md33
-rw-r--r--docs/design/030-one-path.md83
2 files changed, 115 insertions, 1 deletions
diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md
index 286485e..bcede34 100644
--- a/docs/design/029-past-one-node.md
+++ b/docs/design/029-past-one-node.md
@@ -320,10 +320,41 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절�
4. **증명 = 제로카피 실행 허가.** 손으로 쓴 판은 패킷과 리프를 그 자리에서 읽고, 경계 검사와 예산은 지킨다. 증명이 준 것은 N1, N2,
N4이고, 트리의 순서로 찾기에는 "정렬됨"이 하나 더 든다(키를 선언한 리스트면 저장소의 불변식이라 증명이 필요 없다).
-**다음 질문(지은 것이 아니다).** "리프가 곧 커밋이다". 바뀐 리프의 열 바이트가 커밋 구간이 되어 로그의 레코드를 대신하고, 필드가 여럿인
+**다음 질문(지은 것이 아니다; 아래 047에서 깨는 실험을 했다).** "리프가 곧 커밋이다". 바뀐 리프의 열 바이트가 커밋 구간이 되어 로그의 레코드를 대신하고, 필드가 여럿인
메시지는 열 순서로 오면, 패킷, 리프, 디스크, 복제가 한 모양이 된다. 재지 않은 값이 있다. append 하나에 리프 하나(32 × 8 = 256 B)를 다시
쓰는 것과 로그 레코드 64 B의 차이, 스냅숏 공유와 압축에 주는 영향이다. 이 원리를 세울지는 깨는 실험을 정하고 나서 정한다.
+## 리프가 곧 커밋인가(047, 2026-10-19)
+
+009의 "한 모양"을 원리로 세울지 깨는 실험을 했다. 주장은 이것이다. 바뀐 리프의 열 바이트가 커밋 구간이 되어 로그와 이미지를 대신하고,
+메시지의 행도 리프로 오면, 패킷, 메모리, 디스크, 복제가 한 모양이 된다. 막대와, 그것이 무엇을 뜻하는지를 돌리기 전에 적고 커밋했다
+(`a93891e`).
+- 기준선(`baseline.py`). 046의 shim과 저널로, 오늘의 저장소가 메시지 하나에 쓰는 리스트 바이트(로그와 이미지)를 커밋 하나에
+ 메시지 1, 16, 256개씩 묶어 쟀다.
+- 모형(`model.py`). 메모리의 바이트 그대로(리프 296–1,320 B, 안쪽 노드 680 B) 커밋이 바뀐 리프를 쓴다고 보고 바이트를 센다. 저장소를
+ 지은 것은 아니다.
+ - cow: 바뀐 리프와 그 위 경로를 새로 쓴다.
+ - tail: 끝에 덧붙이기는 셀만 마지막 리프의 빈칸에 그 자리에서 쓴다. 쥔 스냅숏은 제 커밋의 개수 너머를 읽지 않는다.
+ - inplace: 다른 바뀜도 그 자리에서 쓴다. 허용되지 않는 길이고, 왜 안 되는지 보이려고 셌다.
+ - 압축은 트리의 규칙대로 셌다.
+| 리스트 바이트/메시지, 커밋 하나에 1 / 16 / 256 | 오늘 | cow | tail | 막대 |
+|---|---|---|---|---|
+| entries(덧붙이기) | 65.5 / 15.7 / 12.4 | 1,636 / 102 / 14.5 | **25.9 / 10.9 / 10.0** | ≤ 오늘 |
+| 은행 이체(흩어진 갱신 셋과 덧붙이기 하나) | 122 / 35.6 / 30.1 | 7,428 / 2,098 / 996 | **4,826 / 1,975 / 992** | ≤ 오늘의 2배 |
+- **덧붙이기는 지나고, 흩어진 갱신은 깨진다.** 미리 적은 대로, "한 단위"는 문구대로는 틀렸다. 덧붙이기와 한꺼번에 싣기에는 리프가
+ 단위다. 흩어진 바뀜에는 델타 꼴이 필요하고, 그것이 로그다. 정직한 설계는 단위 둘이다. 덧붙이기는 리프의 꼬리에 쓰고, 흩어진 갱신은
+ 로그에 쓴다.
+- inplace는 바이트로는 지나지만(186 / 126 / 122), 쥔 스냅숏이 그 쓰기를 93만 / 54만 / 1만 번 본다. 쓰기와 커밋 사이에서 죽으면 옛 값도
+ 잃는다. cow, tail, 아래의 delta에서는 스냅숏이 보는 쓰기가 0이다.
+- 돌린 뒤의 후보(막대 밖). 리프 뒤에 바뀜을 담을 방(델타 16 B씩)을 두고, 방이 차면 리프를 새로 쓰는 것(delta)이다. 방 8칸에서 739 /
+ 545 / 292, 32칸에서 363 / 268 / 176, 128칸에서 249 / 161 / 136으로 모두 막대를 넘는다. 오늘의 로그는 바뀜 하나를 약 7.5 B에 담기 때문이다.
+ 자리는 varint, 정수는 zigzag로 줄이고, 틀은 커밋에 하나다.
+- **패킷을 리프로(`packet.c`).** 오늘 `pure_list_read`는 UAX #14의 load 행(필드 여섯, 2,787행)을 행 하나에 기계 명령 1,318(사이클 372)로
+ 푼다. 32행의 열 덩어리로 오면 검사하고 그 자리에서 받는 데 44.4(사이클 14.2)다. 막대(1/10 이하)를 지나고, 모든 칸이 같다. 이것은
+ 메시지 형식을 바꾸는 일이다(행 대신 32행의 열 덩어리).
+- 009로 다시 보면, 항목의 셀은 패킷, 리프, 디스크의 리프 꼬리, 복제에서 한 모양(binary64)을 지킬 수 있다. 흩어진 바뀜만 다른 그릇(델타)에
+ 담긴다. 로그도 정수가 아닌 값은 binary64를 그대로 담는다.
+
## 열린 질문: 스키마의 진화
같은 항목을 두 모양으로 든다. 지금은 레코드의 모양이 바뀌면 목록을 새 모양으로 다시 써서(100만 항목에 172 ms 막음) 그동안 옛
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의 마감 선언.