Concurrency: Generalize UnblockCallback to MachineCallback #4106

shamb0 · 2024-12-24T06:48:00Z

Key Changes:

- Introduces `MachineCallbackState` to represent operation outcomes (Ready/TimedOut)
- Replaces `UnblockCallback` with a more general `MachineCallback` trait
- Consolidates callback methods into a single interface for better extensibility
- Updates thread blocking mechanisms and synchronization primitives to use the new callback system

This is the first PR in a series to add support for asynchronous file operations:

Reference: Requirements Discussion at Add support for vectorized read with libc::readv #4084 (comment)
1. Generalize callback system (this PR)
2. Add callback support to FileDescription::read
3. Implement readv using the new callback system

shamb0 · 2024-12-24T07:33:10Z

@rustbot ready

RalfJung · 2024-12-26T22:12:34Z

src/concurrency/thread.rs


+pub type DyMachineCallback<'tcx> = Box<dyn MachineCallback<'tcx> + 'tcx>;


Please call this DynMachineCallback<'tcx, T>.

And then define DynUnblockCallback<'tcx> as alias for DynMachineCallback<'tcx, UnblockKind>.

RalfJung · 2024-12-26T22:13:06Z

src/concurrency/thread.rs

+}
+
+/// Generic callback trait for machine operations.
+pub trait MachineCallback<'tcx>: VisitProvenance {


Please move this to machine.rs.

src/concurrency/thread.rs

RalfJung · 2024-12-26T22:15:36Z

src/concurrency/thread.rs


+pub type DyMachineCallback<'tcx> = Box<dyn MachineCallback<'tcx> + 'tcx>;
+
+/// Macro for creating machine callbacks
 #[macro_export]
 macro_rules! callback {


This should also be in machine.rs

src/concurrency/thread.rs

RalfJung · 2024-12-26T22:18:27Z

src/concurrency/thread.rs

+                                interp_ok(())
+                            }
+                            MachineCallbackState::TimedOut => {
+                                panic!("Join thread operation received unexpected timeout state - operations do not support timeouts")


No need to write such a detailed error each time. Also, please avoid the rightwards drift. So instead of a match unblock, just have something like

assert_eq!(unblock, UnblockKind::Ready);

at the beginning of the function, and then go on with the function body as before.

RalfJung · 2024-12-26T22:19:38Z

Thanks for the PR! I left some comments.

@rustbot author

shamb0 · 2024-12-27T10:58:15Z

Thank you for your thoughtful review and detailed comments. I've addressed all the feedback to improve the code's quality, ensuring the changes align with your recommendations on callback generics.

The PR is now ready for your review, but I’m happy to make further refinements if needed to meet our quality standards.

Please feel free to reach out if any part of the changes needs clarification or further attention. :)

@rustbot ready

RalfJung

Thanks! This is pretty close.

However, I am not entirely convinced by some of the comments you have been adding. Were they generated by an LLM? See the detailed review for more.

Generating comments with an LLM is fine but they should be reviewed for plausibility and usefulness before putting them in the codebase. I helps me do that review if you let me know which parts are LLM-generated.

RalfJung · 2024-12-27T11:41:11Z

src/concurrency/thread.rs

-            }
-        }
+/// Type alias for boxed machine callbacks with generic argument type.
+pub type DyMachineCallback<'tcx, T> = Box<dyn MachineCallback<'tcx, T> + 'tcx>;


This type alias should also be in machine.rs, next to the definition of MachineCallback. Also, please consistently use the Dyn prefix, not Dy.

src/machine.rs

RalfJung · 2024-12-27T11:44:55Z

src/machine.rs

+/// Creates machine callbacks with captured variables and generic argument types.
+///
+/// This macro generates the boilerplate needed to create type-safe callbacks:
+/// - Creates a struct to hold captured variables
+/// - Implements required traits (VisitProvenance, MachineCallback)
+/// - Handles proper lifetime and type parameters
+///
+/// The callback body receives the interpreter context and completion argument.


Again this is a lot of text but not very helpful text. Instead, can you put a small example of how to use the macro? That would be a lot more useful.

RalfJung · 2024-12-27T11:45:34Z

src/machine.rs

