diff options
| author | eunhhu <[email protected]> | 2026-10-19 14:48:47 +0100 |
|---|---|---|
| committer | eunhhu <[email protected]> | 2026-10-19 14:48:47 +0100 |
| commit | 0f8c2ec7f98ed34f5567a168147737442d93f9fc (patch) | |
| tree | c8939c89820af22696e5aaede7ab6067f453a7bc /docs | |
| parent | 415bc5af13f6658ac44a0d135bb0f290191a44f6 (diff) | |
| download | pure-0f8c2ec7f98ed34f5567a168147737442d93f9fc.tar.gz pure-0f8c2ec7f98ed34f5567a168147737442d93f9fc.zip | |
029, 030: 047 written into 029 (the leaf as the commit: appends pass, sparse updates break, two units as said beforehand; packets as 32-row column chunks 1,318 to 44 a row); 030 the one execution path, settled but for one choice: border reading rows where the payload has them, the handler emitted with registers, typed event buffers, shared captures and whole numbers, stored lists read in their leaves (a keyed seek by the guides' keys: 813 a point end to end, cycles 348, nothing copied out), commits writing appends into the leaf's tail and sparse updates to the log, replication as 046; what goes (the executor as a path, the batch lanes, the AArch64 layer, pure_list_read each message, the 54-state walks, the generic list API on hot paths, the bytes piece tree for whole sets); the verifier's three facts (N1, N4 new; N2 widened); representation choices; the user's choice (system cc at install, or Pure's own emitter per instruction set); the order, representation first inside the executor, each step with its check
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/design/029-past-one-node.md | 33 | ||||
| -rw-r--r-- | docs/design/030-one-path.md | 83 |
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의 마감 선언. |
