Module happens_before 

Happens-before edges: a sparse, authored partial order over dynamic events.

Where --replay-schedule-from replays a complete total order captured from a prior run, a happens-before specification pins down only the few events that matter for a race and lets the deterministic scheduler fill in the rest. An agent (or human) that already knows a target race can therefore construct it deterministically instead of blind seed-search.

Model

An Anchor names a precise, deterministic per-thread stop point. Following the owner’s refinement of RFC #1146, the primary addressing is a Position — “after N syscalls” or “after M retired conditional branches (RCBs)” on a specific thread — optionally decorated with a CodeLocation (function and/or source line, resolved from debug info) for readability. The RFC’s richer addressing modes (Nth occurrence of a named syscall, RIP hit, or function entry) remain expressible but are deliberately not the lead addressing scheme.

A HappensBeforeEdge states that one anchor must be observed before another thread is allowed to proceed past its anchor. A HappensBeforeSpec is the whole authored partial order: a table of named threads, a table of named events (anchors), and the edge list connecting them.

This module owns the model only: parsing (JSON and a terse DSL), normalization, and static validation (name resolution, exactly-one-position, and cycle detection). Resolving a CodeLocation to a concrete address via debug info, and enforcing edges in the scheduler, live in higher layers.

Structs

Anchor

A fully normalized anchor: a named, deterministic per-thread stop point.

CodeLocation

A source-level location, resolvable to/from an address via debug info.

EdgeSpec

One ordering constraint: before happens-before after.

EventSpec

A single named event (anchor) in the declarative format.

HappensBeforeEdge

A normalized happens-before edge between two anchors.

HappensBeforeProgram

A validated, normalized happens-before program: anchors indexed by name plus the edge list, guaranteed acyclic with all references resolved.

HappensBeforeSpec

The declarative happens-before specification, as read from a JSON file or desugared from the terse DSL. This mirrors the reviewed RFC #1146 file format verbatim so an authored file round-trips.

HbThreadCounters

One thread’s happens-before counting state: its occurrence counters, and for each relative anchor whose base this thread has reached, the origin: the count of the relative anchor’s counter just after the base entry. Belongs to the thread, like its syscall count: empty for a new thread, kept across the thread’s own exec.

ThreadRef

A resolved reference to a thread.

ThreadSpec

How a symbolic thread label resolves to a concrete DetTid.

Enums

HappensBeforeError

An error produced while parsing or validating a happens-before specification.

PhaseSpec

Serializable mirror of SyscallPhase using lowercase author-friendly names.

Position

The deterministic per-thread stop point that an anchor addresses.

Strength

How strictly an edge is enforced by the scheduler.

Constants

DEFAULT_MAX_HOLD_NS

The hold budget of a version-2 spec that sets no max_hold_ns: 10 s of virtual time.

HAPPENS_BEFORE_VERSION

The newest schema version understood by this build. Version 2 adds relative anchors (from), the futex_op filter and the hold budget (max_hold_ns); version 1 files load unchanged, with their old semantics. A build that understands only version 1 refuses a version-2 file instead of silently dropping the fields it does not know.

HAPPENS_BEFORE_VERSION_1

The original schema version, still accepted. It may not use any field that version 2 added (HappensBeforeError::NewFieldInVersion1).

Functions

syscall_never_reaches_tracer

True for a syscall that never reaches Hermit’s tracer on the ptrace backend, whatever Detcore subscribes to: Reverie lets rt_sigreturn run untraced from its private page so a signal frame is restored safely. A syscall anchor on one could never fire, so the run refuses it.

syscall_never_returns_on_success

True for a syscall that does not return to its caller when it succeeds: the exec family replaces the image, and the exit family ends the thread. A posthook anchor on one is refused at load.

syscall_takes_fd_first

True when sysno’s first argument is a file descriptor, so an anchor may restrict it with fd. The list is the fd-first syscalls a guest is likely to anchor on; an fd on any other syscall is refused when the spec is loaded rather than matched against an argument that is not a descriptor.

Type Aliases

OccurrenceCounters

One thread’s syscall-occurrence counters (HappensBeforeProgram::count_syscall_occurrences).

OccurrenceKey

The key of one per-thread occurrence counter: a syscall number, an optional file descriptor and an optional futex operation (Anchor::occurrence_key).