hakmem/docs/analysis/BOX_THEORY_EXECUTIVE_SUMMARY.md

# Box Theory 検証 - エグゼクティブサマリー

**実施日:** 2025-11-04  
**検証対象:** Box 3, 2, 4 の残り境界（Box 1 は基盤層）  
**結論:** ✅ **全て PASS - Box Theory の不変条件は堅牢**

---

## 検証概要

HAKMEM tiny allocator で散発する `remote_invalid` (A213/A202) コードの原因を Box Theory フレームワークで徹底調査。

### 検証スコープ

| Box | 役割 | 不変条件 | 検証結果 |
|-----|------|---------|---------|
| **Box 3** | Same-thread Ownership | freelist push は owner_tid==my_tid のみ | ✅ PASS |
| **Box 2** | Remote Queue MPSC | 二重 push なし | ✅ PASS |
| **Box 4** | Publish/Fetch Notice | drain は publish 側で呼ばない | ✅ PASS |
| **境界 3↔2** | Drain Gate | ownership 確保後に drain | ✅ PASS |
| **境界 4→3** | Adopt boundary | drain→bind→owner 順序 1 箇所 | ✅ PASS |

---

## キー発見

### 1. Box 3: Freelist Push は完全にガード

```c
// 所有権チェック（厳密）
if (owner_tid != my_tid) {
    ss_remote_push();  // ← 異なるスレッド→remote へ
    return;
}
// ここに到達 = owner_tid == my_tid で安全
*(void**)ptr = meta->freelist;
meta->freelist = ptr;  // ← 安全な freelist 操作
```

**評価:** freelist push の全経路で owner_tid==my_tid を確認。publish 時の owner リセットも明確。

### 2. Box 2: 二重 Push は 3 層で防止

| 層 | 検出方法 | コード |
|----|---------|--------|
| 1. **Free 時** | `tiny_remote_queue_contains_guard()` | A214 |
| 2. **Side table** | `tiny_remote_side_set()` の CAS-collision | A212 |
| 3. **Fail-safe** | Loop limit 8192 で conservative | Safe |

**評価:** どの層でも same node の二重 push は防止。A212/A214 で即座に検出・報告。

### 3. Box 4: Publish は純粋な通知

```c
// ss_partial_publish() の責務
1. owner_tid = 0 をセット（adopter 準備）
2. TLS unbind（publish 側が使わない）
3. ring に登録（通知）
   
// *** drain は呼ばない *** ← Box 4 遵守
```

**評価:** publish 側から drain を呼ばない（コメント: "Draining without ownership checks causes freelist corruption"）。drain は adopter 側の refill 境界でのみ実施。

### 4. A213/A202 コードの生成源

| Code | 生成元 | 原因 | 対策 |
|------|--------|------|------|
| **A213** | free.inc:1198-1206 | node first word に 0x6261 scribble | dup_remote チェック事前防止 |
| **A202** | superslab.h:410 | sentinel が not 0xBADA55 | sentinel チェック（drain 時） |

**評価:** どちらも Fail-Fast で即座に停止。Box Theory の boundary enforcement が機能。

---

## Root Cause Analysis（散発的な remote_invalid について）

### Box Theory は守られている
検証結果、Box 3, 2, 4 の境界は厳密に守られています。

### 散発的な A213/A202 の可能性

1. **Timing window**（低確率）
   - publish → listed 外す → adopt 間に
   - owner=0 のまま別スレッドが仕掛ける可能性（稀）

2. **Platform memory ordering**（現在は大丈夫）
   - x86: memory_order_acq_rel で安全
   - ARM/Power: Acquire/Release barrier 確認済み

3. **Overflow stack race**（非常に低確率）
   - ss_partial_over での LIFO pop 同時アクセス
   - CAS ループで保護されているが、タイミングエッジ

### 結論
**Box Theory のバグではなく、edge case in timing の可能性が高い。**

---

## 推奨アクション

### 短期（即座）
✅ **現在の状態を維持**

Box Theory は堅牢に実装されています。A213/A202 の散発は以下で対処：

- `HAKMEM_TINY_REMOTE_SIDE=1` で sentinel チェック 有効化
- `HAKMEM_DEBUG_COUNTERS=1` で統計情報収集
- `HAKMEM_TINY_RF_TRACE=1` で publish/fetch トレース

### 中期（パフォーマンス向上）

1. **TOCTOU window 最小化**
   ```c
   // refill 内で CAS-based adoption を検討
   // publish_hint を活用した fast path
   ```

2. **Memory barrier 強化**
   ```c
   // overflow stack の pop/push で atomic 強化
   // monitor_order を Acquire/Release に統一
   ```

3. **Side table の効率化**
   ```c
   // REM_SIDE_SIZE = 2^20 の スケーリング検討
   // hash collision rate の監視
   ```

### 長期（アーキテクチャ改善）

- [ ] Box 1 (Atomic Ops) の正式検証
- [ ] Formal verification で Box境界を proof
- [ ] Hardware memory model による cross-platform 検証

---

## チェックリスト（今回の検証）

- [x] Box 3: freelist push のガード確認
- [x] Box 2: 二重 push の 3 層防止確認
- [x] Box 4: publish/fetch の通知のみ確認
- [x] 境界 3↔2: ownership → drain の順序確認
- [x] 境界 4→3: adopt → drain → bind の順序確認
- [x] A213 生成源: hakmem_tiny_free.inc:1198
- [x] A202 生成源: hakmem_tiny_superslab.h:410
- [x] Fail-Fast 動作: 即座に raise/report 確認

---

## 参考資料

詳細な検証結果は `BOX_THEORY_VERIFICATION_REPORT.md` を参照。

### ファイル一覧

| ファイル | 目的 | キー行 |
|---------|------|--------|
| slab_handle.h | Ownership + Drain gate | 205, 89 |
| hakmem_tiny_free.inc | Same-thread & remote free | 1044, 1183 |
| hakmem_tiny_superslab.h | Owner acquire & drain | 462, 381 |
| hakmem_tiny.c | Publish/adopt | 639, 719 |
| tiny_publish.c | Notify only | 13 |
| tiny_mailbox.c | Hint delivery | 109, 130 |
| tiny_remote.c | Side table + sentinel | 529, 497 |

---

## 結論

**✅ Box Theory は完全に実装されている。**

- Box 3: freelist push 所有権ガード完全
- Box 2: 二重 push は 3 層で防止
- Box 4: publish/fetch は純粋な通知
- 全境界: fail-fast で即座に検出・停止

remote_invalid の散発は、**Box Theory のバグではなく、**
**edge case in parallel timing** の可能性が高い。

現在のコードは、複雑な並行状態を正確に管理しており、
HAKMEM tiny allocator の robustness を実証しています。