Struct HappensBeforeSpec 

pub struct HappensBeforeSpec {
    pub version: u32,
    pub max_hold_ns: Option<u64>,
    pub threads: BTreeMap<String, ThreadSpec>,
    pub events: BTreeMap<String, EventSpec>,
    pub edges: Vec<EdgeSpec>,
}

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.

Fields

version: u32

Schema version: HAPPENS_BEFORE_VERSION_1 or HAPPENS_BEFORE_VERSION.

max_hold_ns: Option<u64>

Version 2 only: how long a thread may stay held at a gate, in committed virtual nanoseconds, before the run is refused (HERMIT_HB_HOLD_BUDGET_EXCEEDED). Defaults to DEFAULT_MAX_HOLD_NS.

threads: BTreeMap<String, ThreadSpec>

Symbolic thread labels mapped to a resolution rule, so authors need not hard-code raw DetTids.

events: BTreeMap<String, EventSpec>

Named events (anchors). Naming events separately from edges lets one event participate in several edges and keeps the edge list readable.

edges: Vec<EdgeSpec>

The partial order itself.

Implementations

impl HappensBeforeSpec

pub fn from_json(s: &str) -> Result<HappensBeforeSpec>

Parse a JSON specification. A version-2 spec is also checked for fields this build does not know (HappensBeforeError::UnknownField), so a misspelled field is refused instead of silently ignored; version 1 keeps its old, lenient handling of unknown fields.

The spec itself is deserialized from the original text, not from the Value used for that check: a Value keeps only the last of two equal keys, which would accept "nth": 1, "nth": 2 as nth 2. Deserializing the text refuses a duplicated field, in either version.

pub fn to_json(&self) -> Result<String>

Serialize to pretty JSON.

pub fn normalize(&self) -> Result<HappensBeforeProgram, HappensBeforeError>

Normalize and statically validate: check the version, resolve thread and event references, require exactly one position per event, parse syscalls and RIPs, and confirm the edge graph is acyclic.

impl HappensBeforeSpec

pub fn from_dsl(input: &str) -> Result<HappensBeforeSpec, HappensBeforeError>

Parse the terse line-oriented DSL into a specification. Symbolic threads mentioned by name become entries in the threads table.

Trait Implementations

impl Clone for HappensBeforeSpec

fn clone(&self) -> HappensBeforeSpec

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for HappensBeforeSpec

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for HappensBeforeSpec

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for HappensBeforeSpec

impl PartialEq for HappensBeforeSpec

fn eq(&self, other: &HappensBeforeSpec) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for HappensBeforeSpec

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for HappensBeforeSpec