Source blocking_io.rs::block_thread_for_io on typed owned callback data. Immediate readiness executes the FnOnce directly. Only actually blocked calls consume a shared callback token; no function-valued registry is requested.

@[reducible, inline]

abbrev Miri.Interpreter.OwnedBlockingIo.M (σ α : Type) : Type

Equations

• Miri.Interpreter.OwnedBlockingIo.M = EStateM Miri.Interpreter.StepError

structure Miri.Interpreter.OwnedBlockingIo.Hooks (S F C Poll Host : Type) : Type

• source : BlockingIo.Hooks S F Poll Host
• register : C → M S Nat
• take : Nat → M S C
• dropCapture : C → M S Unit

def Miri.Interpreter.OwnedBlockingIo.block {S F C P H : Type} (h : Hooks S F C P H) (fd : F) (interest : BlockingIo.Interest) (deadline : Option Concurrency.ThreadDeadline) (capture : C) (invoke : C → Concurrency.UnblockKind → M S Unit) : M S Unit

Owns the source_fd argument and callback environment. Source removes the IO interest in its callback body, not in this helper. Registration follows the source add-interest and immediate-readiness check.

Equations

• One or more equations did not get rendered due to their size.