Entire pinned concurrency/blocking_io.rs. Host mio Source/Poll and events remain real stateful effects; all event ordering, weak ownership, readiness and callback policy is implemented here.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.BlockingIo.Interest : Type

• read : Interest
• write : Interest
• readWrite : Interest

@[instance_reducible]

instance Miri.Interpreter.BlockingIo.instDecidableEqInterest : DecidableEq Interest

Equations

• Miri.Interpreter.BlockingIo.instDecidableEqInterest x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.BlockingIo.instReprInterest : Repr Interest

Equations

• Miri.Interpreter.BlockingIo.instReprInterest = { reprPrec := Miri.Interpreter.BlockingIo.instReprInterest.repr }

def Miri.Interpreter.BlockingIo.instReprInterest.repr : Interest → Nat → Std.Format

Equations

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

def Miri.Interpreter.BlockingIo.Interest.fulfilled (interest : Interest) (ready : Files.Readiness) : Bool

Equations

• Miri.Interpreter.BlockingIo.Interest.read.fulfilled ready = (ready.readable || ready.error)
• Miri.Interpreter.BlockingIo.Interest.write.fulfilled ready = (ready.writable || ready.error)
• Miri.Interpreter.BlockingIo.Interest.readWrite.fulfilled ready = (ready.readable || ready.writable || ready.error)

structure Miri.Interpreter.BlockingIo.Source : Type

• fd : Files.WeakRef
• blocked : Array (Concurrency.ThreadId × Interest)

structure Miri.Interpreter.BlockingIo.Manager (Poll : Type) : Type

• poll : Option Poll
• sources : Array (Files.FdId × Source)

structure Miri.Interpreter.BlockingIo.Event : Type

• token : Files.FdId
• ready : Files.Readiness

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

• readiness : Readiness.Hooks S F
• get : M S (Manager Poll)
• put : Manager Poll → M S Unit
• newPoll : M S (Except (IoError.HostError Host) Poll)
• dropPoll : Poll → M S Unit
• registerHostSource : Poll → F → Files.FdId → Interest → M S (Except (IoError.HostError Host) Unit)
• pollHost : Poll → Option Clock.Duration → Nat → M S (Except (IoError.HostError Host) (Array Event))
• sourceReadiness : F → M S Files.Readiness
• setSourceReadiness : F → Files.Readiness → M S Unit
• cloneFd : F → M S F

def Miri.Interpreter.BlockingIo.newManager {S F P H : Type} (h : Hooks S F P H) (communicate : Bool) : M S (Except (IoError.HostError H) (Manager P))

Equations

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

def Miri.Interpreter.BlockingIo.register {S F P H : Type} (h : Hooks S F P H) (fd : F) : M S Unit

Equations

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

def Miri.Interpreter.BlockingIo.addBlockedThread {S F P H : Type} (h : Hooks S F P H) (id : Files.FdId) (thread : Concurrency.ThreadId) (interest : Interest) : M S Unit

Equations

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

def Miri.Interpreter.BlockingIo.removeBlockedThread {S F P H : Type} (h : Hooks S F P H) (id : Files.FdId) (thread : Concurrency.ThreadId) : M S Unit

Equations

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

def Miri.Interpreter.BlockingIo.runGc {S F P H : Type} (h : Hooks S F P H) : M S Unit

Equations

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

def Miri.Interpreter.BlockingIo.blockThreadForIo {S F P H : Type} (h : Hooks S F P H) (fd : F) (interest : Interest) (deadline : Option Concurrency.ThreadDeadline) (callback : Concurrency.SyncRuntime.Callback S) : M S Unit

Equations

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

def Miri.Interpreter.BlockingIo.poll {S F P H : Type} (budget : Nat) (h : Hooks S F P H) (timeout : Option Clock.Duration) : M S (Except (IoError.HostError H) Unit)

All event-source readiness bits are OR-ed before any readiness or IO callbacks execute, matching the source collect::<Vec<_>>() first phase.

Equations

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

def Miri.Interpreter.BlockingIo.pollAndUnblock {S F P H : Type} (budget : Nat) (h : Hooks S F P H) (timeout : Option Clock.Duration) : M S Unit

Equations

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

def Miri.Interpreter.BlockingIo.anyThreadBlockedOnHost {S F P H : Type} (h : Hooks S F P H) : M S Bool

Equations

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