docs(phase29aa): queue P6 intersection join
This commit is contained in:
@ -1,6 +1,6 @@
|
||||
# Phase 29aa: RC insertion safety expansion(CFG-aware design)
|
||||
|
||||
Status: P5 Complete (Multi-predecessor Return join)
|
||||
Status: P6 Ready (Multi-predecessor Return join - intersection)
|
||||
Scope: Phase 29z の単一block限定実装から、誤releaseを起こさない形で CFG-aware に拡張するための設計を固める。
|
||||
|
||||
Entry:
|
||||
@ -25,6 +25,7 @@ Progress:
|
||||
- P3: Jump→Return(単一 predecessor)で state 伝播し ReturnCleanup を成立させる(P2維持)
|
||||
- P4: Jump-chain(単一 predecessor 直列)で state 伝播し ReturnCleanup を成立させる(P2/P3 維持)
|
||||
- P5: Multi-predecessor Return で incoming state が完全一致する場合のみ ReturnCleanup を成立させる(P2/P3/P4 維持)
|
||||
- P6: Multi-predecessor Return で incoming state の「安全な共通部分(intersection)」のみ cleanup する(P2-P5 維持)
|
||||
|
||||
P3 SSOT:
|
||||
- Contract:
|
||||
@ -75,3 +76,17 @@ P5 SSOT:
|
||||
- selfcheck Case 3.7(state一致 → Return block に 1 cleanup)PASS
|
||||
- selfcheck Case 3.8(state不一致 → 全ブロック 0 cleanup)PASS
|
||||
- 既定OFF維持(featureなしは no-op)
|
||||
|
||||
P6 SSOT:
|
||||
- Objective:
|
||||
- Return block が multi-predecessor のとき、incoming state が完全一致しない場合でも
|
||||
「全経路で必ず保持されている ptr→value」のみを ReturnCleanup で release する。
|
||||
- Contract:
|
||||
- cleanup は Return block の BeforeTerminator のみ(Jump/Branch block には入れない)
|
||||
- join state は `intersection`(全 predecessor の end_state に同じ ptr が存在し、かつ value が同一のものだけ)
|
||||
- intersection が empty の場合は cleanup しない
|
||||
- subset/partial merge は許可するが、PHI 的な “値の合成” はしない(同一値のみ)
|
||||
- Non-goals:
|
||||
- PHI/loop/early-exit の cleanup
|
||||
- value が一致しない ptr を release 対象に含めること
|
||||
- Jump block への release 挿入(P2維持)
|
||||
|
||||
Reference in New Issue
Block a user