Skip to content

Commit a2ccf6b

Browse files
committed
restoreLive 실행 경계 계약을 기계 강제로 (외부 리뷰 최우선 지적 수용)
- Runtime.execSeq 상태 변이 카운터(run/runAsync/setGlobal/install/loadPackages)로 경계 위반을 O(1) 감지. restoreLive가 위반 시 자동으로 재해시 경로 승격 = 조용히 틀린 복원 불가능. 실측: 위반 27.4ms 안전 복원, 준수 0.69ms 즉시 경로(rehashed 플래그). - probe를 가드 검증형으로 갱신(자동 감지 + 즉시 경로 보존), 게이트 20검사 green. - restore()의 힙 성장 비대칭 관찰(리뷰 부수 지적)을 계약 실태 표 열린 항목으로 등록. - README/소비 계약/타입(RestoreInfo.rehashed) 동기화.
1 parent c0e7570 commit a2ccf6b

10 files changed

Lines changed: 49 additions & 28 deletions

File tree

README.ko.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ reactive.restoreLive(cp.index, sp0); // 라이브-차분 복원(바뀐
103103
console.log(rt.run("x")); // 1
104104
```
105105

106-
**실행 경계 계약**: `restoreLive`저장된 해시끼리만 비교한다(재해싱 0 = 즉시성의 근거). 그래서 파이썬을 실행했다면 복원 전에 반드시 `checkpoint()`로 경계를 닫아야 한다. 경계를 보장할 수 없으면 `restore()`(전체 복원, 안전 기준선)를 쓴다.
106+
**실행 경계 계약(기계 강제)**: `restoreLive`경계(마지막 `checkpoint()`/복원 이후 실행 없음)를 지키면 저장 해시 비교만으로 즉시 복원한다(재해싱 0, 실측 ~1ms). 경계 위반(실행·예외·전역 변이)은 상태 변이 카운터로 O(1) 자동 감지되어 재해시 경로로 승격되므로 **조용히 틀린 복원은 일어나지 않는다**(실측 ~27ms). 어느 경로였는지는 반환값 `rehashed`로 확인한다.
107107

108108
### 빌린 시스템콜 브리지
109109

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ reactive.restoreLive(cp.index, sp0); // live-diff restore (writes only
103103
console.log(rt.run("x")); // 1
104104
```
105105

106-
**Execution boundary contract**: `restoreLive` compares stored hashes only (zero re-hashing is what makes it instant). So if you ran Python, you must close that boundary with `checkpoint()` before restoring. If you cannot guarantee the boundary, use `restore()` (full restore, the safe baseline).
106+
**Execution boundary contract (machine-enforced)**: when the boundary holds (no execution since the last `checkpoint()`/restore), `restoreLive` compares stored hashes only and restores instantly (zero re-hashing, ~1ms measured). A boundary violation (execution, exception, global mutation) is auto-detected in O(1) via a state-mutation counter and the restore upgrades to the re-hash path, so **a silently wrong restore cannot happen** (~27ms measured). The returned `rehashed` flag tells you which path ran.
107107

108108
### Borrowed syscall bridge
109109

