Pinned unix/linux_like/eventfd.rs. The source read/write retry callback re-reads the user buffer on every write retry, even though num is captured. Concrete retry-budget exhaustion is an unresolved execution resource outcome.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.EventFd.Finish (S : Type) : Type

Equations

• Miri.Interpreter.EventFd.Finish S = Miri.Interpreter.IoCompletionData.Finish S Miri.Interpreter.IoError.ErrorKind

structure Miri.Interpreter.EventFd.Event : Type

• counter : UInt64
• nonblock : Bool
• clock : Concurrency.VClock
• blockedReads : Array Concurrency.ThreadId
• blockedWrites : Array Concurrency.ThreadId

def Miri.Interpreter.EventFd.maximumCounter : Nat

Equations

• Miri.Interpreter.EventFd.maximumCounter = 2 ^ 64 - 2

def Miri.Interpreter.EventFd.readiness (event : Event) : Files.Readiness

Equations

• Miri.Interpreter.EventFd.readiness event = { readable := event.counter != 0, writable := event.counter.toNat != Miri.Interpreter.EventFd.maximumCounter }

inductive Miri.Interpreter.EventFd.DeferredBackend (S F : Type) : Type

• legacy {S F : Type} : DeferredBackend S F
• typed {S F : Type} (read write : F → MPlaceTy Memory.Provenance → IoCompletionData.Capture → M S Unit) : DeferredBackend S F

structure Miri.Interpreter.EventFd.PhysicalHooks (S F : Type) : Type

• runtime : Concurrency.SyncRuntime.Hooks S Nat Int32 (MPlaceTy Memory.Provenance)
• getEvent : F → M S Event
• putEvent : F → Event → M S Unit
• cloneFd : F → M S F
• dropFd : F → M S Unit
• insertNew : Event → M S Int32
• libcI32 : String → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• readI32 : OpTy Memory.Provenance → M S Int32
• u64Layout : M S LocalLayout
• unaligned : Memory.Pointer (Option Memory.Provenance) → LocalLayout → M S (MPlaceTy Memory.Provenance)

  Source ptr_to_mplace_unaligned: formation alone performs no memory access.

• readU64 : MPlaceTy Memory.Provenance → M S UInt64
• writeU64 : UInt64 → MPlaceTy Memory.Provenance → M S Unit
• updateReadiness : F → M S Unit

  Actual update_fd_readiness(fd, FORCE_EDGE), including source clock effects.

• unblockThread : Concurrency.ThreadId → M S Unit

  Actual active-thread/stack switch, FnOnce callback and restore.

structure Miri.Interpreter.EventFd.Hooks (S F : Type) extends Miri.Interpreter.EventFd.PhysicalHooks S F : Type

• runtime : Concurrency.SyncRuntime.Hooks S Nat Int32 (MPlaceTy Memory.Provenance)
• getEvent : F → M S Event
• putEvent : F → Event → M S Unit
• cloneFd : F → M S F
• dropFd : F → M S Unit
• insertNew : Event → M S Int32
• libcI32 : String → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• readI32 : OpTy Memory.Provenance → M S Int32
• u64Layout : M S LocalLayout
• unaligned : Memory.Pointer (Option Memory.Provenance) → LocalLayout → M S (MPlaceTy Memory.Provenance)
• readU64 : MPlaceTy Memory.Provenance → M S UInt64
• writeU64 : UInt64 → MPlaceTy Memory.Provenance → M S Unit
• updateReadiness : F → M S Unit
• unblockThread : Concurrency.ThreadId → M S Unit
• deferred : DeferredBackend S F

def Miri.Interpreter.EventFd.read {S F : Type} (h : Hooks S F) (retryBudget : Nat) (fd : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (finish : Finish S) : M S Unit

Takes one source strong self reference. Production transfers it into the typed retry interpreter; the fixture branch retains its explicit runner bound.

Equations

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

def Miri.Interpreter.EventFd.write {S F : Type} (h : Hooks S F) (retryBudget : Nat) (fd : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (finish : Finish S) : M S Unit

Equations

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

def Miri.Interpreter.EventFd.create {S F : Type} (h : Hooks S F) (value flags : OpTy Memory.Provenance) : M S Int32

Equations

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