Skip to content
Open
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
7 changes: 7 additions & 0 deletions .github/workflows/pyre-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -446,6 +446,13 @@ jobs:
--lib -- --ignored --test-threads=1 \
compiler::tests::test_host_loop_external_jump_to

- name: Run cel's release-only probe gates (Linux only)
# Debug builds ignore these tests because their arithmetic is intentionally
# wrapping. Run only their correctness gates here; benchmark loops remain
# available through `cargo run -p cel --release`.
if: runner.os == 'Linux'
run: cargo test --release -p cel --no-default-features --features dynasm

# The CPython suite rides this job's Linux copy rather than a job of its
# own: it needs the same checkout, toolchain, Cargo cache and prepared
# Charon/LLBC set, and those cost a job's worth of setup to assemble a
Expand Down
9 changes: 7 additions & 2 deletions AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -194,8 +194,13 @@ comment at the site citing both sides.

## Before committing

- `cargo test --all --features dynasm`. The feature flag is mandatory: without it
`majit-metainterp` emits `compile_error!` and every error after it is noise.
- `cargo test --all --no-default-features --features dynasm`. Both halves matter.
`--features dynasm` selects a backend; `--no-default-features` is what keeps the
selection consistent across crates. With default features on, the workspace's
example interpreters default to `cranelift` and supply it to the one shared
`majit-metainterp`, while `pyre-jit` compiles in its dynasm registrations — so
the binary dispatches through one backend and holds the other's hooks. Nothing
emits an error; the tests simply run against a mismatched pair.
- `python3 pyre/check.py` — every backend the host can build. A perf regression
is a finding to explain, not an automatic veto: if the slower code is the
line-by-line port and the faster was a shortcut, **the port stands** — record
Expand Down
19 changes: 16 additions & 3 deletions majit/charon-corpus/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,8 @@ out in issue #97:

The corpus also includes a header-first object model. These functions pin
lowering decisions that otherwise fail by leaving a residual call or an
untyped field access rather than raising an error:
untyped field access rather than raising an error, so each is pinned by an
assertion in `majit-translate/tests/test_mir_frontend.rs`:

| Function | Premise it pins |
|-----------------------|-------------------------------------------------------|
Expand All @@ -97,11 +98,23 @@ only data field is `typeptr`. The two-word allocation can fuse when its
allocation can fuse from its declared layout because no class word exists to
disagree with the type pointer.

Both shapes are carried because `resolve_header_plan` has an arm for each, and
a corpus holding only the two-word shape can never reach the second: the match
lands on the stored `w_class` before `header_declares_no_class_word` is
consulted.

The fixture spells `pyre_object::pyobject::get_instantiate` literally because
`model.rs` currently recognises that path suffix. The one-word header does not
use this helper. `_immutable_fields_W_IntObject` preserves the marker shape
harvested by `front::llbc_hints`.

harvested by `front::llbc_hints`; `lower_function` runs upstream of that
consumer, so no assertion in `test_mir_frontend.rs` covers it. Every other
identity in the corpus is named after no host, so a fixture cannot tell a
general recogniser apart from one conformed to a particular host.

`corpus.ullbc` is regenerated in place whenever this fixture is edited, and it
embeds the source verbatim, so counts taken against an older artefact — op
censuses, lowered-graph totals, local-fn counts — are not comparable across a
regeneration. Re-measure rather than subtract.

## Findings

Expand Down
93 changes: 68 additions & 25 deletions majit/examples/cel/src/colscalar.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,8 @@
//! Diagnostic: does a SCALAR `int` state-field base for raw_load compile, and
//! does WRITING that field every iteration (as the wasmi kernel does with
//! `state.mem_base = __mb`) change the outcome vs a READ-ONLY scalar field?
//!
//! The `column` probe proved base-in-REGISTER compiles (13-16x). This isolates the
//! VirtualStatesCantMatch root cause: base-in-SCALAR-FIELD. Two programs,
//! identical except one re-writes the scalar field each iteration.
//! RDONLY keeps `state.col_base` read-only after initialization; WRITTEN
//! reassigns it from a register every iteration.
//! Prints compiles/aborts for each. RELEASE ONLY.
//! Raw-load regression probe with the base address in a scalar `int` state
//! field. One program reads a base initialized before the loop; the other
//! rewrites the same field on every iteration. Both must compile. This protects
//! `VirtualizableConfig::identity_input_index`: treating scalar input slot 0 as
//! the virtualizable identity makes the read-only variant fail loop closing.

use crate::common::*;
use std::sync::atomic::Ordering;
Expand All @@ -23,6 +18,14 @@ const OP_SET_BASE: i64 = 6; // [SET_BASE, src_reg] state.col_base = regs[src]
struct VmState {
regs: Vec<i64>,
col_base: i64,
/// What `OP_RETURN` hands back.
///
/// The `; state` merge point leaves the loop through `break` before it
/// assigns the walk's resume pc, so after the loop `pc` still names the
/// position the walk started from and `program[pc + 1]` — the operand
/// saying which register holds the result — cannot be read there. The
/// result has to arrive in `state`.
ret: i64,
}

