Source IO callback ownership on the actual machine. The one supply is ThreadMachine.nextCallback via views; IO storage contains only positive data.

@[reducible, inline]

abbrev Miri.Interpreter.OwnedIoMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.OwnedIoMachine.State = Miri.Interpreter.TypedSyncMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.OwnedIoMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.OwnedIoMachine.M = Miri.Interpreter.TypedSyncMachine.M

structure Miri.Interpreter.OwnedIoMachine.Views (U F : Type) : Type

• storage : U → OwnedIoRuntime.Storage F
• putStorage : U → OwnedIoRuntime.Storage F → U
• nextCallback : U → Nat
• putNextCallback : U → Nat → U

def Miri.Interpreter.OwnedIoMachine.owns {U F K : Type} (v : Views U F) (token : Nat) : M K U Bool

Equations

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

def Miri.Interpreter.OwnedIoMachine.register {U F K : Type} (v : Views U F) (capture : OwnedIoRuntime.Capture F) : M K U Nat

Equations

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

def Miri.Interpreter.OwnedIoMachine.take {U F K : Type} (v : Views U F) (token : Nat) : M K U (OwnedIoRuntime.Capture F)

Equations

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

structure Miri.Interpreter.OwnedIoMachine.Operations (S F E : Type) : Type

• event : EventFd.PhysicalHooks S F
• completion : IoCompletion.Hooks S E
• errorFromKind : IoError.ErrorKind → EStateM StepError S (IoError.Error E)
• dropWatcher : Nat → EStateM StepError S Unit
• pollReady : Nat → Array (Int32 × IoCompletion.Dest) → EStateM StepError S UInt32
• writeU32 : UInt32 → IoCompletion.Dest → EStateM StepError S Unit
• epollReady : F → IoCompletion.Dest → IoCompletion.Dest → EStateM StepError S Nat
• epollRemoveBlocked : F → Concurrency.ThreadId → EStateM StepError S Unit

def Miri.Interpreter.OwnedIoMachine.hooks {U F K E : Type} (v : Views U F) (h : Operations (State K U) F E) : OwnedIoRuntime.Hooks (State K U) F E

Equations

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

def Miri.Interpreter.OwnedIoMachine.bindEvent {U F K E : Type} (v : Views U F) (h : Operations (State K U) F E) : EventFd.Hooks (State K U) F

Real eventfd FileDescription execution now selects the data interpreter; no source callback registration consults a legacy Registry S.

Equations

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

def Miri.Interpreter.OwnedIoMachine.bindPoll {U F K E Iter : Type} (v : Views U F) (h : Operations (State K U) F E) (poll : PollShims.Hooks (State K U) F Iter) : PollShims.Hooks (State K U) F Iter

Equations

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

def Miri.Interpreter.OwnedIoMachine.bindEpoll {U F K E Iter : Type} (v : Views U F) (h : Operations (State K U) F E) (epoll : EpollShims.Hooks (State K U) F Iter) : EpollShims.Hooks (State K U) F Iter

Equations

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