Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,11 @@ The generated loop is now written from the program's source alone, and the manif
- **Generated protocol and trace types spell a dependency type qualified when its bare name is taken** in the entry by another visible module, and read the type the checker narrowed a call to, so `Random.int` with literal bounds is `Int` in a trace as it is at the call.
- **A missing `depends` edge is reported as one.** Naming `Module.Type` from a module this module does not depend on used to advise adding the type to the other module's `exposes`.
- **A module checked or verified as one unit of a program is lowered against the program's answer modules**, not only those its own dependency cone reaches.
- **A generated loop updates an answer module's state in place on the Rust backend.** The loop now hands the state out of the run for the length of one answer, and every function on the way to the answer takes the run by value, so a Map or Vector the state holds is no longer copied whole on every request. A process answering 2,000 requests from a module holding a 100,000-entry Map went from 0.76 s to 0.01 s.
- **`aver check .` checks a process that calls an operation of a capability under a subdirectory.** An answer module walked as the entry of its own program lent the batch its bare `module` name, which no program can import, and every process lost the capability's namespace (`unknown-ident 'Lib'`).
- **`aver effects --write` adds the in-place effects a process is missing.** A yielding function's list is still left alone for what it reaches through its stops, but what its body performs where it is written is added, as `aver check` requires.
- **A wasm-gc build no longer asks for equality on an answer module's state.** The list of answer tuples every tuple gets in case `List.zip` builds one demanded an equality helper for a state that has none (one holding a provider's resource, for example), and the build failed with `carrier eq inner type ... has no eq dispatch`.
- **An `answer-shape` warning is reported once**, by the answer module, not again by every module that imports it.
- **A capability loaded under a longer path that names its own type by its declared name (`Wire.Heard` inside `Slice.Wire`) means its own type** at every user, as it does when it is checked on its own.
- **`answer-shape` no longer warns about answer effects that return at once**, such as `Tcp.readNow`, `Tcp.writeNow`, `Tcp.accept`, `Time.unixMs` and a job kind's `begin` and `take`.
- **When a generated run ends, the jobs that parked requests wait on are cancelled**, so a job an answer module began itself no longer outlives the run.
Expand Down
4 changes: 2 additions & 2 deletions docs/language.md
Original file line number Diff line number Diff line change
Expand Up @@ -554,12 +554,12 @@ type Run.Pending

**What the compiler generates.** `AVER_YIELD_DUMP=1 aver check main.av --module-root .` prints all of it after the protocol. In outline:

- `__Process`, `__Slot`, `__Run`: the slot table (`Map<Int, __Slot>`), one field per answer module holding its state, per keyed process the keys it has seated and retired, the version of every answer module, the count of answers that arrived too late, the count of dropped instances, the stop flag, the clock reading and the next free id. A slot carries its instance number, its request, the wake it is parked on, `due` and `ms`, and the answer module and version a `Settled` wake waits on.
- `__Process`, `__Slot`, `__Run`: the slot table (`Map<Int, __Slot>`), one field per answer module holding its state as an `Option` (it is `None` only while one answer function holds the state), per keyed process the keys it has seated and retired, the version of every answer module, the count of answers that arrived too late, the count of dropped instances, the stop flag, the clock reading and the next free id. A slot carries its instance number, its request, the wake it is parked on, `due` and `ms`, and the answer module and version a `Settled` wake waits on.
- `__start`, `__seat<P>`, `__seatFamilies`, `__seatFamily<P>`: seating at start-up and at every turn boundary.
- `__current`, `__nextInstance`, `__settle<P>`, `__park`, `__bump`: the two invariants of the table. An answer that carries the current instance replaces that process's one slot and raises its number. An answer that carries an older one changes nothing and is counted. An `Err` parks the request where it stands and keeps the state the module returned.
- `__askable`, `__askableSlot`, `__deadlinePassed`, `__view`: the gate that decides which slots this turn may ask, and the view the policies read.
- `__waitPlan`, `__timeout`: the one wait of a turn, with one key per parked item, and its timeout: zero while some request can be asked already, the soonest deadline otherwise, and one second when nothing carries either.
- `__serve`, `__serve<P>`, `__serve<P><Kind>`: the dispatch, one arm per request kind of each process, which calls the answer module's own function and settles or parks on what it answered.
- `__serve`, `__serve<P>`, `__take<Module>`, `__serve<P><Kind>`: the dispatch, one arm per request kind of each process, which hands the answer module's state out of the run, calls the module's own function with it, and settles or parks on what it answered, writing the state it returned back. Handing the state out means the answer function holds the only reference to it, so a Map or Vector in it is updated in place rather than copied on every request, on the Rust backend in particular, where the run is moved from each of these functions to the next rather than borrowed.
- `__turn`, `__serveEach`, `__runAll`, `__all`, `main`: observe the stop flag, wait once, read the clock, serve every askable slot in slot order, seat the families, and repeat until the run is over.
- `__over`, `__cancelWaited`: the end of a run, which cancels every job a parked request is still waiting on.

