diff --git a/src/concurrency/thread.rs b/src/concurrency/thread.rs index 0db3e1455c..6d22dd8d68 100644 --- a/src/concurrency/thread.rs +++ b/src/concurrency/thread.rs @@ -19,7 +19,7 @@ use crate::concurrency::data_race; use crate::shims::tls; use crate::*; -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq)] enum SchedulingAction { /// Execute step on the active thread. ExecuteStep, @@ -30,6 +30,7 @@ enum SchedulingAction { } /// What to do with TLS allocations from terminated threads +#[derive(Clone, Copy, Debug, PartialEq)] pub enum TlsAllocAction { /// Deallocate backing memory of thread-local statics as usual Deallocate, @@ -39,7 +40,7 @@ pub enum TlsAllocAction { } /// The argument type for the "unblock" callback, indicating why the thread got unblocked. -#[derive(Debug, PartialEq)] +#[derive(Clone, Copy, Debug, PartialEq)] pub enum UnblockKind { /// Operation completed successfully, thread continues normal execution. Ready, @@ -47,7 +48,8 @@ pub enum UnblockKind { TimedOut, } -/// Type alias for unblock callbacks using UnblockKind argument. +/// Type alias for unblock callbacks, i.e. machine callbacks invoked when +/// a thread gets unblocked. pub type DynUnblockCallback<'tcx> = DynMachineCallback<'tcx, UnblockKind>; /// A thread identifier. diff --git a/src/machine.rs b/src/machine.rs index ff0a337d14..845ba48432 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -1737,44 +1737,26 @@ pub trait MachineCallback<'tcx, T>: VisitProvenance { /// Type alias for boxed machine callbacks with generic argument type. pub type DynMachineCallback<'tcx, T> = Box<dyn MachineCallback<'tcx, T> + 'tcx>; -/// Creates a callback for blocking operations with captured state. +/// Creates a `DynMachineCallback`: /// -/// When a thread blocks on a resource (as defined in `enum BlockReason`), this callback -/// executes once that resource becomes available. The callback captures needed -/// variables and handles the completion of the blocking operation. -/// -/// # Example /// ```rust -/// // Block thread until mutex is available -/// this.block_thread( -/// BlockReason::Mutex, -/// None, -/// callback!( -/// @capture<'tcx> { -/// mutex_ref: MutexRef, -/// retval: Scalar, -/// dest: MPlaceTy<'tcx>, -/// } -/// |this, unblock: UnblockKind| { -/// // Verify successful mutex acquisition -/// assert_eq!(unblock, UnblockKind::Ready); -/// -/// // Enter critical section -/// this.mutex_lock(&mutex_ref); -/// -/// // Process protected data and store result -/// this.write_scalar(retval, &dest)?; -/// -/// // Exit critical section implicitly when callback completes -/// interp_ok(()) -/// } -/// ), -/// ); +/// callback!( +/// @capture<'tcx> { +/// var1: Ty1, +/// var2: Ty2<'tcx>, +/// } +/// |this, arg: ArgTy| { +/// // Implement the callback here. +/// todo!() +/// } +/// ) /// ``` +/// +/// All the argument types must implement `VisitProvenance`. #[macro_export] macro_rules! callback { (@capture<$tcx:lifetime $(,)? $($lft:lifetime),*> - { $($name:ident: $type:ty),* $(,)? } + { $($name:ident: $type:ty),* $(,)? } |$this:ident, $arg:ident: $arg_ty:ty| $body:expr $(,)?) => {{ struct Callback<$tcx, $($lft),*> { $($name: $type,)*