tweak docs a little

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,15 +40,16 @@ 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,
     /// The operation did not complete within its specified duration.
     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.

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,)*