Expand Down
10 changes: 9 additions & 1 deletion src/capability/work.rs
Original file line number Diff line number Diff line change
Expand Up @@ -816,7 +816,15 @@ pub fn check_answers(
let mut shapes = Vec::new();
for (module, group) in &modules {
let (shape, module_findings) = check_answer_module(registry, module, group, fn_sigs);
findings.extend(module_findings);
// A warning about an answer function is the answer module's own: it
// is reported when that module is checked, not again by every module
// of the program that can see it under its imported name.
let foreign = entry_module.is_some_and(|entry| entry != module.as_str());
findings.extend(
module_findings
.into_iter()
.filter(|finding| !(foreign && finding.severity == WorkSeverity::Warning)),
);
if let Some(shape) = shape {
shapes.push(shape);
}
Expand Down
2 changes: 2 additions & 0 deletions src/codegen/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4196,6 +4196,7 @@ mod tests {
program_shape: None,
mir_program: None,
bare_i64: Default::default(),
rust_owned_record_params: Default::default(),
discovered_lemmas: Vec::new(),
sample_expected: std::collections::HashMap::new(),
declined_cases: std::collections::HashMap::new(),
Expand Down Expand Up @@ -4321,6 +4322,7 @@ mod tests {
program_shape: None,
mir_program: None,
bare_i64: Default::default(),
rust_owned_record_params: Default::default(),
discovered_lemmas: Vec::new(),
sample_expected: std::collections::HashMap::new(),
declined_cases: std::collections::HashMap::new(),
Expand Down
1 change: 1 addition & 0 deletions src/codegen/lean/builtins.rs
Original file line number Diff line number Diff line change
Expand Up @@ -354,6 +354,7 @@ mod tests {
program_shape: None,
mir_program: None,
bare_i64: Default::default(),
rust_owned_record_params: Default::default(),
discovered_lemmas: Vec::new(),
sample_expected: std::collections::HashMap::new(),
declined_cases: std::collections::HashMap::new(),
Expand Down
1 change: 1 addition & 0 deletions src/codegen/lean/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ fn empty_ctx() -> CodegenContext {
program_shape: None,
mir_program: None,
bare_i64: Default::default(),
rust_owned_record_params: Default::default(),
discovered_lemmas: Vec::new(),
sample_expected: std::collections::HashMap::new(),
declined_cases: std::collections::HashMap::new(),
Expand Down
9 changes: 9 additions & 0 deletions src/codegen/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -499,6 +499,13 @@ pub struct CodegenContext {
/// Fail-closed: empty (all-`Boxed`) for hand-assembled test contexts
/// and for dependency-module fragments (callers unseen).
pub bare_i64: crate::ir::mir::BareI64Facts,
/// Record params the Rust backend takes by value because the function
/// consumes them: it returns the record, updates it at its last use, or
/// hands it at its last use to a callee that takes it by value. Indexed
/// by param position. Computed once by the Rust transpile after its MIR
/// rewrites, so every signature and every call site read the same
/// decision; empty (borrow by default) everywhere else.
pub rust_owned_record_params: HashMap<crate::ir::FnId, Vec<bool>>,
/// Kernel-proved lemmas parsed back from a committed
/// `DiscoveredLemmas.lean` (the `--discover` artifact), set by the CLI
/// on a normal `aver proof` run when the discovery-surface hash still
Expand Down Expand Up @@ -925,6 +932,7 @@ pub fn build_context(
synthesized_buffered_fns,
packed_sequence_layouts: HashMap::new(),
bare_i64,
rust_owned_record_params: Default::default(),
#[cfg(feature = "runtime")]
proof_ir: crate::ir::ProofIR::default(),
// Symbol table threaded through from the pipeline (or
Expand Down Expand Up @@ -1412,6 +1420,7 @@ pub(crate) fn empty_test_ctx() -> CodegenContext {
program_shape: None,
mir_program: None,
bare_i64: Default::default(),
rust_owned_record_params: Default::default(),
discovered_lemmas: Vec::new(),
sample_expected: std::collections::HashMap::new(),
declined_cases: std::collections::HashMap::new(),
Expand Down
2 changes: 1 addition & 1 deletion src/codegen/rust/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,7 @@ fn clear_owned_param_borrows(name: &str, mask: &mut [bool], ctx: &CodegenContext
let Some(mir_fn) = ctx.mir_program.as_ref().and_then(|p| p.fn_by_id(fn_id)) else {
return;
};
let owned = super::from_mir::owned_collection_param_names(mir_fn, &rfd.params);
let owned = super::from_mir::owned_collection_param_names(mir_fn, &rfd.params, ctx);
if owned.is_empty() {
return;
}
Expand Down
160 changes: 154 additions & 6 deletions src/codegen/rust/from_mir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -496,7 +496,8 @@ impl MirFnEmitPolicy {
/// refinement requires an owned carrier instead: non-final uses clone,
/// final uses move, and Map/Vector mutators preserve retained aliases via
/// COW. Missing facts remain flagged and keep borrow-by-default.
pub(super) fn apply_own_param(&mut self, mir_fn: &crate::ir::mir::MirFn) {
pub(super) fn apply_own_param(&mut self, mir_fn: &crate::ir::mir::MirFn, ctx: &CodegenContext) {
let consumed = ctx.rust_owned_record_params.get(&mir_fn.fn_id);
for (i, param) in mir_fn.params.iter().enumerate() {
// Only collection params are candidates (the only thing
// `own_param`'s RULE 1 ever flags). A non-collection param is
Expand All @@ -510,7 +511,8 @@ impl MirFnEmitPolicy {
continue;
};
let returned_record_successor = matches!(ty, Type::Named { .. })
&& result_contains_record_successor_of(&mir_fn.body.node, param.local);
&& (result_contains_record_successor_of(&mir_fn.body.node, param.local)
|| consumed.and_then(|owned| owned.get(i)).copied() == Some(true));
// `own_param`'s `prone`/clearing both index `aliased_slots`
// by PARAM POSITION `i` (its `(0..nparams).filter(|&i| …)`),
// matching `MirParam.local = LocalId(i)`; match that exactly.
Expand Down Expand Up @@ -610,13 +612,15 @@ fn result_contains_record_successor_of(expr: &MirExpr, slot: LocalId) -> bool {
pub(super) fn owned_collection_param_names(
mir_fn: &crate::ir::mir::MirFn,
param_types: &[(String, Type)],
ctx: &CodegenContext,
) -> HashSet<String> {
let consumed = ctx.rust_owned_record_params.get(&mir_fn.fn_id);
let mut out = HashSet::new();
for (i, (name, ty)) in param_types.iter().enumerate() {
let returned_record_successor = matches!(ty, Type::Named { .. })
&& mir_fn.params.get(i).is_some_and(|param| {
&& (mir_fn.params.get(i).is_some_and(|param| {
result_contains_record_successor_of(&mir_fn.body.node, param.local)
});
}) || consumed.and_then(|owned| owned.get(i)).copied() == Some(true));
let collection_graduated = is_owned_collection_candidate(ty)
&& !mir_fn.aliased_slots.get(i).copied().unwrap_or(true);
if !collection_graduated && !returned_record_successor {
Expand All @@ -627,6 +631,150 @@ pub(super) fn owned_collection_param_names(
out
}

/// Which record params of every function the Rust backend takes by value.
///
/// A record param is borrowed by default, so a function that consumes it
/// clones it first, and while that clone is alive the caller's copy still
/// holds every Map and Vector the record carries. A later in-place update of
/// one of them then copies it whole. A function consumes a param when it
/// updates it at its last use or hands it at its last use to a callee that
/// takes it by value; taking such a param by value lets a chain
/// of calls move one record from caller to callee, which is what keeps the
/// state a generated loop hands an answer module uniquely owned.
///
/// The facts are a least fixpoint over the program: a callee taking a param
/// by value is what makes passing it at the last use a consumption. A
/// self-tail-recursive function already takes every param by value; a mutual
/// tail-call group keeps its borrowing wrappers and is never a by-value
/// callee here.
pub(super) fn compute_owned_record_params(
ctx: &CodegenContext,
) -> HashMap<crate::ir::FnId, Vec<bool>> {
let mut owned: HashMap<crate::ir::FnId, Vec<bool>> = HashMap::new();
let Some(program) = ctx.mir_program.as_ref() else {
return owned;
};
let mut candidates: Vec<(crate::ir::FnId, Vec<usize>)> = Vec::new();
for (id, mir_fn) in program.iter() {
let Some(resolved) = ctx.resolved_program.fn_by_id(*id) else {
continue;
};
if ctx.mutual_tco_members.contains(id) {
continue;
}
if super::toplevel::resolved_fn_has_self_tailcall(resolved) {
owned.insert(*id, vec![true; resolved.params.len()]);
continue;
}
let by_value = owned_collection_param_names(mir_fn, &resolved.params, ctx);
let mut abi = Vec::with_capacity(resolved.params.len());
let mut open = Vec::new();
for (i, (name, ty)) in resolved.params.iter().enumerate() {
let taken = !should_borrow_param(ty) || by_value.contains(&aver_name_to_rust(name));
if !taken && matches!(ty, Type::Named { .. }) && mir_fn.params.get(i).is_some() {
open.push(i);
}
abi.push(taken);
}
owned.insert(*id, abi);
if !open.is_empty() {
candidates.push((*id, open));
}
}
loop {
let mut graduated = Vec::new();
for (id, open) in &candidates {
let Some(mir_fn) = program.fn_by_id(*id) else {
continue;
};
for &i in open {
if owned[id][i] {
continue;
}
let slot = mir_fn.params[i].local;
if consumes_local(&mir_fn.body.node, slot, &owned) {
graduated.push((*id, i));
}
}
}
if graduated.is_empty() {
break;
}
for (id, i) in graduated {
if let Some(abi) = owned.get_mut(&id) {
abi[i] = true;
}
}
}
owned
}

/// Whether `expr` consumes the local in `slot`: updates it as the base of a
/// record update at its last use, or passes it at its last use to a callee
/// position `owned` says is by value. Returning it bare is not a consumption:
/// a function that only hands its param back keeps borrowing it.
fn consumes_local(
expr: &MirExpr,
slot: LocalId,
owned: &HashMap<crate::ir::FnId, Vec<bool>>,
) -> bool {
let last_use_of =
|arg: &MirExpr| local_of(arg).is_some_and(|local| local.slot == slot && local.last_use);
let by_value = |callee: crate::ir::FnId, index: usize| {
owned
.get(&callee)
.and_then(|abi| abi.get(index))
.copied()
.unwrap_or(false)
};
match expr {
MirExpr::Call(call) => {
if let MirCallee::Fn(callee) = call.node.callee
&& call
.node
.args
.iter()
.enumerate()
.any(|(index, arg)| last_use_of(&arg.node) && by_value(callee, index))
{
return true;
}
call.node
.args
.iter()
.any(|arg| consumes_local(&arg.node, slot, owned))
}
MirExpr::TailCall(call) => {
call.node
.args
.iter()
.enumerate()
.any(|(index, arg)| last_use_of(&arg.node) && by_value(call.node.target, index))
|| call
.node
.args
.iter()
.any(|arg| consumes_local(&arg.node, slot, owned))
}
MirExpr::RecordUpdate(update) => {
last_use_of(&update.node.base.node)
|| consumes_local(&update.node.base.node, slot, owned)
|| update
.node
.updates
.iter()
.any(|field| consumes_local(&field.value.node, slot, owned))
}
_ => {
let mut found = false;
crate::ir::mir::expr::walk_children(expr, &mut |child| {
found = found || consumes_local(child, slot, owned);
});
found
}
}
}

/// The legacy representation-backed `Tcp.Connection` carrier maps to its
/// flat root alias. Capability-owned represented records such as
/// `Terminal.Size` take the ordinary module-qualified path below.
Expand Down Expand Up @@ -3573,7 +3721,7 @@ pub(super) fn emit_mir_fn_body_routed(
// SIGNATURE (`emit_fn_def_with_visibility`) computes the SAME owned
// set from the same `mir_fn.aliased_slots` and emits `mut p: T`, so
// body and signature agree on which params are owned.
policy.apply_own_param(mir_fn);
policy.apply_own_param(mir_fn, ctx);
// Apply the Int unboxing facts so a proven-bare slot emits native
// `i64`. Same per-fn slice the signature emit reads (via
// `bare_fn_facts`), so body and signature agree on which params /
Expand Down Expand Up @@ -3677,7 +3825,7 @@ pub(super) fn emit_mir_tco_fn(
// a structural TCO decision that takes precedence, so drop any
// rc-wrapped name back out of `owned_params` to keep signature and
// body consistent.
policy.apply_own_param(mir_fn);
policy.apply_own_param(mir_fn, ctx);
// Int unboxing: a bare `i64` counter param is `Copy`-by-value, so it
// is never rc-wrapped — a param bare in the summary is disjoint from
// `rc_wrapped` by construction (rc only wraps non-Copy pass-through
Expand Down
1 change: 1 addition & 0 deletions src/codegen/rust/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,7 @@ fn transpile_project(
ctx.mir_program = Some(
crate::ir::mir::optimize::bare_i64_rewrite::rewrite_for_rust(prog, &boxed, &carrier),
);
ctx.rust_owned_record_params = from_mir::compute_owned_record_params(ctx);
}
let has_embedded_policy = ctx.policy.is_some();
let has_runtime_policy = ctx.runtime_policy_from_env;
Expand Down
Loading
Loading