todc_utils/specifications/
snapshot.rs

1//! A sequential specification of a [snapshot object](https://en.wikipedia.org/wiki/Shared_snapshot_objects).
2use core::array::from_fn;
3use std::fmt::Debug;
4use std::hash::Hash;
5use std::marker::PhantomData;
6
7use crate::specifications::Specification;
8
9use SnapshotOperation::{Scan, Update};
10
11/// A process identifier.
12pub type ProcessId = usize;
13
14/// An operation for a snapshot object.
15#[derive(Debug, Copy, Clone)]
16pub enum SnapshotOperation<T, const N: usize> {
17    /// Scan the object and return an view containing the values in each component.
18    ///
19    /// If the return value of a scan is not-yet-known, this can be represented
20    /// as `Scan(pid, None)`.
21    Scan(ProcessId, Option<[T; N]>),
22    /// Update the component of the object belonging to this process.
23    Update(ProcessId, T),
24}
25
26/// A specification of an `N`-process [snapshot object](https://en.wikipedia.org/wiki/Shared_snapshot_objects).
27///
28/// Each component of the snapshot contains a value of type `T`.
29pub struct SnapshotSpecification<T: Clone + Debug + Default + Eq + Hash, const N: usize> {
30    data_type: PhantomData<T>,
31}
32
33impl<T: Clone + Debug + Default + Eq + Hash, const N: usize> Specification
34    for SnapshotSpecification<T, N>
35{
36    type State = [T; N];
37    type Operation = SnapshotOperation<T, N>;
38
39    fn init() -> Self::State {
40        from_fn(|_| T::default())
41    }
42
43    fn apply(operation: &Self::Operation, state: &Self::State) -> (bool, Self::State) {
44        match operation {
45            Scan(_, result) => match result {
46                Some(view) => (view == state, state.clone()),
47                None => panic!("Cannot apply Scan with an unknown return value."),
48            },
49            Update(i, value) => {
50                let mut new_state = state.clone();
51                new_state[*i] = value.clone();
52                (true, new_state)
53            }
54        }
55    }
56}
57
58#[cfg(test)]
59mod tests {
60    use super::{SnapshotOperation::*, SnapshotSpecification, Specification};
61
62    type Spec = SnapshotSpecification<u32, 3>;
63
64    mod init {
65        use super::*;
66
67        #[test]
68        fn returns_array_of_defaults() {
69            let state = Spec::init();
70            assert_eq!(state, [u32::default(), u32::default(), u32::default()]);
71        }
72    }
73
74    mod apply {
75        use super::*;
76
77        type Value = u32;
78        const NUM_PROCESSES: usize = 3;
79
80        #[test]
81        fn update_applied_to_proper_component() {
82            let id = 1;
83            let value = 123;
84            let (_, new_state) = Spec::apply(&Update(id, value), &Spec::init());
85            assert_eq!(new_state[id], value);
86            for i in [0, 2] {
87                assert_eq!(new_state[i], Value::default());
88            }
89        }
90
91        #[test]
92        fn update_always_valid() {
93            for i in 0..NUM_PROCESSES {
94                let (valid, _) = Spec::apply(&Update(i, i as u32), &Spec::init());
95                assert!(valid);
96            }
97        }
98
99        #[test]
100        fn scan_doesnt_affect_state() {
101            let (_, new_state) = Spec::apply(&Scan(0, Some([0, 0, 0])), &Spec::init());
102            assert_eq!(Spec::init(), new_state);
103        }
104
105        #[test]
106        fn scan_not_valid_if_differs_from_state() {
107            let mut new_state = Spec::init();
108            new_state[0] = 123;
109            let (valid, _) = Spec::apply(&Scan(0, Some(new_state)), &Spec::init());
110            assert!(!valid);
111        }
112    }
113}
todc_utils/specifications/snapshot.rs

todc_utils/specifications/
snapshot.rs