docs/consuming/contract.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ subpath export: `pyproc/runtime`, `pyproc/reactive`, `pyproc/syscall-bridge`, `p
3333

3434
- 타입은 동봉된 `index.d.ts`가 계약이다.
3535
- 엔진 내부(`HEAPU8`, `Runtime.raw` 등)를 직접 만지지 않는다. `raw`는 탈출구이고 계약 밖이다.
36-
- **restoreLive 실행 경계 계약**: 파이썬을 실행했다면 복원 전에 `checkpoint()`로 경계를 닫는다. 전제를 보장할 수 없으면 `restore()`(전체 복원)를 쓴다.
36+
- **restoreLive 실행 경계 계약(기계 강제)**: 경계를 지키면 즉시 복원(재해싱 0), 위반은 자동 감지되어 재해시 경로로 승격된다(조용한 오염 없음). 반환값 `rehashed`로 경로 확인. 즉시성이 필요하면 복원 전 `checkpoint()`로 경계를 닫아라.
3737

3838
## 방향과 경계
3939

index.d.ts

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ export interface CheckpointInfo {
2222
export interface RestoreInfo {
2323
pagesWritten: number;
2424
mbWritten: number;
25+
/** 이번 복원이 재해시 경로였는지. 경계 위반이 자동 감지되면 true. */
26+
rehashed: boolean;
2527
}
2628

2729
export interface SyscallBridgeConfig {
@@ -73,7 +75,7 @@ export class MemoryCapability {
7375
export class ReactiveController {
7476
checkpoint(): CheckpointInfo;
7577
restore(j: number, savedSP: number | null): void;
76-
/** opts.rehash: 실행 경계 계약이 깨졌을 수 있으면(예외로 더러워진 힙) 현재 힙을 재해시해 비교. */
78+
/** 경계 위반(마지막 checkpoint/restore 이후 실행·변이)은 자동 감지되어 재해시 경로로 복원된다. opts.rehash는 강제 재해시. */
7779
restoreLive(j: number, savedSP: number | null, opts?: { rehash?: boolean }): RestoreInfo;
7880
timeTravel(j: number, savedSP: number | null, opts?: { rehash?: boolean }): RestoreInfo;
7981
stackSave(): number | null;

mainPlan/web-python-runtime/01-architecture.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,12 @@ pyproc의 코어는 새 이론이 아니라 codaro `tests/_attempts`에서 브
4444

4545
| 항목 | 계약 | 실제 | 상태 |
4646
|---|---|---|---|
47-
| restoreLive 실행 경계 | 복원 전 마지막 실행을 `checkpoint()`로 닫아야 한다(재해싱 0이 즉시성의 근거) | 계약을 어기면 stale 해시 비교로 0페이지 복원(조용한 오동작). 코드 주석·README 사용례로 계약 명문화 + 브라우저 게이트가 계약 준수 경로를 기계 검증(2026-07-11, restoreLive 0.84ms 실측) | 문서 + 게이트로 고정. 위반 감지 가드는 attempts 후보 |
47+
| restoreLive 실행 경계 | 경계 준수 시 즉시(재해싱 0), 위반 시에도 조용한 오염 없음 | **기계 강제(2026-07-11)**: Runtime.execSeq(상태 변이 카운터)로 위반을 O(1) 감지해 자동 재해시 승격. 반환값 `rehashed`로 경로 확인, 게이트 상시 검증 | 해소 (외부 리뷰 지적 반영) |
4848
| 페이지 해시 soundness | 실질적 sound(누락 확률 무시 가능) | 이중 32비트(실효 64비트, ~2^-64)로 승격. 비용 1.54배, 30MB 힙 14.3ms 실측 | 해소 (attempts/reactiveSoundness 졸업, 2026-07-11) |
4949
| syscallBridge | input/HTTP/subprocess를 실제로 빌린다 | v1 실배선: input(동기 + JSPI `run_sync`), urllib(동기 XHR, proxyUrl 옵션), subprocess(`["python","-c",code]`, 자식 워커, runAsync 경로). 저수준 socket·requests 계열은 미배선 | v1 해소 (attempts/syscallBridge 졸업, 2026-07-11). 잔여는 local-parity 축 |
5050
| PyProc 오류 경로 | 부팅·행·죽음이 유한 시간에 귀결 | 부팅 실패 reject + `map(.., {taskTimeoutMs})` 행 수렴 + kill/스냅샷 respawn(302ms 실측). 남은 것: 협조적 취소(SIGINT) | 해소 (attempts/processLifecycle 졸업, 2026-07-11). 취소는 후보 |
5151
| Pyodide 스냅샷 API | 스냅샷-fork | `_makeSnapshot`/`_loadSnapshot`은 Pyodide 밑줄(실험) API. 버전 핀(v314.0.2)으로만 안전 | 버전 올릴 때 최우선 재검증 항목 |
52+
| restore()의 힙 성장 처리 | 두 복원 경로의 성장 처리 동등 | restore()(전체 복원)는 base 범위 밖 성장 페이지를 되돌리지 않고, restoreLive는 명시 처리한다(비대칭). 다음 checkpoint의 성장분 루프가 체인을 다시 정합시키므로 실해는 없을 가능성이 높으나 미실측 | 열림(외부 리뷰 관찰). runtimeParity probe 후보 |
5253

5354
## 프론티어 (정직한 벽 = WASM dlopen)
5455

mainPlan/web-python-runtime/03-progress-ledger.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,12 @@
44

55
## 결정 원장 (최신이 위)
66

7+
### 2026-07-11 외부 리뷰 대응: restoreLive 경계 계약을 기계 강제로
8+
9+
- 외부 코드 리뷰의 최우선 지적("sound를 파는 라이브러리에서 soundness 전제가 강제되지 않는다") 수용. `Runtime.execSeq`(상태 변이 카운터: run/runAsync/setGlobal/install/loadPackages)로 경계 위반을 **O(1) 감지**해 restoreLive가 자동으로 재해시 경로로 승격. 실측: 위반 시 27.4ms 안전 복원, 준수 시 0.69ms 즉시 경로 유지(`rehashed` 플래그로 확인).
10+
- 리뷰의 다른 지적 중 SIGINT 부재·버전 관문·OPFS 경제성은 리뷰 시점 이후 이미 해소됐음을 확인. "리액티브 과설계" 우려는 dartlab의 독립 재발명이 수요 반증. restore()의 힙 성장 비대칭 관찰은 계약 실태 표에 열린 항목으로 등록(probe 후보).
11+
- 릴리즈 0.0.4(버전만. 태그 폐지 정책 확정: 표식은 package.json 하나, npm 퍼블리시 개시 시 태그를 절차의 자동 산출물로 재도입).
12+
713
### 2026-07-11 dartlab 흡수 완주 + parity 승격 5종 (게이트 20검사)
814

915
- 한 턴에 승격 5종: `restoreLive({rehash})`(예외 안전 복원), `AsgiServer`(소켓 0 dispatch 3.4ms), `Terminal`(+examples/terminal.html), `interrupt(pid)`(SIGINT 517ms 수렴, respawn 0), `saveBase/loadBase`(OPFS 영속, 30MB 쓰기 256ms/읽기 46ms).

src/capabilities/reactive.js

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,25 +3,27 @@
33
// WASM은 mprotect/dirty-page가 없어 실행 경계마다 완전 해시로 델타를 재구성한다.
44
// 완전 해시(Uint32 워드)가 sound의 열쇠 - 샘플링은 불완전 델타 -> 복원 크래시.
55
//
6-
// 실행 경계 계약 (소비자가 지켜야 하는 규율):
7-
// restoreLive()"마지막 checkpoint()/restore() 이후 파이썬 실행이 없었다"를 전제한다.
8-
// 저장된 liveIdx 해시가 현재 힙을 대변한다고 믿고 재해싱 없이 비교하기 때문이다(그래서 즉시).
9-
// 실행을 했다면 반드시 checkpoint()로 경계를 닫고 나서 복원하라. 전제를 보장할 수 없으면
10-
// restore()(전체 복원, 안전 기준선)를 쓴다. 이 계약은 README 사용례와 함께 유지한다.
6+
// 실행 경계 계약 (기계 강제, 2026-07-11부터):
7+
// restoreLive()의 즉시성(재해싱 0)은 "마지막 checkpoint()/restore() 이후 실행 없음"이 전제다.
8+
// 이 전제를 Runtime.execSeq(상태 변이 카운터)로 O(1) 감지한다. 경계가 깨져 있으면(실행·예외·
9+
// setGlobal 등) 조용한 오염 대신 자동으로 재해시 경로로 승격해 복원한다. 반환값 rehashed로
10+
// 어느 경로였는지 알 수 있고, opts.rehash로 강제할 수도 있다.
1111
import { PAGE_SIZE as PAGE } from "../runtime/memoryCapability.js";
1212

1313
// Runtime.enableReactive()가 이 컨트롤러를 만든다. 소비자는 checkpoint/restore만 쓴다.
1414
export class ReactiveController {
1515
constructor(rt) {
16-
this._mem = rt.memory;
16+
this._rt = rt; this._mem = rt.memory;
1717
this.base = null; this.deltas = []; this.hashes = []; this.liveIdx = -1; this.prevHashes = null;
18+
this._seqAt = -1; // 마지막 checkpoint/restore 시점의 Runtime.execSeq (경계 위반 감지)
1819
}
1920
// 현재 힙 상태를 체크포인트로 저장. 첫 호출=base 통째, 이후=바뀐 페이지 델타.
2021
checkpoint() {
2122
const mem = this._mem, hashes = mem.pageHashes();
2223
if (this.base === null) {
2324
this.base = mem.sliceAll(); this.deltas.push(new Map());
2425
this.hashes.push(hashes); this.prevHashes = hashes; this.liveIdx = 0;
26+
this._seqAt = this._rt.execSeq; // 경계 닫힘
2527
return { index: 0, changedPages: 0, deltaBytes: this.base.length, kind: "base" };
2628
}
2729
// 해시 배열은 페이지당 2워드 interleave(실효 64비트). 두 워드 모두 같아야 "안 바뀜".
@@ -32,6 +34,7 @@ export class ReactiveController {
3234
for (let p = this.prevHashes.length / 2; p < hashes.length / 2; p++) delta.set(p, mem.slicePage(p)); // 성장분
3335
this.deltas.push(delta); this.hashes.push(hashes); this.prevHashes = hashes;
3436
this.liveIdx = this.deltas.length - 1;
37+
this._seqAt = this._rt.execSeq; // 경계 닫힘
3538
let bytes = 0; for (const b of delta.values()) bytes += b.length;
3639
return { index: this.deltas.length - 1, changedPages: delta.size, deltaBytes: bytes, kind: "delta" };
3740
}
@@ -45,6 +48,7 @@ export class ReactiveController {
4548
for (let k = 1; k <= j; k++) for (const [p, b] of this.deltas[k]) mem.writePage(p, b);
4649
mem.stackRestore(savedSP);
4750
this.liveIdx = j; this.prevHashes = this.hashes[j];
51+
this._seqAt = this._rt.execSeq;
4852
}
4953
// 라이브-차분 복원: 저장 해시 비교만(재해싱 0) -> 다른 페이지만 write. 인접 시간여행 즉시.
5054
// 전제는 파일 상단의 "실행 경계 계약" 참조. 성장 처리: 현재 힙이 목표보다 크면 목표 범위
@@ -53,7 +57,9 @@ export class ReactiveController {
5357
// 저장 해시 대신 현재 힙을 재해시해 비교한다(dartlab 노트북 런타임에서 흡수, 2026-07-11).
5458
restoreLive(j, savedSP, opts = {}) {
5559
const mem = this._mem, targetH = this.hashes[j];
56-
const liveH = opts.rehash ? mem.pageHashes() : this.hashes[this.liveIdx];
60+
// 경계 위반(마지막 checkpoint/restore 이후 상태 변이) 감지 시 자동으로 재해시 경로 승격.
61+
const rehash = !!opts.rehash || this._rt.execSeq !== this._seqAt;
62+
const liveH = rehash ? mem.pageHashes() : this.hashes[this.liveIdx];
5763
const nLive = liveH.length / 2, nTarget = targetH.length / 2; // 페이지당 2워드 interleave
5864
let written = 0, wroteBytes = 0;
5965
for (let p = 0; p < nLive; p++) {
@@ -66,7 +72,8 @@ export class ReactiveController {
6672
}
6773
mem.stackRestore(savedSP);
6874
this.liveIdx = j; this.prevHashes = this.hashes[j];
69-
return { pagesWritten: written, mbWritten: +(wroteBytes / 1048576).toFixed(2) };
75+
this._seqAt = this._rt.execSeq;
76+
return { pagesWritten: written, mbWritten: +(wroteBytes / 1048576).toFixed(2), rehashed: rehash };
7077
}
7178
timeTravel(j, savedSP, opts = {}) { return this.restoreLive(j, savedSP, opts); }
7279

src/runtime/runtime.js

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -33,16 +33,18 @@ export class Runtime {
3333
this._py = py;
3434
this.memory = new MemoryCapability(py);
3535
this._micropip = null;
36+
this.execSeq = 0; // 상태 변이 카운터. 리액티브가 실행 경계 위반을 O(1)로 감지하는 근거.
3637
}
37-
run(code) { return this._py.runPython(code); }
38-
runAsync(code) { return this._py.runPythonAsync(code); }
39-
setGlobal(name, value) { this._py.globals.set(name, value); }
38+
run(code) { this.execSeq++; return this._py.runPython(code); }
39+
runAsync(code) { this.execSeq++; return this._py.runPythonAsync(code); }
40+
setGlobal(name, value) { this.execSeq++; this._py.globals.set(name, value); }
4041
getGlobal(name) { return this._py.globals.get(name); }
4142
async install(pkg) {
43+
this.execSeq++;
4244
if (!this._micropip) { await this._py.loadPackage("micropip"); this._micropip = this._py.pyimport("micropip"); }
4345
await this._micropip.install(pkg);
4446
}
45-
async loadPackages(pkgs) { await this._py.loadPackage(pkgs); }
47+
async loadPackages(pkgs) { this.execSeq++; await this._py.loadPackage(pkgs); }
4648

4749
// Layer 1 능력 등록(opt-in). 소비자는 능력 계약만 받고 엔진 내부는 만지지 않는다.
4850
enableReactive() { return new ReactiveController(this); }

tests/attempts/runtimeParity/exceptionRestoreProbe.html

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,19 @@ <h1>probe: 예외로 더러워진 힙의 안전 복원 (dartlab 흡수)</h1>
2525
try { rt.run("x = 999\nraise ValueError('boom')"); } catch (e) {}
2626
check("전제: 예외 후 힙은 더럽다(x==999)", rt.run("x") === 999);
2727

28-
// 결함 재현: 저장 해시 신뢰 복원은 stale 비교라 오염을 못 본다
29-
reactive.restoreLive(cp.index, sp0);
30-
check("결함 재현: rehash 없는 restoreLive는 오염 잔존(x==999)", rt.run("x") === 999);
31-
32-
// 흡수한 해법: 현재 힙 재해시 후 복원
33-
try { rt.run("x = 555\nraise ValueError('boom2')"); } catch (e) {}
28+
// 기계 가드: 경계 위반을 execSeq로 감지해 자동 재해시 승격 -> 옵션 없이도 안전
3429
const t0 = performance.now();
35-
const r = reactive.restoreLive(cp.index, sp0, { rehash: true });
36-
timings.rehashRestoreMs = +(performance.now() - t0).toFixed(1);
37-
check("해법: restoreLive({rehash})가 x==1 복원", rt.run("x") === 1, `${timings.rehashRestoreMs}ms, ${r.pagesWritten}p`);
30+
const r = reactive.restoreLive(cp.index, sp0);
31+
timings.autoRehashMs = +(performance.now() - t0).toFixed(1);
32+
check("가드: 경계 위반 자동 감지 + 재해시 복원(x==1)", rt.run("x") === 1 && r.rehashed === true, `${timings.autoRehashMs}ms, ${r.pagesWritten}p`);
33+
34+
// 경계를 지키면 즉시 경로 유지(재해싱 0)
35+
rt.run("x = 5");
36+
reactive.checkpoint();
37+
const t1 = performance.now();
38+
const r2 = reactive.restoreLive(cp.index, sp0);
39+
timings.fastPathMs = +(performance.now() - t1).toFixed(2);
40+
check("경계 준수 시 즉시 경로 유지(rehashed=false)", r2.rehashed === false && rt.run("x") === 1, `${timings.fastPathMs}ms`);
3841

3942
// 복원 뒤 인터프리터 연속 실행(파이썬이 멀쩡한가)
4043
check("복원 후 연속 실행", rt.run("x + 41") === 42);

tests/browser/gate.html

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,8 @@ <h1>pyproc 브라우저 게이트</h1>
5757
check("restore: 전체 복원으로 x === 1", rt.run("x") === 1);
5858

5959
try { rt.run("x = 555\nraise ValueError('boom')"); } catch (e) {} // 예외 = 경계 없는 오염
60-
reactive.restoreLive(cp.index, sp0, { rehash: true });
61-
check("restoreLive({rehash}): 예외 오염 복원", rt.run("x") === 1);
60+
const rr1 = reactive.restoreLive(cp.index, sp0); // 옵션 없이: 가드가 자동 재해시 승격
61+
check("restoreLive 가드: 경계 위반 자동 감지 복원", rt.run("x") === 1 && rr1.rehashed === true);
6262

6363
// base의 OPFS 영속: 내보내고 되읽은 base로도 복원이 성립해야 한다
6464
const opfsRoot = await navigator.storage.getDirectory();

0 commit comments

Comments
 (0)