detcore_model/
replay_departure.rs

1/*
2 * Copyright (c) Meta Platforms, Inc. and affiliates.
3 * All rights reserved.
4 *
5 * This source code is licensed under the BSD-style license found in the
6 * LICENSE file in the root directory of this source tree.
7 */
8
9//! Bounded observations of a faithful preemption replay leaving its history.
10//! These observations do not establish a timer cause or a common replay prefix.
11
12use serde::Deserialize;
13use serde::Serialize;
14
15use crate::pid::DetTid;
16use crate::time::LogicalTime;
17
18/// The production point that observed a nonadvancing change point.
19#[derive(Clone, Copy, Debug, Deserialize, Eq, PartialEq, Serialize)]
20pub enum Source {
21    /// The thread could not file its next change point.
22    ThreadFiling,
23    /// The scheduler omitted a change point from its output history.
24    SchedulerChangePoint,
25}
26
27/// One observed change point, with coordinates from the observing run.
28#[derive(Clone, Debug, Deserialize, Eq, PartialEq, Serialize)]
29pub struct Finding {
30    /// The production observer, selected by the coordinator.
31    pub source: Source,
32    /// The authenticated thread, not an independently supplied payload ID.
33    pub thread: DetTid,
34    /// The preceding change point's logical time.
35    pub previous: LogicalTime,
36    /// The new change point's logical time, at or before `previous`.
37    pub observed: LogicalTime,
38    /// The thread's slice counter where the thread itself observed the finding.
39    pub slice: Option<u64>,
40    /// The new recording's observed event count at acceptance, if recording.
41    /// This is not an input-history index or an exact common-prefix length.
42    pub recorded_event_count: Option<u64>,
43}
44
45/// A bounded run diagnostic: detections are counted, only the first is retained.
46#[derive(Clone, Debug, Deserialize, Eq, PartialEq, Serialize)]
47pub struct Summary {
48    /// Number of accepted detections, not distinct physical causes.
49    pub count: u64,
50    /// The first accepted observation in the run's deterministic order.
51    pub first: Finding,
52}
detcore_model/replay_departure.rs

detcore_model/
replay_departure.rs