#[majit_macros::jit_interp(
Expand All @@ -32,6 +35,7 @@ struct VmState {
state_fields = {
regs: [int; virt],
col_base: int,
ret: int,
},
)]
fn mainloop(program: &Code, num_regs: usize, col_base: i64, threshold: u32) -> i64 {
Expand All @@ -48,6 +52,7 @@ fn mainloop(program: &Code, num_regs: usize, col_base: i64, threshold: u32) -> i
let mut state = VmState {
regs: vec![0; num_regs],
col_base,
ret: 0,
};

{
Expand All @@ -58,7 +63,11 @@ fn mainloop(program: &Code, num_regs: usize, col_base: i64, threshold: u32) -> i
}

loop {
jit_merge_point!();
// `; state` selects the single-executor close: the walk's final state is
// transferred into `state` here and the native loop resumes at the close
// pc, instead of discarding the walk outcome and re-running the circuit
// the walk already executed.
jit_merge_point!(driver, program, pc; state);
let opcode = program[pc];
match opcode {
OP_LOAD => {
Expand Down Expand Up @@ -106,14 +115,29 @@ fn mainloop(program: &Code, num_regs: usize, col_base: i64, threshold: u32) -> i
}
pc += 4;
}
// Stores into `ret` and then leaves through an in-arm `return`,
// never `{ store; break }`: `classify.rs` `is_break_expr` requires
// the arm body to be exactly `break`, so a composite body classifies
// `Lowerable` and its tail `break` reaches `lower_stmt_fallback`,
// which guards an enclosed `return` but not an enclosed `break` —
// the statement is inert and is silently dropped, leaving the
// lowered arm to fall through to the dispatch back-edge.
OP_RETURN => {
let r = program[pc + 1] as usize;
return state.regs[r];
state.ret = state.regs[r];
return state.ret;
}
_ => break,
// Was `_ => break` with the panic below the loop. The loop now has a
// second way out — the merge point's own `break` on a walk that
// reached a terminal return — so falling out of it no longer
// identifies a bad opcode, and the panic moves into the arm that
// actually saw one.
_ => panic!("fell off end of code"),
}
}
panic!("fell off end of code");
// Reached only when the merge point broke out on a walk that already ran the
// terminal opcode, so the result is whatever that opcode parked in `ret`.
state.ret
}

fn clean_interp(program: &Code, num_regs: usize, col_base: i64) -> i64 {
Expand Down Expand Up @@ -266,7 +290,14 @@ fn make_col(n: i64) -> Vec<i64> {
v
}

fn run_case(label: &str, prog: &[i64], col_base: i64) {
/// One case's correctness + tier-liveness gate. There is no timing half in this
/// probe — it reports compile/abort counts, not ns/row — so this is the whole
/// of the work `run` does.
///
/// `on_c >= 1` says a trace was minted for the case's loop. It does not say the
/// trace has a real body (an empty dispatch still compiles a bare `Finish()`),
/// so it is the liveness half only.
fn gate_case(label: &str, prog: &[i64], col_base: i64) {
COMPILES.store(0, Ordering::Relaxed);
ABORTS.store(0, Ordering::Relaxed);
let clean = clean_interp(prog, NUM_REGS, col_base);
Expand All @@ -279,23 +310,35 @@ fn run_case(label: &str, prog: &[i64], col_base: i64) {
let on_a = ABORTS.load(Ordering::Relaxed);
assert_eq!(clean, off, "{label}: clean vs off");
assert_eq!(clean, on, "{label}: clean vs on -> miscompile");
let verdict = if on_c >= 1 {
"COMPILES"
} else {
"ABORTS (never compiles)"
};
println!("[{label}] compiles: off={off_c} on={on_c} aborts(on)={on_a} -> {verdict}");
assert_eq!(off_c, 0, "{label}: JIT-off must never compile");
// Was a printed verdict — "COMPILES" / "ABORTS (never compiles)" — because
// RDONLY genuinely never compiled before the `identity_input_index` fix the
// header describes. Both cases compile now, so the outcome the probe exists
// to watch is a fixed one and belongs in an assertion: a printed verdict
// cannot fail a run, and the two equality gates above stay green with the
// JIT tier entirely inert.
assert!(
on_c >= 1,
"{label}: JIT-on compiled nothing (aborts={on_a}) — the scalar-field \
base no longer closes the trace"
);
println!("[{label}] compiles: off={off_c} on={on_c} aborts(on)={on_a}");
}

pub fn run() {
/// Both cases' gates. This is the whole probe; `run` adds only the banner.
pub(crate) fn run_gates() {
let n: i64 = std::env::var("CELN")
.ok()
.and_then(|s| s.parse().ok())
.unwrap_or(300_000);
let col = make_col(n);
let base = col.as_ptr() as i64;
println!("scalar-int-state-field base for raw_load: read-only vs written\n");
run_case("RDONLY ", &rdonly_program(n), base);
run_case("WRITTEN", &written_program(n, base), base);
gate_case("RDONLY ", &rdonly_program(n), base);
gate_case("WRITTEN", &written_program(n, base), base);
std::hint::black_box(&col);
}

pub fn run() {
println!("scalar-int-state-field base for raw_load: read-only vs written\n");
run_gates();
}
Loading
Loading