From 3284aa06b4174ab6522d668a70f910a603729ef5 Mon Sep 17 00:00:00 2001 From: Alliana <56180684+Allianaab2m@users.noreply.github.com> Date: Wed, 29 Jul 2026 01:42:10 +0900 Subject: [PATCH] =?UTF-8?q?spec:=200056=20Deterministic=20Resource=20Clean?= =?UTF-8?q?up=20=E2=80=94=20defer=20=E3=81=AB=E3=82=88=E3=82=8B=E3=82=B9?= =?UTF-8?q?=E3=82=B3=E3=83=BC=E3=83=97=E8=84=B1=E5=87=BA=E6=99=82=E3=81=AE?= =?UTF-8?q?=E3=83=95=E3=82=A1=E3=82=A4=E3=83=8A=E3=83=A9=E3=82=A4=E3=82=B6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ホスト資源（fd・ソケット）をスコープ脱出の全経路で確定的に解放する言語機構を 定める。ブロック項 `defer ` を導入し、正常完了・エラーチャネル・自己末尾 呼び出し（0045）のいずれでも action がちょうど 1 回走ることを保証する。 0024/0048 A2 の finalizer 禁止とは衝突しない。禁止対象は RC 回収の観測であり、 `defer` はレキシカルで参照カウントを見ない（D12）。RC を持たないバックエンドで 意味論が変わらないことがその実証になる。 キャンセルは第 3 のチャネルを作らず、協調キャンセルとしてエラーチャネルに載せる 方針を Open Questions に記す。接続断・タイムアウトは既に throws チャネル上にある。 README の Current Drafts に 0056 を追記し、漏れていた 0053・0054 も補う。 --- README.md | 3 + specs/0056-deterministic-resource-cleanup.md | 188 +++++++++++++++++++ 2 files changed, 191 insertions(+) create mode 100644 specs/0056-deterministic-resource-cleanup.md diff --git a/README.md b/README.md index cfdc5be..50b4cfd 100644 --- a/README.md +++ b/README.md @@ -130,3 +130,6 @@ Accepted にする前に解くべき未解決事項。 - [0050: Socket — wasi:sockets 上のプリミティブ effect](specs/0050-socket-primitive-effect.md) - [0051: Bytes — 不変のバイト列](specs/0051-bytes.md) - [0052: Backend Targets — wasm-unknown / wasm-wasip2 と platform 関数の供給差](specs/0052-backend-targets.md) +- [0053: Bitwise Operators and Shifts](specs/0053-bitwise-operators.md) +- [0054: Random — the `Random` Effect and a Seedable PRNG](specs/0054-random-effect-and-prng.md) +- [0056: Deterministic Resource Cleanup — `defer` によるスコープ脱出時のファイナライザ](specs/0056-deterministic-resource-cleanup.md) diff --git a/specs/0056-deterministic-resource-cleanup.md b/specs/0056-deterministic-resource-cleanup.md new file mode 100644 index 0000000..b5c3076 --- /dev/null +++ b/specs/0056-deterministic-resource-cleanup.md @@ -0,0 +1,188 @@ +# 0056: Deterministic Resource Cleanup — `defer` によるスコープ脱出時のファイナライザ + +Status: Draft + +ホストが握る資源（ファイル記述子、ソケット）を、スコープを抜けるすべての経路で確定的に解放するための言語機構を定める。ブロック項 `defer ` を導入し、その action が囲むブロックの正常完了・エラーチャネルによる脱出・自己末尾呼び出しによる脱出のいずれにおいてもちょうど 1 回実行されることを保証する。0048 の ARC が線形メモリ上のヒープ値を回収するのに対し、本仕様はホスト資源の解放を担う。両者は独立した機構であり、`defer` は参照カウントを一切観測しない（0024 / 0048 A2 との整合は本文で論証する）。 + +## Summary + +- ブロック項 **`defer `** を追加する（0004 のブロック構文の拡張）。スコープは**それを含むブロックの残り**であり、`if` の分岐・`match` のアーム・`try` の body に自然に閉じる。 +- action は**スコープ脱出時**に評価され、同一ブロック内の複数の `defer` は**登録の逆順**に実行される。Zig と同じレキシカルブロックスコープであり、Go の関数スコープは採らない。 +- 保証する脱出経路は 3 つ：**正常完了**、**エラーチャネル**（`throw` / `?` / 呼び出し先からの伝播、0011）、**自己末尾呼び出し**（0045）。Emela はループ構文を持たず、すべての反復が自己末尾呼び出しであるため、3 つ目は必須である。 +- action は `throws` を持ってはならず、型は `Unit` または `Never` でなければならない。action の effect は囲む関数の `uses` に合流する。 +- `panic` は action を実行しない。ホスト資源はインスタンス破棄時にホストが回収する。 +- 所有権・借用・線形性は導入しない（0000 の非目標を維持）。安全性は「`close` は冪等」（0050 P7 / 0055 P2）という既存方針に依拠する。 + +## Motivation + +現在の Emela には、資源解放の言語機構が存在しない。`File` / `Listener` / `Connection` はホスト発行の識別子を包んだ普通のレコードにすぎず、0048 の ARC が回収するのは線形メモリ上のヒープ値だけで、ホストが握る fd やソケットには届かない。解放は明示的な `Fs.close(handle)` / `Socket.close(handle)` の呼び出しだけが担っている。 + +その結果、**エラー経路でハンドルが確実に漏れる**。`std.fs` の便宜関数がその実例である。 + +```emela +pub fn read_file(path: String) -> Bytes throws FsError { + let f = raw_open_read(path)? + let data = read_all_loop(f)? -- ここで throw すると + raw_close(f.id) -- close に到達しない + data +} +``` + +同型の漏れが `write_file`、および 0046 の `HttpServer.respond` / `accept_one` にもある。とりわけ深刻なのは**サーバの accept ループ**である。0045 が保証する自己末尾呼び出しによって accept ループは有界メモリで無限に回るため、1 反復あたり 1 個の fd の漏れは確実に枯渇へ至る。 + +0011 の `try` / `catch` は「必ず実行される節」を持たないため、この問題を解けない。手で書くならすべての脱出点に `close` を複製することになり、`?` を使う限り脱出点はソース上に現れない。 + +一方、0024 / 0048 A2 は finalizer・デストラクタ・weak reference を明示的に禁じている。禁じられているのは**参照カウントによる回収を観測可能にすること**であり、`defer` はそれとは別の機構である（後述）。 + +## Specification + +以下、キーワードは RFC 2119 に従う。 + +### 構文とスコープ + +- **D1** ブロック（0004）の項として `defer ` を追加する。`` を本仕様では **action** と呼ぶ。 +- **D2** `defer` の**スコープ**は、それを含むブロックの、その `defer` 項より後ろの部分である。したがって `if` の分岐・`match` のアーム・`try` の body・`catch` のアームに書かれた `defer` は、そのブロックにのみ効く。 +- **D3** `defer` はブロックの末尾項であってはならない（MUST NOT）。守るべき本体が空であり、その action は `defer` を外した式と等価だからである。 + +### 実行の保証 + +- **D4** action は、そのスコープからの以下のすべての脱出経路において、**ちょうど 1 回**実行されなければならない（MUST）。 + 1. **正常完了** — スコープが値を生じてブロックの外へ流れる。 + 2. **エラーチャネル**（0011）— `throw`、`?` による伝播、または呼び出し先から伝播したエラーがスコープを貫く。action の実行後、エラーは元の伝播先へ向けて再送出されなければならない（MUST）。 + 3. **自己末尾呼び出し**（0045）— スコープ内の末尾位置にある自己末尾呼び出しが関数の先頭へ戻る。action は反復ごとに実行されなければならない（MUST）。 + + 経路 3 は、Emela がループ構文を持たずすべての反復を自己末尾呼び出しで表現するために必要である。これを欠くと `defer` はループ本体で一度も実行されない。 +- **D5** action は `defer` 項に到達した時点ではなく、**脱出時**に評価される（MUST）。 +- **D6** 同一ブロック内に複数の `defer` がある場合、action は**登録の逆順**に実行されなければならない（MUST）。ネストしたスコープでは、内側のスコープの action が外側のものより先に実行される（MUST）。 +- **D7** action の実行は、0009 の effect 意味論および 0011 のエラーチャネルに関して観測可能な順序を持つ。action が `uses` に現れる effect を行う場合、その作用は D4 の各経路について、脱出が完了する前に生じたものとして観測される（MUST）。 + +### action の制約 + +- **D8** action は `throws` を持ってはならない（MUST NOT）。型は `Unit` または `Never` でなければならない（MUST）。 + + 根拠：body がエラーを伝播している最中に action もエラーを送出すると、どちらを伝播するかの選択を強いられる。0011 のエラーチャネルは単一のエラー型を運ぶため 2 つを合成できず、抑制（suppression）の概念を導入するのは本仕様の複雑さに見合わない。実用上の制約はほとんどない。解放操作である `Socket.close`（0050 P7）と `Fs.close`（0055 P2）は既に infallible として定義されている。失敗しうる後始末は `try { ... } catch { e -> () }` で包んで明示的に握りつぶす。 +- **D9** action の effect row は、それを含む関数の `uses`（0009 / 0022）に合流する。したがって `defer Fs.close(f.id)` を含む関数は `uses { Fs }` を持たなければならない（MUST）。 + +### 保証しないこと + +- **D10** `panic`（0011）は action を実行しない（MUST NOT）。`panic` はインスタンスの終了であり、通常評価へ復帰しない。ホストが保持する資源は**インスタンスの破棄時にホストが回収する**。`proc_exit` および `main` からの正常終了についても同様に action は実行されない。 + + したがって `defer` は**プロセス内での資源枯渇を防ぐ**機構であって、プロセス終了時の資源回収を担うものではない。 +- **D11** `defer` は use-after-close を防がない。`defer close(h)` を書いた後もそのハンドルは自由に読め、他所へ渡せる。所有権・借用・線形性・アフィン型は導入しない（MUST NOT。0000 の非目標を維持）。安全性は `close` の冪等性（0050 P7 / 0055 P2）に依拠する。 + +### 0024 / 0048 A2 との関係 + +0024 および 0048 A2 は finalizer・デストラクタ・weak reference を禁じている。禁止の対象は**参照カウントによる回収（refcount が 0 に達する瞬間）を観測可能にすること**であり、`defer` はこれに該当しない。 + +- **D12** action の実行点は、`defer` を含むブロックの構造だけによって決まらなければならない（MUST）。値の到達可能性・参照カウント・回収のタイミングに依存してはならない（MUST NOT）。 + +この規則から次が従う。action が値 `x` を参照していても、`x` の参照カウントがいくつであろうとスコープを抜ければ action は実行される。逆に `x` が回収されても action は実行されない。action は束縛にぶら下がっておらず、`defer` を通じて回収のタイミングを観測することはできない。 + +さらに、0048 A9 により参照カウント命令を無視してよいバックエンド（ホスト GC を持つもの）においても、`defer` の意味論は変わらない。これは `defer` が finalizer ではないことの実証である。デストラクタであれば、参照カウントを持たないバックエンドで意味が変わってしまう。 + +## Examples + +### 資源の解放 + +```emela +pub fn read_file(path: String) -> Bytes throws FsError { + let f = raw_open_read(path)? + defer raw_close(f.id) + read_all_loop(f)? -- throw しても close される +} +``` + +### サーバの accept ループ（経路 3） + +```emela +fn serve(listener: Listener) -> Unit uses { Socket } { + try { + let conn = Socket.accept(listener)? + defer Socket.close(conn.id) + let data = Socket.read(conn, 4096)? + Socket.write(conn, data)? + } catch { e -> () } + serve(listener) -- 自己末尾呼び出し（0045） +} +``` + +`defer` は `try` の body に書かれているので、スコープはその body である。接続は、読み書きが成功しても失敗しても、反復ごとに閉じられる。 + +### 逆順とネスト + +```emela +fn f() -> Unit uses { Io } { + defer Io.print("a") + defer Io.print("b") + { + defer Io.print("c") + Io.print("inner") + } + Io.print("outer") +} +-- inner / c / outer / b / a の順に出力される +``` + +### 拒否される例 + +```emela +fn bad1() -> Unit uses { Fs } throws FsError { + let f = Fs.open_read("x")? + defer Fs.read(f, 1)? -- 誤り（D8）: action は throws を持てない + () +} + +fn bad2() -> Unit uses { Io } { + Io.print("x") + defer Io.print("y") -- 誤り（D3）: 末尾項の defer +} + +fn bad3() -> Unit uses { Fs } { + let f = Fs.open_read("x") -- （型エラーは別） + defer f.id -- 誤り（D8）: action の型は Unit か Never +} +``` + +## Compilation Notes + +この節は非規範的である。 + +- **typed IR（0012）**への追加は 1 ノードでよい。`cleanup { body, action }` は「`body` を評価し、`body` からのあらゆる脱出において `action` を評価する」を意味する。ブロックの lowering は `let` と同じ形で畳める。すなわち `defer a; rest` は `cleanup { body: , action: a }` となり、D2 のスコープと D6 の逆順（後の `defer` ほど内側になる）が構造から自動的に得られる。 +- **展開**。`cleanup` は 0045 の自己末尾呼び出し書き換えの**後**に、既存のノードだけへ展開できる。 + + ```text + let $v = try { body' } catch { $e -> action; throw $e } + action + $v + ``` + + ここで `body'` は、内部の各自己末尾呼び出しの直前にも `action` を挿入した `body` である。展開は**内側から外側へ**（post-order）行う必要がある。外側から行うとネストした `defer` の実行順序が D6 に反する。 +- **`action` のコード複製**は脱出経路の数だけ生じる（正常路 1 + catch 路 1 + 自己末尾呼び出しの数）。Zig と同じ方式であり、action は実務上数命令の `close` 呼び出しである。動的な defer リストを持たないため実行時表現はゼロである。 +- **保護用の `try` は、body が実際にその地点を貫いて raise しうるときだけ出す**。無条件に出すと、非 throwing 関数において catch アームの再送出が関数境界のエラー返却経路に落ち、戻り値表現と食い違う。判定は「`throw` / `?` / throwing な呼び出しを含むか」を、内側の `try` の body（そこで捕まる）と入れ子の関数リテラル（別関数）を除いて走査すればよい。catch アームの網羅性は型検査が保証しているので、この判定で必要十分である。 +- **自己末尾呼び出しの表現がバックエンドで異なる点に注意する**。ジャンプとして実装するバックエンド（WASM の `br`）では、ジャンプが正常路を飛び越えるため、各自己末尾呼び出しの直前に `action` を挿入する必要がある。トランポリン用のマーカー値として実装するバックエンド（JavaScript）では、マーカーが正常路を値として通過するため、挿入すると action が反復ごとに 2 回実行される。展開はこの差をパラメータとして持つ必要がある。 +- **0048 の RC 挿入との順序**。`cleanup` の展開は RC 命令の挿入より前に行う。展開が `action` を `let` の値位置に置く形（`let $c = action; <脱出>`）にしておけば、0048 の release 挿入は `let` の継続側へ降りるため、**action は、それが参照する束縛の release より前**に置かれる。3 経路すべてでこの順序が保たれる。 +- **参照実装における既知の前提**。0048 の release 挿入パスは「自己末尾呼び出しは末尾位置にしか現れない」という不変条件に依存しており、末尾以外の部分式（`let` の値、`try` の body、`if` の条件、`match` の scrutinee）を走査していない。今日はそれで健全である（0045 T1 によりそれらは末尾位置ではないため）が、本仕様の展開はその不変条件を破る。展開は自己末尾呼び出しを `try` の body に入れ、さらに値経路の `let` の値にも入れるからである。 + + したがって release 挿入パスは、**自己末尾呼び出しをそれがどこにあっても脱出として扱い**、その直前に release を置く必要がある。`throw` については不要である。`throw` による大域脱出時の解放はバックエンドの unwind クリーンアップ（0048 A7）が担うのに対し、自己末尾呼び出しは単なるジャンプでありそこを通らないためである。この扱いは経路ごとに丁度 1 回を保つ。ジャンプが発火した経路はその下の release に到達せず、ジャンプのない経路はこの release に到達しない。 +- **`defer` は 0049 の `with` とは無関係**である。`with` は静的 handler の供給であり、`defer` は制御構文である。キーワードは重複しない。 + +## Open Questions + +- **`use x = e` 形の糖衣**。`let x = e; defer close(x)` の頻出パターンに対する専用構文（`use x = Fs.open_read(p)?` が `close` を自動で導く）は考えうるが、「どの関数が解放関数か」をコンパイラに教える機構（0041 の `@lang` 属性、あるいはトレイト）を要する。`defer` は `use` を包含するので、先に `defer` を定め、必要になってから糖衣を検討する。 +- **`defer { ... }` のブロック形**。当面 action は単一の式に限る。ブロック形を許すと action の内部にさらに `defer` を書けてしまい、意味を定める価値が薄い。 +- **キャンセル**。Emela には cancel / timeout / structured concurrency の概念がない。一方、実際に「途中で打ち切られる」事象（接続断、ホストのタイムアウト）はすべて既に 0011 のエラーチャネルに乗っている。協調キャンセル（明示的なチェックポイントがエラーを送出する形）を採る限り、D4 の経路 2 がそのまま cancel を覆う。非協調なプリエンプションを導入する場合は trap 相当となり、D10 により action は実行されない。将来、エラーチャネルから独立した第 3 の脱出理由を導入する場合でも、`cleanup { body, action }` は脱出理由に依存しない形なので、変わるのは展開規則だけである。 +- **`main` の正常終了時に action を走らせるか**。D10 は走らせないと定めたが、`main` の本体は普通のブロックであり、正常完了は D4 の経路 1 でもある。参照実装では `main` の本体の `defer` は経路 1 として実行され、`proc_exit` による中断だけが除外される。この境界を規範として書き下すかは未決である。 +- **プラグインバックエンド（0012 の外部 IR 受け渡し）**。`cleanup` ノードを ABI に露出するか、渡す前に展開するかは実装の裁量とする。露出する場合、自己末尾呼び出しの表現（ジャンプかマーカーか）をバックエンドが宣言する必要がある。 + +## 他仕様との関係 + +- **0004（Blocks and Expression Semantics）**: ブロック項に `defer` を追加する。ブロックの値と型は変わらない。 +- **0009（Effect Semantics）/ 0022（Effect-Row Polymorphism）**: action の effect row は囲む関数の `uses` に合流する（D9）。新たな effect は導入しない。 +- **0011（Error handling）**: D4 の経路 2 がエラーチャネルによる脱出を覆う。`try` / `catch` に「必ず実行される節」を追加するのではなく、独立した項として定める。action は `throws` を持てない（D8）。 +- **0012（Typed IR）**: `cleanup { body, action }` を 1 ノード追加する。表層構文との対応は 1 対 1 である。 +- **0024（Memory Model）/ 0048（ARC）**: A2 の finalizer 禁止と衝突しない。`defer` はレキシカルな制御構文であり、回収のタイミングを観測しない（D12）。両者は独立で、0048 が線形メモリ上のヒープ値を、本仕様がホスト資源を担う。0048 A9 のバックエンドでも意味論は同一である。 +- **0045（Self Tail Calls）**: D4 の経路 3。自己末尾呼び出しによるスコープ脱出でも action が実行されることを要求する。0045 T2 の有界メモリ保証は維持される（`defer` は動的なリストを持たない）。 +- **0049（Effects as Compile-Time DI）**: `with` キーワードとは無関係。`defer` は handler の供給ではない。 +- **0050（Socket）/ 0055（Fs）**: `close` の冪等性（0050 P7 / 0055 P2）が D11 の安全性の根拠である。両モジュールの便宜関数は本仕様の `defer` で書き直される。 +- **0046（HTTP Server）**: `HttpServer.respond` / `accept_one` の接続解放が本仕様で確定的になる。 +- **0000（Language Design Principles）**: 所有権・借用・move を導入しない非目標を維持する（D11）。