Add shuttle-tokio #238

sarsko · 2025-12-02T00:52:02Z

Adds shuttle-tokio implementation and wrappers.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

jorajeev

Only reviewed upto tokio-stream

jorajeev · 2025-12-03T13:48:33Z

wrappers/tokio/README.md

+]
+
+[dependencies]
+tokio = { package = "shuttle-tokio", version = "VERSION_NUMBER" }


We should just have users depend on * right?

jorajeev · 2025-12-03T13:55:19Z

wrappers/tokio/README.md

@@ -0,0 +1,34 @@
+# ShuttleTokio


Let's avoid introducing the term ShuttleTokio which is not really meaningful to anyone. Change this heading to:

# Shuttle support for `tokio`

jorajeev · 2025-12-03T13:58:08Z

wrappers/tokio/README.md

@@ -0,0 +1,34 @@
+# ShuttleTokio
+
+This folder contains the implementation and wrapper for ShuttleTokio, which provides [tokio](https://crates.io/crates/tokio) support to Shuttle.


replace with

This folder contains the implementation and wrapper that enables testing of [tokio](https://crates.io/crates/tokio) applications with Shuttle.

jorajeev · 2025-12-03T13:59:17Z

wrappers/tokio/README.md

+
+## How to use
+
+To use it, do something akin to the following in your Cargo.toml:


Replace do something akin to the following to add the following.

jorajeev · 2025-12-03T14:01:03Z

wrappers/tokio/README.md

+
+## Limitations
+
+The development of ShuttleTokio has come as a consequence of teams at Amazon needing support for model checking code using tokio. What has driven development is the functionality needed by these teams, meaning there are parts of tokio which have not been implemented or which have not been modeled faithfully. This is something to keep in mind if you want to use ShuttleTokio, and there is some likelihood that there will be functionality that will need to be added. We are happy to review PRs if there is functionality you'd like to add to ShuttleTokio.


Replace this with:

Shuttle's tokio support does not currently model all tokio functionality. Some parts of tokio have not been implemented or may not be modeled faithfully. Keep this in mind when using Shuttle with tokio, as you may encounter missing functionality that needs to be added. If you encounter missing features, please file an issue or, better yet, open a PR to contribute the functionality.

jorajeev · 2025-12-03T14:19:15Z

wrappers/tokio/impls/tokio-macros/src/lib.rs

+
+/// Always fails with the error message below.
+/// ```text
+/// The #[shuttle_tokio::main] macro requires rt or rt-multi-thread.


Both here (and in similar uses below), will the error say [shuttle_tokio::main] and not [tokio::main] ?

jorajeev · 2025-12-03T14:21:51Z

wrappers/tokio/impls/tokio-stream/Cargo.toml

+[features]
+default = ["time"]
+
+full = [


This is not the complete list,see https://github.com/tokio-rs/tokio/blob/master/tokio/Cargo.toml#L29

You're linking to the wrong crate, see https://github.com/tokio-rs/tokio/blob/master/tokio-stream/Cargo.toml#L22

jorajeev · 2025-12-03T14:24:23Z

wrappers/tokio/impls/tokio-stream/README.md

@@ -0,0 +1,6 @@
+# ShuttleTokioStream


Change to # Shuttle support for tokio-stream

jorajeev · 2025-12-03T14:28:55Z

wrappers/tokio/impls/tokio-stream/README.md

@@ -0,0 +1,6 @@
+# ShuttleTokioStream
+
+This package was made by doing the following:


Rewrite this as

This package was derived from tokio-stream by: 1. Cloning the original repository 2. Replacing the tokio dependency with Shuttle's tokio implementation in Cargo.toml 3. Removing extraneous files and dependencies (docs, fuzz tests, CHANGELOG.md, etc.)

jorajeev · 2025-12-03T14:31:42Z

wrappers/tokio/impls/tokio-stream/src/lib.rs

+    attr(deny(warnings, rust_2018_idioms), allow(dead_code, unused_variables))
+))]
+
+//! This is the "impl" crate implementing [`tokio-stream`] support for [`Shuttle`].


Please rephrase this as per my comments in PR #232

sarsko · 2026-01-13T00:45:25Z

wrappers/tokio/impls/tokio/tests/rate_limiter.rs

@@ -0,0 +1,173 @@
+// Rate limiter test demonstrating a subtle concurrency bug that Shuttle can catch


Not fully clear to me why this lives here

sarsko · 2026-01-13T00:47:15Z

wrappers/tokio/impls/tokio/tests/blog.rs

@@ -0,0 +1,144 @@
+use shuttle::future::block_on;


This does not belong in tokio-test

sarsko · 2026-01-13T00:49:08Z

wrappers/tokio/impls/tokio/tests/blog.rs

+}
+
+#[tokio_orig::test]
+async fn test_async_connection_limit_traditional() {


Why do we have a tokio test?

Co-authored-by: Rajeev Joshi <jorajeev@amazon.com> Co-authored-by: Bernhard Kragl <kraglb@amazon.com>

sarsko force-pushed the tokio2 branch from 9a90871 to 519d0a1 Compare December 2, 2025 08:53

jorajeev reviewed Dec 3, 2025

View reviewed changes

sarsko commented Jan 13, 2026

View reviewed changes

sarsko and others added 3 commits January 13, 2026 02:16

Add shuttle-tokio

308f0db

Co-authored-by: Rajeev Joshi <jorajeev@amazon.com> Co-authored-by: Bernhard Kragl <kraglb@amazon.com>

Comment cleanup

f816d92

Make blog and rate_limiter tests compile

085d285

sarsko force-pushed the tokio2 branch from 0c016fb to 085d285 Compare January 13, 2026 01:20

		@@ -0,0 +1,34 @@
		# ShuttleTokio

		This folder contains the implementation and wrapper for ShuttleTokio, which provides [tokio](https://crates.io/crates/tokio) support to Shuttle.


		## How to use

		To use it, do something akin to the following in your Cargo.toml:


		## Limitations

		The development of ShuttleTokio has come as a consequence of teams at Amazon needing support for model checking code using tokio. What has driven development is the functionality needed by these teams, meaning there are parts of tokio which have not been implemented or which have not been modeled faithfully. This is something to keep in mind if you want to use ShuttleTokio, and there is some likelihood that there will be functionality that will need to be added. We are happy to review PRs if there is functionality you'd like to add to ShuttleTokio.

		@@ -0,0 +1,6 @@
		# ShuttleTokioStream

		This package was made by doing the following:

		@@ -0,0 +1,173 @@
		// Rate limiter test demonstrating a subtle concurrency bug that Shuttle can catch

Add shuttle-tokio #238

Are you sure you want to change the base?

Add shuttle-tokio #238

Uh oh!

Conversation

sarsko commented Dec 2, 2025

Uh oh!

jorajeev left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants