Checkers and reports

Import the synchronization checker (synccheck) and memory-race checker (racecheck) from tirx_harness. Both execute on the CPU for a concrete kernel invocation. Their guarantees and limitations are described in Compiler analysis.

Entry points

Pass a specialized TIRx function as kernel; for a TIRx-lite kernel, use kernel.func. Bind all runtime parameters by name in inputs, including output buffers. Buffer bindings are CPU NumPy arrays; scalar parameters take concrete scalar values. Only parameterless kernels may omit the bindings. Tensor-map parameters use tirx_harness.numsim.TensorMap.numpy().

tirx_harness.synccheck(kernel: tvm_tirx.tirx.Function, inputs: dict | None = None)

Run native synchronization analysis for one concrete TIRx invocation.

Returns a SyncCheckReport.

tirx_harness.racecheck(kernel: tvm_tirx.tirx.Function, inputs: dict | None = None)

Run native data-race analysis for one concrete TIRx invocation.

Returns a RaceReport.

Reports

Inspect report.verdict and report.findings, save report.to_dict(), or call report.print() for readable evidence. report.require_clean() raises a RuntimeError subclass unless the verdict is clean.

Verdict

Meaning

clean

The invocation passed within the checker’s supported model and coverage.

review

An advisory needs investigation.

incomplete

Missing bindings, unsupported behavior, or a coverage limit prevented a complete check.

error

The checker detected a violation.

Each finding has id, status, kind, message, and details fields, plus to_dict() for serialization. Details carry available source and witness evidence. A clean report applies to the supplied specialization, launch, and inputs; see the checker scope.

The following classes are return types; obtain them from the entry points above.

class tirx_harness.numsim.checker_report.SyncCheckReport(native_payload: dict[str, Any])

Public report for one native Synccheck execution.

to_dict() → dict[str, Any]
format() → str
property verdict: str
print() → None
property findings: list[Finding]
require_clean() → None
class tirx_harness.numsim.checker_report.RaceReport(native_payload: dict[str, Any])

Public report for one native Racecheck execution.

format() → str
property verdict: str
to_dict() → dict[str, Any]
print() → None
property findings: list[Finding]
require_clean() → None