Path：路径与深度优先

pub(crate) struct Path {
    preemption_bound: Option<u8>,
    pos: usize,
    branches: object::Store<Entry>,
    exploring: bool,
    skipping: bool,
    exploring_on_start: bool,
}

pub(crate) struct Schedule {
    preemptions: u8,
    initial_active: Option<u8>,
    threads: [Thread; MAX_THREADS],
    prev: Option<object::Ref<Schedule>>,
    exploring: bool,
}

pub(crate) struct Load {
    values: [u8; MAX_ATOMIC_HISTORY],
    pos: u8,
    len: u8,
    exploring: bool,
}

pub(crate) struct Spurious {
    spur: bool,
    exploring: bool,
}

pub(super) fn is_traversed(&self) -> bool {
    self.pos == self.branches.len()
}

pub(super) fn branch_thread(
    &mut self,
    execution_id: execution::Id,
    seed: impl ExactSizeIterator<Item = Thread>,
) -> Option<thread::Id> {
    if self.is_traversed() {
        assert_path_len!(self.branches);

        // 用 seed 新建一个 Schedule：调用方算好的「默认线程」是 Active，
        // 其余按能不能跑分成 Skip / Yield / Disabled
        // …
    }

    let schedule = object::Ref::from_usize(self.pos)
        .downcast::<Schedule>(&self.branches)
        .expect("Reached unexpected exploration state. Is the model fully deterministic?")
        .get(&self.branches);

    self.pos += 1;

    schedule
        .threads
        .iter()
        .enumerate()
        .find(|&(_, th)| th.is_active())
        .map(|(i, _)| thread::Id::new(execution_id, i))
}

let round = ROUND.fetch_add(1, SeqCst);   // std 原子，跨轮保留
let a: &'static AtomicUsize = Box::leak(Box::new(AtomicUsize::new(0)));
if round == 0 {
  a.load(Relaxed);                         // 只有第 0 轮多一个 Schedule + 一个 Load
}
let t = thread::spawn(move || a.store(1, Relaxed));
a.store(2, Relaxed);
t.join().unwrap();

Reached unexpected exploration state. Is the model fully deterministic?

pub(super) fn step(&mut self) -> bool {
    self.pos = 0;
    self.exploring = self.exploring_on_start;
    self.skipping = false;

    for last in (0..self.branches.len()).rev() {
        let last = object::Ref::from_usize(last);

        // Remove all objects that were created **after** this branch
        self.branches.truncate(last);

        if let Some(schedule_ref) = last.downcast::<Schedule>(&self.branches) {
            let schedule = schedule_ref.get_mut(&mut self.branches);

            if !schedule.exploring {
                continue;
            }

            // Transition the active thread to visited.
            if let Some(thread) = schedule.threads.iter_mut().find(|th| th.is_active()) {
                *thread = Thread::Visited;
            }

            // Find a pending thread and transition it to active
            let rem = schedule
                .threads
                .iter_mut()
                .find(|th| th.is_pending())
                .map(|th| {
                    *th = Thread::Active;
                })
                .is_some();

            if rem {
                return true;
            }
        } else if let Some(load_ref) = last.downcast::<Load>(&self.branches) {
            let load = load_ref.get_mut(&mut self.branches);

            if !load.exploring {
                continue;
            }

            load.pos += 1;

            if load.pos < load.len {
                return true;
            }
        } else if let Some(spurious_ref) = last.downcast::<Spurious>(&self.branches) {
            let spurious = spurious_ref.get_mut(&mut self.branches);

            if !spurious.exploring {
                continue;
            }

            if !spurious.spur {
                spurious.spur = true;
                return true;
            }
        } else {
            unreachable!();
        }
    }

    false
}

macro_rules! assert_path_len {
    ($branches:expr) => {{
        assert!(
            // if we are panicking, we may be performing a branch due to a
            // `Drop` impl (e.g., for `Arc`, or for a user type that does an
            // atomic operation in its `Drop` impl). if that's the case,
            // asserting this again will double panic. therefore, short-circuit
            // the assertion if the thread is panicking.
            $branches.len() < $branches.capacity() || std::thread::panicking(),
            "Model exceeded maximum number of branches. This is often caused \
             by an algorithm requiring the processor to make progress, e.g. \
             spin locks.",
        );
    }};
}

{
  "preemption_bound": null,
  "pos": 0,
  "branches": { "entries": [
    { "Schedule": { "preemptions": 0, "initial_active": 0, "threads": ["Active", …], "prev": null, "exploring": true } },
    { "Schedule": { "preemptions": 0, "initial_active": 0, "threads": ["Active", …], "prev": { "index": 0, "_p": null }, "exploring": true } },
    { "Schedule": { "preemptions": 0, "initial_active": 0, "threads": ["Visited", "Active", …], "prev": { "index": 1, "_p": null }, "exploring": true } },
    { "Schedule": { "preemptions": 1, "initial_active": 1, "threads": ["Active", "Visited", …], "prev": { "index": 2, "_p": null }, "exploring": true } }
  ] },
  "exploring": true,
  "skipping": false,
  "exploring_on_start": true
}