Skip to content

Commit 1560ff2

Browse files
committed
Pin the elision attack programs as tests, plan the dynamic-loading melding
Distill the adversarial review's attack programs into five permanent runtime regressions using the printing-finalizer oracle (a double-free prints twice, a leak prints zero, the print position pins when elided ownership ends): the conditional move at a join, two calls with the retain kept at the first, a value returned and passed, a spawned value used by the spawner after, and a 200-iteration move-heavy loop asserting 600 finalizations and a bounded heap. Record in RC_ELISION.md how elision melds with dynamically loaded modules, in three layers: a hard border (boundary calls keep the fixed callee-owns convention, so each side is correct regardless of the other and hot reload is safe by construction), move elision unaffected (caller-local against the universal convention), and summaries as an opt-in ABI section with dual entry points bound by the load-time linker, so a summary mismatch costs performance, never correctness.
1 parent 67aa87d commit 1560ff2

2 files changed

Lines changed: 87 additions & 1 deletion

File tree

plans/RC_ELISION.md

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,8 @@ everywhere else the borrow wins, so the composition is strictly better and never
129129
mode. One summary map drives both sides in one compilation, and `--rc-report` should print each
130130
function's modes so tests can pin them (the same oracle pattern the move elision used).
131131
- **Separate compilation later.** Bytecode-level linking (IMPORT.md) must serialize summaries into
132-
the module format, or boundaries fall back to all-Owned. Whole-program holds today.
132+
the module format, or boundaries fall back to all-Owned. Whole-program holds today. The fuller
133+
melding is its own section below.
133134
- **Multicore later.** A borrow is valid only within the frame-synchronous world. Cross-core sends
134135
are moves of `Owned<T>` (DESIGN_NOTES), and a send is an escape, so the models compose.
135136
- **Closures later.** If first-class functions ever land, a capture is an escape. The static call
@@ -141,6 +142,26 @@ everywhere else the borrow wins, so the composition is strictly better and never
141142
per-mode tests: a read-only param is Borrowed, a stored or returned or reassigned param is Owned, a
142143
spawn target is all-Owned.
143144

145+
## Dynamic loading and module boundaries (how elision melds with IMPORT.md)
146+
147+
Dynamically loaded bytecode modules (load-time linking, hot reload) break the whole-program
148+
assumption, and the melding is three layers, from safest to most optimized:
149+
150+
1. **The hard border.** Module-boundary calls use the fixed callee-owns convention, always. Inside a
151+
module, full elision applies and is invisible from outside, so each side is correct regardless of
152+
what the other side does. This is the safest assumption made structural rather than assumed, and
153+
it makes hot reload safe by construction: a reloaded module can change its internals freely while
154+
its exports keep the fixed convention. No metadata is needed for correctness.
155+
2. **Move elision needs nothing.** It is caller-local against the universal callee-owns convention,
156+
so it survives dynamic loading and reload untouched.
157+
3. **Metadata as the opt-in optimization layer.** Cross-border borrows need to know the other side,
158+
so per-function parameter-mode summaries ship in the bytecode module format
159+
(BYTECODE_FILE_FORMAT.md) as a versioned ABI section. The safe realization: an exported function
160+
carries two entry points, the conventional one and a borrowed-convention fast path, and the
161+
load-time linker binds a caller to the fast path only when the summaries verify. A reload whose
162+
summaries changed re-binds affected callers to the conventional entry. A mismatch therefore costs
163+
performance, never correctness, which extends the oracle-not-gate rule to the linker.
164+
144165
## Order of execution
145166

146167
1. **Summaries plus report, no codegen change.** Compute per-function parameter modes with the

solid-snake-compiler/src/bytecode_gen.rs

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2001,6 +2001,71 @@ mod codegen_tests {
20012001
);
20022002
}
20032003

