Skip to content

Commit 49a07ce

Browse files
net: framed: property testing FrameWrite is cancel safe (#939)
Summary: Pull Request resolved: #939 i see now that D80626978 has most of what the following comment states. clearly i messed up the rebase. this is just a small continuation of that. introduce proptest-based property tests for `FrameWrite` cancellation safety. add proptest dev/test deps; factor test harness (`Throttled`, `SharedWriter`, `Gate`, `BudgetedWriter`, `budget_drips`) into `test_support`; add generator sanity check (`test_budget_sequence`). new property `test framewrite_cancellation_is_safe` uses `assert_cancel_safe_async` to cancel/restart send at arbitrary poll boundaries under fuzzed budget drip sequences, with shared gate+writer ensuring state persists. wrap in timeout to catch regressions; verify emitted frame matches body. behavior is unchanged; we now exercise cancel-safety as a theorem. currently the property test covers only flat byte buffers (written for pre D80704703); the next diff in the stack will extend it to multipart buffers, exercising the same cancel-safety guarantees when a frame body is split across multiple `Part`s. Reviewed By: mariusae Differential Revision: D80651806 fbshipit-source-id: fade3043596c7bb942e3538c444aa5a1c963c7c3
1 parent a79ee2b commit 49a07ce

File tree

1 file changed

+20
-14
lines changed

1 file changed

+20
-14
lines changed

hyperactor/src/channel/net/framed.rs

Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -798,20 +798,26 @@ mod property_tests {
798798
}
799799

800800
// Theorem: `FrameWrite::send` is cancel-safe.
801-
// That is, it yields the correct frame even if cancelled and
802-
// restarted at any poll boundary, as long as progress eventually
803-
// continues.
804801
//
805-
// Setup:
806-
// - `Gate` meters write budget, shared across attempts.
807-
// - `SharedWriter` wraps the `WriteHalf`, so attempts share a
808-
// handle.
809-
// - `on_pending` drips budget from a fuzzed sequence with a
810-
// fallback to ensure completion.
802+
// Matches the cancel-safety contract from `test_utils::cancel_safe`:
803+
// - State remains valid across cancellations.
804+
// - Restartability: a fresh `send` can resume from shared state.
805+
// - No partial side effects: either no frame is observed, or the
806+
// complete frame is observed.
807+
//
808+
// Semi-formal:
809+
// ∀ drip sequences D, ∀ finite cancellation schedules C:
810+
// if Σ D ≥ 8 + |body|, then
811+
// restarting `send(body)` under C eventually yields Ok(())
812+
// and the reader observes exactly one frame = `body`.
813+
//
814+
// Intuition: Even if the future is cancelled at any
815+
// `Poll::Pending`, shared state (`Gate` + `SharedWriter`) ensures
816+
// eventual completion with the correct frame, provided enough
817+
// budget is dripped.
811818
proptest! {
812819
#![proptest_config(ProptestConfig { cases: 64, ..ProptestConfig::default() })]
813820
#[test]
814-
#[ignore] // temporary: re-enable once merge/build is sorted
815821
fn framewrite_cancellation_is_safe(drips in budget_drips()) {
816822
// proptest! generates a plain `#[test]`, not
817823
// `#[tokio::test]`, so no runtime is provided
@@ -866,14 +872,14 @@ mod property_tests {
866872
// `assert_cancel_safe_async` can cancel at
867873
// any Pending boundary, drop it, and then
868874
// retry from the same shared world state.
869-
// - Map `Result<(), io::Error>` → `Result<(),
870-
// io::ErrorKind>` so the `expected` value
871-
// (`Ok(())`) is comparable (requires
875+
// - Map `Result<(), io::Error>` →
876+
// `Result<(),()>` so the `expected` value
877+
// (`Ok(())`) is equality comparable (requires
872878
// `PartialEq`).
873879
{
874880
let bw = BudgetedWriter::new(shared.clone(), gate.clone());
875881
let mut fw = FrameWrite::new(bw, body.clone());
876-
async move { fw.send().await.map(|_| ()).map_err(|e| e.kind()) }
882+
async move { fw.send().await.map_err(|_| ()) }
877883
},
878884
Ok(()),
879885
// `step`: invoked on each `Poll::Pending` to

0 commit comments

Comments
 (0)