nucleus/resources/
state.rs

1use crate::error::StateTransition;
2
3/// Cgroup lifecycle state machine matching Nucleus_Resources_CgroupLifecycle.tla
4///
5/// State transitions:
6/// nonexistent -> created -> configured -> attached -> monitoring -> removed
7///
8/// Properties verified by TLA+ model:
9/// - resource_limits_enforced: Once configured, can only move to attached, monitoring, or removed
10/// - cleanup_guaranteed: Eventually reaches removed state
11/// - no_resource_leak: Removed state is terminal and stable
12#[derive(Debug, Clone, Copy, PartialEq, Eq)]
13pub enum CgroupState {
14    /// Initial state - cgroup doesn't exist
15    Nonexistent,
16    /// Cgroup created in filesystem
17    Created,
18    /// Resource limits configured
19    Configured,
20    /// Process attached to cgroup
21    Attached,
22    /// Monitoring resource usage
23    Monitoring,
24    /// Cgroup removed - terminal state
25    Removed,
26}
27
28impl StateTransition for CgroupState {
29    fn can_transition_to(&self, next: &CgroupState) -> bool {
30        use CgroupState::*;
31
32        matches!(
33            (self, next),
34            (Nonexistent, Created)
35                | (Created, Configured)
36                | (Configured, Attached)
37                | (Attached, Monitoring)
38                | (Monitoring, Removed)
39                // Cleanup paths
40                | (Created, Removed)
41                | (Configured, Removed)
42                | (Attached, Removed)
43                // Stuttering
44                | (Nonexistent, Nonexistent)
45                | (Created, Created)
46                | (Configured, Configured)
47                | (Attached, Attached)
48                | (Monitoring, Monitoring)
49                | (Removed, Removed)
50        )
51    }
52
53    fn is_terminal(&self) -> bool {
54        matches!(self, CgroupState::Removed)
55    }
56}
57
58#[cfg(test)]
59mod tests {
60    use super::*;
61
62    #[test]
63    fn test_valid_transitions() {
64        assert!(CgroupState::Nonexistent.can_transition_to(&CgroupState::Created));
65        assert!(CgroupState::Created.can_transition_to(&CgroupState::Configured));
66        assert!(CgroupState::Configured.can_transition_to(&CgroupState::Attached));
67        assert!(CgroupState::Attached.can_transition_to(&CgroupState::Monitoring));
68        assert!(CgroupState::Monitoring.can_transition_to(&CgroupState::Removed));
69    }
70
71    #[test]
72    fn test_error_paths() {
73        // Can cleanup from Created or Configured on error
74        assert!(CgroupState::Created.can_transition_to(&CgroupState::Removed));
75        assert!(CgroupState::Configured.can_transition_to(&CgroupState::Removed));
76    }
77
78    #[test]
79    fn test_invalid_transitions() {
80        // Cannot skip states
81        assert!(!CgroupState::Nonexistent.can_transition_to(&CgroupState::Configured));
82        assert!(!CgroupState::Created.can_transition_to(&CgroupState::Attached));
83
84        // Cannot go backwards
85        assert!(!CgroupState::Configured.can_transition_to(&CgroupState::Created));
86        assert!(!CgroupState::Removed.can_transition_to(&CgroupState::Monitoring));
87    }
88
89    #[test]
90    fn test_terminal_state() {
91        assert!(!CgroupState::Nonexistent.is_terminal());
92        assert!(!CgroupState::Created.is_terminal());
93        assert!(!CgroupState::Configured.is_terminal());
94        assert!(!CgroupState::Attached.is_terminal());
95        assert!(!CgroupState::Monitoring.is_terminal());
96        assert!(CgroupState::Removed.is_terminal());
97    }
98}
nucleus/resources/state.rs

nucleus/resources/
state.rs
