Canonical machine ownership/clock binding for poll and epoll. Other payload injection/downcast is explicit so an unavailable descriptor cannot masquerade as an epoll instance. The source Epoll does not contain ReadinessWatched.

structure Miri.Interpreter.PollMachine.Epoll : Type

• watcher : Nat

def Miri.Interpreter.PollMachine.instDecidableEqEpoll.decEq (x✝ x✝¹ : Epoll) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.PollMachine.instDecidableEqEpoll.decEq { watcher := a } { watcher := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.PollMachine.instDecidableEqEpoll : DecidableEq Epoll

Equations

• Miri.Interpreter.PollMachine.instDecidableEqEpoll = Miri.Interpreter.PollMachine.instDecidableEqEpoll.decEq

def Miri.Interpreter.PollMachine.instReprEpoll.repr : Epoll → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PollMachine.instReprEpoll : Repr Epoll

Equations

• Miri.Interpreter.PollMachine.instReprEpoll = { reprPrec := Miri.Interpreter.PollMachine.instReprEpoll.repr }

def Miri.Interpreter.PollMachine.name : Epoll → String

Equations

• Miri.Interpreter.PollMachine.name x✝ = "epoll"

def Miri.Interpreter.PollMachine.metadata : Epoll → String

Equations

• Miri.Interpreter.PollMachine.metadata x✝ = "S_IFREG"

structure Miri.Interpreter.PollMachine.DescriptorHooks (O : Type) : Type

• inject : Epoll → O
• project : O → Option Epoll

def Miri.Interpreter.PollMachine.insertEpoll {K U H D O : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : DescriptorHooks O) (watcher : Nat) : MachineHooks.M K U Int32

Owning transfer into the real descriptor table; no extra watcher retain.

Equations

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

def Miri.Interpreter.PollMachine.dropEpoll {K U H D O : Type} (h : ReadinessMachine.Hooks K U H D O) (base : Readiness.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O))) (epoll : Epoll) : MachineHooks.M K U Unit

Call at actual Epoll watcher-field drop, after strong FD count reaches zero.

Equations

• Miri.Interpreter.PollMachine.dropEpoll h base epoll = (Miri.Interpreter.ReadinessMachine.bind h base).dropWatcher epoll.watcher

def Miri.Interpreter.PollMachine.bind {K U H D O Host System I : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : DescriptorHooks O) (deadline : DeadlineMachine.Hooks K U Host System) (base : EpollShims.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O)) I) : EpollShims.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O)) I

Equations

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

def Miri.Interpreter.PollMachine.bindEntryPoll {S F P H I : Type} (budget : Nat) (io : BlockingIo.Hooks S F P H) (base : PollDispatch.Hooks S F I) : PollDispatch.Hooks S F I

Uses actual mio poll(0) and source Interrupted policy via BlockingIo.

Equations

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