2004+
// Runtime elision regressions distilled from the adversarial memory-safety review's attack
2005+
// programs. Each uses a printing Delete finalizer as the oracle: a double-free prints twice, a
2006+
// leak prints zero times, and the print position pins when the elided ownership actually ends.
2007+
const RES_TYPE: &str =
2008+
"type Res(Delete):\n id: Int\n def delete(self):\n print(\"D\", self.id)\n\n";
2009+
2010+
#[test]
2011+
fn rc_conditional_move_at_join_frees_exactly_once() {
2012+
// The value is passed on one branch only and its drop sits after the join, so the
2013+
// control-flow guard must keep the counting. One finalizer per run, on both branch outcomes.
2014+
let (_, out) = run_src(&format!(
2015+
"{RES_TYPE}def take(r: Res) -> Int:\n return r.id\n\ndef run(flag: Bool) -> Int:\n let a = Res(5)\n let x = 0\n if flag:\n x = take(a)\n return x\n\nprint(\"t\", run(true))\nprint(\"f\", run(false))\n"
2016+
));
2017+
assert_eq!(out, "t D 5\n5\nf D 5\n0\n");
2018+
}
2019+
2020+
#[test]
2021+
fn rc_two_calls_retain_stays_at_the_first() {
2022+
// Passed to two calls: the retain must stay at the first (the value is still live), and only
2023+
// the second is a move. The finalizer fires once, at the consuming call, before the print
2024+
// that follows it.
2025+
let (_, out) = run_src(&format!(
2026+
"{RES_TYPE}def peek(r: Res) -> Int:\n return r.id\n\ndef consume(r: Res) -> Int:\n return r.id\n\nlet r = Res(5)\nlet a = peek(r)\nlet b = consume(r)\nprint(\"ab\", a, b)\n"
2027+
));
2028+
assert_eq!(out, "D 5\nab 5 5\n");
2029+
}
2030+
2031+
#[test]
2032+
fn rc_returned_and_passed_value_stays_live() {
2033+
// The callee both reads its parameter and returns it, so ownership rides out on the return
2034+
// and the caller's binding stays valid after.
2035+
let (_, out) = run_src(&format!(
2036+
"{RES_TYPE}def peek(r: Res) -> Int:\n return r.id\n\ndef wrap(r: Res) -> Res:\n let x = peek(r)\n return r\n\nlet r = wrap(Res(6))\nprint(\"id\", r.id)\n"
2037+
));
2038+
assert_eq!(out, "id 6\nD 6\n");
2039+
}
2040+
2041+
#[test]
2042+
fn rc_spawned_value_usable_by_spawner_and_freed_once() {
2043+
// Spawn takes its own reference, the spawner keeps using the value after, and exactly one
2044+
// finalizer fires once both are done.
2045+
let (_, out) = run_src(&format!(
2046+
"{RES_TYPE}def worker(r: Res):\n print(\"worker\", r.id)\n\nlet r = Res(8)\nspawn worker(r)\nprint(\"main sees\", r.id)\nscheduler_run()\n"
2047+
));
2048+
assert_eq!(out, "main sees 8\nworker 8\nD 8\n");
2049+
}
2050+
2051+
#[test]
2052+
fn rc_move_heavy_loop_frees_all_and_stays_bounded() {
2053+
// Per-iteration temporaries moved through aliases and calls, 200 iterations: every resource's
2054+
// finalizer fires exactly once and the heap stays bounded, so the elision leaks nothing and
2055+
// frees nothing twice under sustained reuse.
2056+
let (vm, out) = run_src(&format!(
2057+
"{RES_TYPE}def take(r: Res) -> Int:\n return r.id\n\ndef combine(a: Res, b: Res) -> Int:\n return a.id + b.id\n\nlet i = 0\nlet acc = 0\nwhile i < 200:\n let r = Res(i)\n let q = r\n acc = acc + take(q)\n let x = Res(i)\n let y = Res(i)\n acc = acc + combine(x, y)\n i = i + 1\nprint(\"acc\", acc)\n"
2058+
));
2059+
let finalized = out.lines().filter(|l| l.starts_with("D ")).count();
2060+
assert_eq!(finalized, 600, "600 resources must each finalize exactly once");
2061+
assert!(out.ends_with("acc 59700\n"), "unexpected tail: {out:?}");
2062+
assert!(
2063+
vm.heap_section_count() < 40,
2064+
"heap should stay bounded under reuse, got {}",
2065+
vm.heap_section_count()
2066+
);
2067+
}
2068+
20042069
#[test]
20052070
fn rc_aliasing_last_use_is_movable() {
20062071
// `let b = a` with `a` dead afterward is a move of the reference into `b`. `a` is a parameter

0 commit comments

Comments
 (0)