diff options
Diffstat (limited to 'docs/design')
| -rw-r--r-- | docs/design/029-past-one-node.md | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/docs/design/029-past-one-node.md b/docs/design/029-past-one-node.md index 668471c..d4eb13c 100644 --- a/docs/design/029-past-one-node.md +++ b/docs/design/029-past-one-node.md @@ -274,6 +274,50 @@ C의 속도로 컴파일하기 쉬운 쪽**이어야 한다. 61–183배의 절� **미룬 것.** 둘이 동시에 주인이 되지 않게, 어느 노드가 파일을 주인으로 열지 정하는 합의의 규칙이 필요하다. 여기서 설계하지 않는다. 실험이 지난 뒤의 다음 결정이다. +## 바깥 피드백 009의 기준으로: 같은 데이터, 한 바이트 모양 + +009의 철칙은 "같은 데이터가 두 가지 바이트 모양을 갖는 순간 실패"다. 패킷, 실행 메모리, 디스크의 리프와 커밋 구간, 복제가 한 표현이어야 +한다. 원리 1의 손으로 쓴 점과 원리 2의 결과를 그 기준으로 다시 쟀다(2026-10-19, 045 `app.c`의 leaves 단들, 046의 저널). + +1. **패킷 바이트 = 실행 입력(역직렬화 0): 손으로 쓴 테두리에서는 지난다. 런타임에서는 아니다.** + - 손으로 쓴 테두리는 메시지의 행을 페이로드가 둔 그 자리에서 읽는다. 역직렬화도 복사도 0이다(테두리 1,595 → 22). 필드 하나인 + 레코드(`Point { code }`)라서 페이로드의 행이 바이트 그대로 실행 배열이다. 남은 것은 검사다(행이 온전한지, 수마다 유한한지). + 바깥에서 온 바이트는 어떤 증명도 덮지 못한다. + - 런타임은 메시지마다 `pure_list_read`로 행을 트리로 다시 짓는다. + - 재지 않은 것: `pure-serve`에서 링크의 레코드를 호스트의 버퍼로 옮기는 복사. +2. **디스크 열 B+트리 리프 = 실행 배열(복사 0): 트리의 순서로 찾을 때만 값이 없다.** + - 앞의 stored_flat은 `ranges`를 트리 밖 배열로 복사했다. 009가 금하는 것이라 사다리에서 뺐고 비교로만 남긴다. + - 복사 없이 트리가 둔 자리에서 읽으면 이렇다(기계 명령/점). + | 단 | 기계 명령 | 그 위의 shared | + |---|---|---| + | stored_flat(복사, 금지) | 6,136 | 564 | + | 리프를 `pure_list_run`으로 | 7,931 | 2,114 | + | 리프를 트리의 꼴대로 바로 | 7,135 | 1,576 | + | 트리의 순서로 찾기 | 6,137 | 578 | + - 위치로 반씩 나누는 탐색은 탐침마다 트리를 내려간다(탐침 하나에 약 78). 트리의 순서로 찾으면 그것이 사라진다. 안쪽 노드마다 자식을 + 그 첫 항목의 start로 고르고(리프를 그 자리에서 읽는다), 리프 안에서 반씩 나눈다. 그러면 복사판과 2.5% 안이다(사이클은 24% 더). + 끝에서 끝으로는 602, 같은 페이로드를 받는 Vega의 2.5배다. + - 그러려면 `ranges`가 start로 정렬되어 있어야 한다. 데이터는 그렇고, start를 키로 선언한 리스트와 그 seek라면 저장소가 그것을 지킨다. + 앱이 손으로 쓴 이분 탐색은 트리가 이미 든 색인을 다시 짓는 것이다. 이것도 겹친 계층이다. +3. **커밋 구간 = 복제 레코드 = 팔로워 바이트: 파일로는 지난다(046). 그 파일이 리프와 다른 모양이다.** + - 046에서 따르는 노드의 파일은 바이트까지 같고, 실은 것은 저장소의 제 연산이다. + - 하지만 항목 하나의 모양을 세어 보면 하나가 아니다(`entries`, 메시지 5000의 n = 0.25). + - 패킷: binary64 LE `000000000000d03f`. + - TREE 리프의 열: 같은 8바이트. 필드 하나이므로 열이 곧 행이다. + - 이미지(체크포인트): binary64를 이어 붙인 것. 필드 하나일 때는 리프의 열과 같은 바이트다. + - 로그: 메시지 하나에 64 B를 쓴다. 값의 8바이트에 56 B의 틀이 붙는다(순번, 앞 순번, 크기, 개수, 16 B 다이제스트, 리스트 이름, 길이, + 종류, varint 자리, 꼬리표). + - 그래서 009의 "한 모양"은 오늘 세 곳에서 깨진다. + - 로그. 리프와 다음 이미지가 들 바뀜을 다시 틀에 담는다. 로그는 이미지를 커밋마다 다시 쓰지 않으려고 있다. + - 필드가 여럿인 레코드. 패킷과 이미지는 행 순서이고(`encode_cell`을 항목마다), 리프는 열 순서다. + - 사건의 리스트(FLAT). 담은 것에 맞춰 폭을 u8/u32로 좁힌다. +4. **증명 = 제로카피 실행 허가.** 손으로 쓴 판은 패킷과 리프를 그 자리에서 읽고, 경계 검사와 예산은 지킨다. 증명이 준 것은 N1, N2, + N4이고, 트리의 순서로 찾기에는 "정렬됨"이 하나 더 든다(키를 선언한 리스트면 저장소의 불변식이라 증명이 필요 없다). + +**다음 질문(지은 것이 아니다).** "리프가 곧 커밋이다". 바뀐 리프의 열 바이트가 커밋 구간이 되어 로그의 레코드를 대신하고, 필드가 여럿인 +메시지는 열 순서로 오면, 패킷, 리프, 디스크, 복제가 한 모양이 된다. 재지 않은 값이 있다. append 하나에 리프 하나(32 × 8 = 256 B)를 다시 +쓰는 것과 로그 레코드 64 B의 차이, 스냅숏 공유와 압축에 주는 영향이다. 이 원리를 세울지는 깨는 실험을 정하고 나서 정한다. + ## 열린 질문: 스키마의 진화 같은 항목을 두 모양으로 든다. 지금은 레코드의 모양이 바뀌면 목록을 새 모양으로 다시 써서(100만 항목에 172 ms 막음) 그동안 옛 |