Complete state/control policy of pinned shims/readiness.rs. Watcher IDs and FD weak refs are ownership identities, not readiness tokens or success claims.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.Readiness.Bits : Type

Equations

• Miri.Interpreter.Readiness.Bits = Miri.Interpreter.Files.Readiness

def Miri.Interpreter.Readiness.Bits.empty : Bits

Equations

• Miri.Interpreter.Readiness.Bits.empty = { }

def Miri.Interpreter.Readiness.Bits.inter (a b : Bits) : Bits

Equations

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

def Miri.Interpreter.Readiness.Bits.union (a b : Bits) : Bits

Equations

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

structure Miri.Interpreter.Readiness.Key : Type

• id : Files.FdId
• number : Int32

@[instance_reducible]

instance Miri.Interpreter.Readiness.instDecidableEqKey : DecidableEq Key

Equations

• Miri.Interpreter.Readiness.instDecidableEqKey = Miri.Interpreter.Readiness.instDecidableEqKey.decEq

def Miri.Interpreter.Readiness.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.Readiness.instDecidableEqKey.decEq { id := a, number := a_1 } { id := b, number := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

structure Miri.Interpreter.Readiness.Interest : Type

• fd : Files.WeakRef
• relevant : Bits
• edgeTriggered : Bool
• data : UInt64
• active : Bits

structure Miri.Interpreter.Readiness.Watcher : Type

• interests : Array (Key × Interest)
• ready : Array Key
• queue : Array Concurrency.ThreadId

structure Miri.Interpreter.Readiness.Watched : Type

• watchers : Array Nat

  Weak watcher identities, in source insertion order.

• clock : Concurrency.VClock

structure Miri.Interpreter.Readiness.Flags : Type

• forceEdge : Bool
• noReleaseClock : Bool

structure Miri.Interpreter.Readiness.Hooks (S F : Type) : Type

• runtime : Concurrency.SyncRuntime.Hooks S Nat Int32 (MPlaceTy Memory.Provenance)
• debugAssertions : Bool
• getWatcher : Nat → M S Watcher
• putWatcher : Nat → Watcher → M S Unit
• upgradeWatcher : Nat → M S Bool
• dropWatcher : Nat → M S Unit
• watcherAlive : Nat → M S Bool
• getFd : Int32 → M S F
• id : F → Files.FdId
• downgrade : F → Files.WeakRef
• upgrade : Files.WeakRef → M S (Option F)
• dropFd : F → M S Unit
• isClosed : Files.WeakRef → M S Bool
• supportsWatching : F → Bool
• getWatched : F → M S Watched
• putWatched : F → Watched → M S Unit
• readiness : F → M S Bits
• delayed : M S (Array F)
• putDelayed : Array F → M S Unit
• unblock : Concurrency.ThreadId → Concurrency.BlockReason → M S Unit

  Must enable/swap the full target thread view, execute its typed callback, and restore only on success. No callback token acknowledgment is accepted.

def Miri.Interpreter.Readiness.consumeOwned {A : Type u_1} {S : Type} (items : List A) (action drop : A → M S Unit) : M S Unit

Vec-style ownership: retain all during collection, then drop each consumed item after its iteration, and drop unconsumed items if an iteration fails.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Readiness.consumeOwned [] action drop = pure ()

def Miri.Interpreter.Readiness.collectOwned {A : Type u_1} {S B : Type} (items : Array A) (acquire : A → M S B) (drop : B → M S Unit) : M S (Array B)

Equations

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

def Miri.Interpreter.Readiness.readyCount {S F : Type} (h : Hooks S F) (watcher : Nat) : M S Nat

Equations

• Miri.Interpreter.Readiness.readyCount h watcher = do let __do_lift ← h.getWatcher watcher pure __do_lift.ready.size

def Miri.Interpreter.Readiness.addBlockedThread {S F : Type} (h : Hooks S F) (watcher : Nat) (thread : Concurrency.ThreadId) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.removeBlockedThread {S F : Type} (h : Hooks S F) (watcher : Nat) (thread : Concurrency.ThreadId) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.wakeReady {S F : Type} (budget : Nat) (h : Hooks S F) (watcher : Nat) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.updateReadiness {S F : Type} (budget : Nat) (h : Hooks S F) (watcher : Nat) (active : Bits) (forceEdge : Bool) (keys : Array Key) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.addInterest {S F : Type} (budget : Nat) (h : Hooks S F) (watcher : Nat) (number : Int32) (relevant : Bits) (edge : Bool) (data : UInt64) : M S Bool

Equations

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

def Miri.Interpreter.Readiness.updateInterest {S F : Type} (budget : Nat) (h : Hooks S F) (watcher : Nat) (key : Key) (change : Interest → Interest) : M S Bool

Equations

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

def Miri.Interpreter.Readiness.removeInterest {S F : Type} (h : Hooks S F) (watcher : Nat) (key : Key) : M S Bool

Equations

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

def Miri.Interpreter.Readiness.updateFd {S F : Type} (budget : Nat) (h : Hooks S F) (fd : F) (flags : Flags) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.addDelayed {S F : Type} (h : Hooks S F) (fd : F) : M S Unit

Equations

• Miri.Interpreter.Readiness.addDelayed h fd = do let __do_lift ← h.delayed h.putDelayed (__do_lift.push fd)

def Miri.Interpreter.Readiness.processDelayed {S F : Type} (budget : Nat) (h : Hooks S F) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.getReadyInterests {S F : Type} (budget max : Nat) (h : Hooks S F) (watcher : Nat) : M S (Array Interest)

Equations

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

def Miri.Interpreter.Readiness.hasWatcherWithBlockedThread {S F : Type} (h : Hooks S F) (fd : F) : M S Bool

Equations

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

def Miri.Interpreter.Readiness.removeFileNumInterests {S F : Type} (h : Hooks S F) (fd : F) (number : Int32) : M S Unit

Equations

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

def Miri.Interpreter.Readiness.dropWatcherMetadata {S F : Type} (h : Hooks S F) (state : Watcher) : M S Unit

Called after the watcher loses its last strong reference. Payload remains available to this destructor, while watcherAlive must already report false.

Equations

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

def Miri.Interpreter.Readiness.dropWatchedMetadata {S F : Type} (h : Hooks S F) (watched : Watched) : M S Unit

Last FD description drop removes all dead FD interests from live watchers, not merely the descriptor number that happened to close last.

Equations

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