From 8071832bc7857634f66c94592b27b188c882ea54 Mon Sep 17 00:00:00 2001 From: eunhhu Date: Mon, 19 Oct 2026 05:54:45 +0100 Subject: 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 --- docs/research/140-spec-suite.md | 60 ++++++++- .../experiments/044-specs/2026-10-19-rto.jsonl | 1 + research/experiments/044-specs/rto.py | 40 ++++++ research/experiments/044-specs/rto_check.py | 145 +++++++++++++++++++++ tests/check.py | 28 +++- tests/specs/rto/README.md | 7 + tests/specs/rto/scenarios.json | 1 + 7 files changed, 280 insertions(+), 2 deletions(-) create mode 100644 research/experiments/044-specs/2026-10-19-rto.jsonl create mode 100644 research/experiments/044-specs/rto.py create mode 100644 research/experiments/044-specs/rto_check.py create mode 100644 tests/specs/rto/README.md create mode 100644 tests/specs/rto/scenarios.json 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). 위 표의 여덟 후보 가운데 무엇을 어떤 모양으로 받을지 정한다. diff --git a/research/experiments/044-specs/2026-10-19-rto.jsonl b/research/experiments/044-specs/2026-10-19-rto.jsonl new file mode 100644 index 0000000..71d73d7 --- /dev/null +++ b/research/experiments/044-specs/2026-10-19-rto.jsonl @@ -0,0 +1 @@ +{"scenarios": 20, "events": 241612, "timeouts": 156, "right": {"batches": 241612, "rounds": 241612, "all": 241612}, "paths_same": true, "costs": {"10": {"ticks": 218070, "timeouts": 78, "ticks_a_timeout": 2795.8, "late_mean_ms": 4.27, "late_most_ms": 9.875}, "100": {"ticks": 21968, "timeouts": 78, "ticks_a_timeout": 281.6, "late_mean_ms": 49.23, "late_most_ms": 99.0}}, "aup_lines": 56, "aup_brace_lines": 11, "python_lines": 30} diff --git a/research/experiments/044-specs/rto.py b/research/experiments/044-specs/rto.py new file mode 100644 index 0000000..e4a4a57 --- /dev/null +++ b/research/experiments/044-specs/rto.py @@ -0,0 +1,40 @@ +# RFC 6298's retransmission timer in plain Python: the reference 140 counts aup's lines against. A sender's segments +# are sent and acknowledged (cumulatively) at given times; the round-trip time of each acknowledged segment that was +# never sent again (Karn) updates SRTT, RTTVAR and RTO (2.2-2.5: 1 s at least, 60 s at most), and the timer runs as +# 5.1-5.6 say: started when one is sent and none runs, stopped when all are acknowledged, restarted when new data is, +# and on expiry the earliest is sent again and RTO doubles. The timer is seen at ticks of period P, as an app sees time. +LOWEST, HIGHEST = 1000, 60000 # milliseconds; the clock's granularity G is the tick's period + + +class Sender: + def __init__(self, period): + self.period, self.srtt, self.rttvar, self.rto, self.measured = period, 0.0, 0.0, 1000.0, False + self.deadline, self.outstanding, self.retransmits = -1.0, [], [] # outstanding: [seq, sent, again] + + def send(self, now, seq): + self.outstanding.append([seq, now, False]) + if self.deadline < 0: + self.deadline = now + self.rto # 5.1 + + def ack(self, now, seq): + acked = [s for s in self.outstanding if s[0] <= seq] + if not acked: + return + self.outstanding = [s for s in self.outstanding if s[0] > seq] + last = acked[-1] + if not last[2]: # Karn: no sample from a segment sent again + r = now - last[1] + if not self.measured: + self.srtt, self.rttvar, self.measured = r, r / 2, True # 2.2 + else: + self.rttvar = 0.75 * self.rttvar + 0.25 * abs(self.srtt - r) # 2.3 + self.srtt = 0.875 * self.srtt + 0.125 * r + self.rto = min(max(self.srtt + max(self.period, 4 * self.rttvar), LOWEST), HIGHEST) # 2.4, 2.5 + self.deadline = now + self.rto if self.outstanding else -1.0 # 5.3, 5.2 + + def tick(self, now): + if self.deadline >= 0 and now >= self.deadline: # 5.4-5.6 + self.outstanding[0][2] = True + self.retransmits.append((self.outstanding[0][0], now)) + self.rto = min(self.rto * 2, HIGHEST) + self.deadline = now + self.rto diff --git a/research/experiments/044-specs/rto_check.py b/research/experiments/044-specs/rto_check.py new file mode 100644 index 0000000..be41ffb --- /dev/null +++ b/research/experiments/044-specs/rto_check.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +"""Research 140: RFC 6298's retransmission timer written in aup (aup's examples/rto.aup), with periodic ticks. + +Each scenario (a seed and a tick period P) is made closed-loop by rto.py's model and a receiver: segments sent at random +gaps, each arriving half a random round trip later unless its first sending is lost (one in five), the receiver +acknowledging cumulatively all it holds without a gap, the acknowledgement arriving after the other half; a segment the +timer sends again arrives. The events (sends, acknowledgements, ticks every P ms) are then given to the app +through pure-run (time MS before each), on Pure's three paths: after every event its SRTT, RTTVAR, RTO, deadline, the +segments outstanding and the retransmissions must be the model's, the paths the same. No known implementation is +compared: the oracle is the model of the same rules. What the ticks cost is measured: ticks a timeout (a one-shot timer +would be one event), and how late a timeout is seen (below P). Then counts lines of rto.aup and of rto.py's model. One +JSON line.""" +import json, os, random, struct, subprocess, sys, tempfile + +here = os.path.dirname(os.path.abspath(__file__)) +pure = os.path.normpath(os.path.join(here, '../../..')) +aup = os.environ.get('AUP', os.path.join(pure, '..', 'aup')) +sys.path.insert(0, here) +import rto # noqa: E402 + +START = 1_000_000 # the first event's time (ms since 1970, as now is) + + +def lines(path, stop=None): + code = braces = 0 + for line in open(path): + if stop and line.startswith(stop): break + text = line.strip() + if not text or text.startswith('#'): continue + code += 1 + braces += text == '}' + return code, braces + + +def scenario(seed, period, segments=40): + """The events the app is given (time, kind, seq), the model's state after each, and the timeouts' lateness. The + network: a sending arrives half a random round trip later unless it is lost (a first sending, one in five), and the + receiver acknowledges at once, cumulatively, all it holds without a gap; the acknowledgement arrives after the other + half.""" + chooser = random.Random(seed) + sender = rto.Sender(period) + pending, t = [], START + period # (time, order, kind, seq): arrivals, then acknowledgements, sends, then ticks + for seq in range(1, segments + 1): + t += chooser.choice([0, 0, 5, 40, 120, 300, 900]) + pending.append((t, 2, 'transmit', seq)) + held, through = set(), 0 # the receiver's segments, and the last one it holds every one up to + + def sent(time, seq, first): + if not first or chooser.random() > 0.2: + half = chooser.randrange(20, 350) + pending.append((time + half, 0, 'arrive', seq * 1000 + half)) + + events, states, late = [], [], [] + tick = START + while pending or sender.outstanding: + pending.sort() + if pending and pending[0][0] < tick + period: # the host ticks every P, the timer running or not + time, _, kind, seq = pending.pop(0) + else: + time, kind, seq = tick + period, 'tick', 0 + tick = time + if kind == 'arrive': # the receiver's: not the app's + seq, half = divmod(seq, 1000) + held.add(seq) + while through + 1 in held: + through += 1 + if through: + pending.append((time + half, 1, 'ack', through)) + continue + if kind == 'transmit': + sender.send(time, seq) + sent(time, seq, True) + elif kind == 'ack': + sender.ack(time, seq) + else: + before, deadline = len(sender.retransmits), sender.deadline + sender.tick(time) + if len(sender.retransmits) > before: + late.append(time - deadline) + sent(time, sender.retransmits[-1][0], False) + events.append((time, kind, seq)) + states.append((sender.srtt, sender.rttvar, sender.rto, sender.deadline, len(sender.outstanding), len(sender.retransmits))) + if len(events) > 200000: + raise RuntimeError('a scenario without end') + return events, states, late + + +def run(module, events, env, work): + commands = os.path.join(work, 'rto.commands') + with open(commands, 'w') as f: + for time, kind, seq in events: + f.write(f'time {time}\n') + f.write('tick tick\n' if kind == 'tick' else f"message {kind} {struct.pack(' 1 else 10 + with tempfile.TemporaryDirectory() as work: + source = open(os.path.join(aup, 'examples', 'rto.aup')).read() + for period in (10, 100): + module = os.path.join(work, f'rto-{period}.pmod') # its tick and its G the scenario's period + with open(os.path.join(work, f'rto-{period}.aup'), 'w') as f: + f.write(source.replace('every 10 ms', f'every {period} ms').replace('fn PERIOD = 10 ', f'fn PERIOD = {period} ')) + subprocess.run([os.path.join(aup, 'build', 'aup'), 'build', os.path.join(work, f'rto-{period}.aup'), '-o', module], check=True) + ticks = timeouts = 0 + lateness = [] + for seed in range(seeds): + events, states, late = scenario(seed, period) + outputs = {} + for name, env in (('batches', {'PURE_JIT': '0'}), ('rounds', {'PURE_JIT': '0', 'PURE_BATCH': '0'}), + ('all', {'PURE_JIT': 'all'})): + got = run(module, events, env, work) + want = [('none',) + s for s in states] + report['right'][name] = report['right'].get(name, 0) + sum(g == w for g, w in zip(got, want)) + outputs[name] = got + report['paths_same'] = report['paths_same'] and outputs['rounds'] == outputs['batches'] == outputs['all'] + report['scenarios'] += 1 + report['events'] += len(events) + ticks += sum(kind == 'tick' for _, kind, _ in events) + timeouts += len(late) + lateness += late + report['timeouts'] += timeouts + costs[period] = {'ticks': ticks, 'timeouts': timeouts, 'ticks_a_timeout': round(ticks / max(timeouts, 1), 1), + 'late_mean_ms': round(sum(lateness) / max(len(lateness), 1), 2), 'late_most_ms': max(lateness, default=0)} + report['costs'] = costs + aup_code, aup_braces = lines(os.path.join(aup, 'examples', 'rto.aup')) + python_code, _ = lines(os.path.join(here, 'rto.py')) + report.update({'aup_lines': aup_code, 'aup_brace_lines': aup_braces, 'python_lines': python_code}) + ok = all(n == report['events'] for n in report['right'].values()) and report['paths_same'] + print(json.dumps(report)) + sys.exit(0 if ok else 1) diff --git a/tests/check.py b/tests/check.py index 7a5f50e..5574b80 100644 --- a/tests/check.py +++ b/tests/check.py @@ -1736,7 +1736,9 @@ def module_specs(aup, pure, work): written back by its view to the same records, cut ones refused; HTTP/1.1 request streams (tests/specs/http) read by its examples/http.aup a packet at a time, cut anywhere, to the same requests; line breaking (UAX #14) by its - examples/linebreak.aup on LineBreakTest.txt's lines (tests/specs/linebreak).""" + examples/linebreak.aup on LineBreakTest.txt's lines (tests/specs/linebreak); + RFC 6298's retransmission timer by its examples/rto.aup on a scenario's + events (tests/specs/rto), the model's state after each.""" import hashlib import os import random @@ -1962,6 +1964,30 @@ def module_specs(aup, pure, work): state = json.loads(line) assert state['fault'] == 'none' and [b != 0 for b in bytes.fromhex(state['views']['boundaries'])] == want, codes runs['linebreak'] = {'lines': len(lines), 'code_points': sum(len(c) for c, _ in lines)} + # RFC 6298's retransmission timer (its examples/rto.aup, ticked): a scenario's sends, acknowledgements and ticks + # (tests/specs/rto, at periods of 10 and 100 ms), after each the model's SRTT, RTTVAR, RTO, deadline and counts. + source, events = (EXAMPLES / 'rto.aup').read_text(), 0 + for scenario in json.loads((pure / 'tests/specs/rto/scenarios.json').read_text()): + period = scenario['period'] + (work / 'rto.aup').write_text(source.replace('every 10 ms', f'every {period} ms').replace('fn PERIOD = 10 ', f'fn PERIOD = {period} ')) + program = work / 'rto.pmod' + compile_module(aup, work / 'rto.aup', program) + given = ''.join(f'time {t}\n' + ('tick tick\n' if kind == 'tick' else f"message {kind} {struct.pack('