diff options
| author | eunhhu <[email protected]> | 2026-10-19 05:54:45 +0100 |
|---|---|---|
| committer | eunhhu <[email protected]> | 2026-10-19 05:54:45 +0100 |
| commit | 8071832bc7857634f66c94592b27b188c882ea54 (patch) | |
| tree | 42779a2fe127f0147980f3ac03de9ca0d4dc33a3 /docs | |
| parent | 475f35cb45a77dc41029126370887fd33b332800 (diff) | |
| download | pure-8071832bc7857634f66c94592b27b188c882ea54.tar.gz pure-8071832bc7857634f66c94592b27b188c882ea54.zip | |
140's 10, RFC 6298's retransmission timer, written in aup with no new opcode (aup's examples/rto.aup, the timer a deadline in the state seen at each periodic tick): 20 scenarios (10 seeds, ticks every 10 and 100 ms; a closed loop: first sendings lost one in five, the receiver acknowledging cumulatively) and their 241,612 events right against rto.py, the model of the same rules (no known implementation takes given events), on the three paths, the paths the same; module_specs in make check: one scenario at both periods (tests/specs/rto, 2,297 events); bars: one workaround (the periodic tick: 2,795.8 ticks a timeout at 10 ms, 281.6 at 100, seen 4.27 and 49.23 ms late on average; ticks 93% and 57% of the counted work), 56 lines against Python's 30, three frictions (an input's period not readable, no abs, send a keyword); the one-shot timer's shape as a decision point, one spec needing it: noted, not made; the suite table's row 10
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/research/140-spec-suite.md | 60 |
1 files changed, 59 insertions, 1 deletions
diff --git a/docs/research/140-spec-suite.md b/docs/research/140-spec-suite.md index 4a8d9f8..1da8f4b 100644 --- a/docs/research/140-spec-suite.md +++ b/docs/research/140-spec-suite.md @@ -56,7 +56,7 @@ | 7 | 텍스트 편집 | UI 개념 | text, 커서 | 편집기의 참조 모델 대조(aup `make check`) | 된다 | 된다 | | 8 | 상자 배치(flex 같은) | UI 개념 | 중첩, 재귀 | 기존 배치 구현(Yoga, Taffy)의 결과와 대조 | 못 쓴다(중첩, 재귀) | 중첩과 재귀는 핸들러에서 된다. 보기에서 재귀 fn을 부르지 못한다(탐침). 쓰지 않음 | | 9 | HTTP/1.1 요청을 패킷마다(RFC 9112) | 스트림의 상태 기계 | 바이트, 이벤트를 넘는 상태 | 경계를 아무 데서나 자른 요청 모음 | 못 쓴다(바이트). 지금은 `serve/`의 C다 | 썼다: 스트림 200개를 어디서 잘라도 h11과 같다. 우회 하나(리스트 값의 대입), 줄 1.9배, C의 83배(아래) | -| 10 | 재시도, 물러서기, 시간 제한 | 시간 | 시각, 한 번의 타이머 | 시각을 준 시뮬레이션 | 우회(주기 틱 `every`와 `now`) | 다시 보지 않음 | +| 10 | 재시도, 물러서기, 시간 제한 | 시간 | 시각, 한 번의 타이머 | 시각을 준 시뮬레이션 | 우회(주기 틱 `every`와 `now`) | 썼다(RFC 6298): 사건 241,612개가 같은 규칙의 모델과 같다. 우회 하나(주기 틱: 10 ms면 타임아웃 하나에 틱 2,796개), 줄 1.9배(아래) | | 11 | X25519, ChaCha20-Poly1305 | 상수 시간 암호 | 데이터에 따라 달라지지 않는 시간 | RFC 7748, RFC 8439의 벡터 | aup 밖(설계상, 아래) | 그대로(설계상 aup 밖) | **11은 핵의 원시 연산으로 둔다(가설).** 실행기의 시간은 데이터에 따라 달라진다. 묶음 실행기도 결함이 나면 묶음을 처음부터 실행기로 @@ -784,6 +784,64 @@ 자기에게 메시지를 걸어 두는 단발 타이머는 핵의 원시(호스트의 일정, 저장, 재생의 결정성)이고, 명세 하나(10)가 닿는다. 쌓임을 막는 규칙대로 적어 두고 만들지 않는다. +## 묶음의 10: 재시도 타이머 (RFC 6298, 2026-10-19) + +보내는 쪽의 재전송 타이머를 썼다(aup의 `examples/rto.aup`). 새 명령도 코어의 C도 없다. +- **규칙.** 확인된 세그먼트 가운데 다시 보낸 적 없는 것의 왕복 시간(Karn)으로 SRTT, RTTVAR, RTO를 고친다(2.2–2.5: 1초 이상, 60초 + 이하). 타이머는 5.1–5.6대로 돈다. 보낼 때 돌지 않으면 걸고, 다 확인되면 멈추고, 새 데이터가 확인되면 다시 건다. 만료하면 가장 이른 + 것을 다시 보내고(앱은 다시 보냄을 기록한다) RTO를 두 배로 한다. +- **시간.** 타이머는 상태의 마감(`deadline`)이다. 앱은 주기 틱(`input tick = every 10 ms`)마다 `now`와 견준다. 140이 처음 적은 + 우회 그대로다. 시계의 단위 G는 틱의 주기다. +- **알려진 구현은 대조하지 않았다.** 운영체제의 TCP는 사건을 줄 수 없다. 오라클은 같은 규칙의 파이썬 모델(`rto.py`)이다. + `rto_check.py`가 닫힌 고리의 망을 만든다: 세그먼트를 무작위 간격으로 보내고, 처음 보낸 것은 다섯에 하나를 잃는다. 받는 쪽은 틈 + 없이 가진 데까지 곧바로 누적 확인하고, 확인은 왕복의 나머지 반 뒤에 닿는다. 다시 보낸 것은 닿는다. 사건마다 시각을 준다(pure-run의 + `time MS`). + +**맞음.** +- 시드 10개 × 주기 둘(10, 100 ms) = 시나리오 20개, 사건 241,612개(타임아웃 156번). 사건마다 SRTT, RTTVAR, RTO, 마감, 남은 세그먼트, + 다시 보냄의 수가 모델과 같다. 세 실행 길에서 모두 맞고, 세 길이 같다. +- Pure의 `make check`(`module_specs`)에 들어갔다. 시나리오 하나(시드 2, 세그먼트 20, 타임아웃 다섯)를 주기 둘로 `tests/specs/rto`에 + 두었다(사건 2,297개). RTO를 세 배로 하는 앱은 그 검사에서 떨어진다. + +**막대.** + +| 막대 | 잰 것 | | +|---|---|---| +| 쓸 수 있다 | aup와 Pure만. 새 명령 없음 | 지남 | +| 우회가 없다 | 주기 틱으로 마감을 본다(아래) | **우회 하나** | +| 줄 수 ≤ 파이썬 참조 | aup 56줄(닫는 괄호만인 줄 11) 대 파이썬 30줄 | **못 미침**(1.9배) | +| C 대비 시간 | 시간의 일이 아니다. 셈한 명령으로 적는다: 쉬는 틱 25, 보냄 12, 확인 112–247(평균 193) | 기록(막대 없음) | +| 견고하다 | 위의 맞음, 세 길이 같음. 세 기계는 아직 | 일부 | + +**틱의 값.** 주기 틱은 타이머가 돌지 않을 때도 사건이다. + +| 주기 | 틱 | 타임아웃 하나에 틱 | 만료를 본 늦음(평균, 최대) | 검사 시나리오에서 틱이 쓴 명령 | +|---|---|---|---|---| +| 10 ms | 218,070 | 2,795.8 | 4.27 ms, 9.875 ms | 54,201 가운데 50,300(93%) | +| 100 ms | 21,968 | 281.6 | 49.23 ms, 99.0 ms | 9,106 가운데 5,175(57%) | + +- 주기를 줄이면 늦음은 준다. 대신 틱이 그만큼 는다. 늦음은 주기 아래이고, 틱의 수는 주기에 반비례한다. 둘을 같이 줄이는 주기는 없다. +- `serve`는 때가 된 틱을 돌린 뒤 저장한다(`run_timers`). 쉬는 틱도 사건이므로, 저장과 재생의 기록도 틱만큼 는다. +- 쉬는 틱과 만료한 틱이 같은 25다. 셈은 블록을 쓴 대로 센다(`charge`). 갈래가 어느 쪽으로 가든 같다. + +**마찰 셋.** +1. 앱이 자기 입력의 주기를 읽지 못한다. G(2.4의 `max(G, 4·RTTVAR)`)가 틱의 주기인데, `every 10 ms`와 `fn PERIOD = 10`에 두 번 쓴다. +2. `abs`가 없다. `|SRTT − R|`을 `max(srtt - r, r - srtt)`로 썼다. +3. `send`는 출력의 낱말이라 입력의 이름으로 쓸 수 없다(`transmit`으로 썼다). + +**줄을 길게 한 것.** 56 대 30이다. 닫는 괄호의 줄을 빼면 45다. +- 레코드 둘(`Segment`, `Retransmit`)이 9줄이다. 파이썬은 리스트와 튜플이다. +- 상태와 입력의 선언이 10줄이다. 파이썬은 생성자의 두 줄이다. +- 확인된 것을 고르는 고리가 6줄이다. 파이썬은 리스트 내포 두 줄이다(`[s for s in … if s[0] <= seq]`). + +**결정점: 단발 타이머.** 주기 틱을 걷어 낼 꼴은 이렇다. +- 앱이 "T에 깨워라"를 건다. 상태의 마감을 호스트가 읽는 꼴이 될 수도, 효과(`after`, `at`)가 될 수도 있다. +- 호스트는 그 시각을 저장소에 두고, T가 되면 핸들러를 `now = T`(또는 그 뒤)로 한 번 돌린다. 저장하고, 재생에서 같은 차례로 돈다. +- 그러면 쉬는 틱(10 ms면 타임아웃 하나에 2,796개)이 없어지고, 만료를 늦음 없이 본다. +- 그러나 지금 그것이 필요한 명세는 이것 하나다. 140의 규칙(핵은 두 명세가 필요로 하는 것만 받는다)대로 적어 두고 만들지 않는다. 두 + 번째 후보: HTTP의 유휴 연결 시간 제한, DNS 질의의 재시도. 둘 다 아직 묶음의 명세가 다루지 않는다. +- 원본: `rto.py`(모델), `rto_check.py`(맞음, 틱의 값, 줄 수), `2026-10-19-rto.jsonl`. + ## 착수 기준 (다음 일) - **바꿀 결정.** 계산의 핵을 설계한다(027). 위 표의 여덟 후보 가운데 무엇을 어떤 모양으로 받을지 정한다. |
