pub struct IpcInvariantChecker;Expand description
IPC invariant checker that validates channel properties
Implementations§
Source§impl IpcInvariantChecker
impl IpcInvariantChecker
Sourcepub fn verify_fifo_ordering(
channel: &IpcChannelModel,
) -> Result<(), IpcModelError>
pub fn verify_fifo_ordering( channel: &IpcChannelModel, ) -> Result<(), IpcModelError>
Verify FIFO ordering: messages dequeued in send order
Sourcepub fn verify_no_message_loss(
channel: &IpcChannelModel,
) -> Result<(), IpcModelError>
pub fn verify_no_message_loss( channel: &IpcChannelModel, ) -> Result<(), IpcModelError>
Verify no message loss: sent - received = pending
Sourcepub fn verify_channel_isolation(
channel: &IpcChannelModel,
) -> Result<(), IpcModelError>
pub fn verify_channel_isolation( channel: &IpcChannelModel, ) -> Result<(), IpcModelError>
Verify channel isolation: messages in a channel have the correct channel_id
Sourcepub fn verify_buffer_bounds(
channel: &IpcChannelModel,
) -> Result<(), IpcModelError>
pub fn verify_buffer_bounds( channel: &IpcChannelModel, ) -> Result<(), IpcModelError>
Verify buffer bounds: message count never exceeds capacity
Sourcepub fn verify_capability_enforcement(
channel: &mut IpcChannelModel,
) -> Result<(), IpcModelError>
pub fn verify_capability_enforcement( channel: &mut IpcChannelModel, ) -> Result<(), IpcModelError>
Verify capability enforcement: operations require correct rights
Sourcepub fn verify_deadlock_freedom(graph: &WaitGraph) -> Result<(), IpcModelError>
pub fn verify_deadlock_freedom(graph: &WaitGraph) -> Result<(), IpcModelError>
Verify deadlock freedom: no cycles in wait-for graph