+macro_rules! callback {
+    (@capture<$tcx:lifetime $(,)? $($lft:lifetime),*>
+     { $($name:ident: $type:ty),* $(,)? }
+     @unblock = |$this:ident, $arg:ident: $arg_ty:ty| $body:expr $(,)?) => {{


Please remove the @unblock = everywhere. Now that there's only one function body here, it should not be needed any more.

RalfJung · 2024-12-27T11:46:54Z

src/machine.rs

+    (@capture<$tcx:lifetime $(,)? $($lft:lifetime),*>
+     { $($name:ident: $type:ty),* $(,)? }
+     @unblock = |$this:ident, $arg:ident: $arg_ty:ty| $body:expr $(,)?) => {{
+        // Create callback struct with the captured variables and generic type T


Please remove these comments, they don't add any information that's not already immediately obvious from looking at the code.

Comments are supposed to describe the code in a high-level way, helping the reader understand the goal of the low-level details visible in the code. These comments feel LLM-generated, and LLMs are pretty bad at generating good comments -- writing good comments requires actually understanding the code, which LLMs are not capable of.

src/machine.rs

RalfJung · 2024-12-27T11:48:20Z

src/shims/time.rs

-                @unblock = |_this| { panic!("sleeping thread unblocked before time is up") }
-                @timeout = |_this| { interp_ok(()) }
+                @unblock = |_this, unblock: UnblockKind| {
+                    match unblock {


This could be an assert_eq!(unblock, UnblockKind::TimedOut); (same below)

RalfJung · 2024-12-29T08:37:05Z

There are merge conflicts due to other PRs that landed recently in this repo. Please resolve the merge conflicts.

@rustbot author

* Introduce UnblockKind enum to represent operation outcomes * Consolidate unblock/timeout methods into single callback interface * Update thread blocking system to use new callback mechanism * Refactor mutex and condvar implementations for new callback pattern Signed-off-by: shamb0 <[email protected]>

shamb0 · 2024-12-29T08:57:33Z

Thank you, @RalfJung, for your detailed feedback on the documentation. I appreciate your emphasis on keeping explanations concise, high-level, and focused on code intent rather than implementation details.

I've updated the documentation based on your suggestions and will continue applying these principles to future Miri contributions. While I used an LLM to assist with refining the docstrings, I ensured the revisions align with your guidance to avoid verbosity and redundancy.

Your earlier review comments have been addressed, but please let me know if there’s anything else that needs adjustment. I’m also working on gaining a deeper understanding of Miri’s documentation practices to ensure consistency across the codebase.

@rustbot ready

shamb0 marked this pull request as ready for review December 24, 2024 07:32

rustbot added the S-waiting-on-review Status: Waiting for a review to complete label Dec 24, 2024

shamb0 mentioned this pull request Dec 26, 2024

Add callback support to FileDescription::read #4110

Open

RalfJung reviewed Dec 26, 2024

View reviewed changes

rustbot added S-waiting-on-author Status: Waiting for the PR author to address review comments and removed S-waiting-on-review Status: Waiting for a review to complete labels Dec 26, 2024

shamb0 force-pushed the generalize-callback-miri-concurrency branch from 5c8652c to 7049aa6 Compare December 27, 2024 10:28

rustbot added S-waiting-on-review Status: Waiting for a review to complete and removed S-waiting-on-author Status: Waiting for the PR author to address review comments labels Dec 27, 2024

RalfJung reviewed Dec 27, 2024

View reviewed changes

rustbot added S-waiting-on-author Status: Waiting for the PR author to address review comments and removed S-waiting-on-review Status: Waiting for a review to complete labels Dec 29, 2024

shamb0 force-pushed the generalize-callback-miri-concurrency branch from 124770d to 42ef1d7 Compare December 29, 2024 08:40

rustbot added S-waiting-on-review Status: Waiting for a review to complete and removed S-waiting-on-author Status: Waiting for the PR author to address review comments labels Dec 29, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Concurrency: Generalize UnblockCallback to MachineCallback #4106

Concurrency: Generalize UnblockCallback to MachineCallback #4106

shamb0 commented Dec 24, 2024

shamb0 commented Dec 24, 2024

RalfJung Dec 26, 2024

RalfJung Dec 26, 2024

RalfJung Dec 26, 2024

RalfJung Dec 26, 2024

RalfJung commented Dec 26, 2024

shamb0 commented Dec 27, 2024 •

edited

Loading

RalfJung left a comment

RalfJung Dec 27, 2024

RalfJung Dec 27, 2024 •

edited by workingjubilee

Loading

RalfJung Dec 27, 2024

RalfJung Dec 27, 2024

RalfJung Dec 27, 2024

RalfJung commented Dec 29, 2024

shamb0 commented Dec 29, 2024 •

edited

Loading


		pub type DyMachineCallback<'tcx> = Box<dyn MachineCallback<'tcx> + 'tcx>;

Concurrency: Generalize UnblockCallback to MachineCallback #4106

Are you sure you want to change the base?

Concurrency: Generalize UnblockCallback to MachineCallback #4106

Conversation

shamb0 commented Dec 24, 2024

Key Changes:

This is the first PR in a series to add support for asynchronous file operations:

shamb0 commented Dec 24, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung commented Dec 26, 2024

shamb0 commented Dec 27, 2024 • edited Loading

RalfJung left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung Dec 27, 2024 • edited by workingjubilee Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung commented Dec 29, 2024

shamb0 commented Dec 29, 2024 • edited Loading

shamb0 commented Dec 27, 2024 •

edited

Loading

RalfJung Dec 27, 2024 •

edited by workingjubilee

Loading

shamb0 commented Dec 29, 2024 •

edited

Loading