Linux futex physical/synchronization binding. Futex callbacks are the exact source FnOnce captures, not arbitrary opaque token completion. None mode never requires a fabricated GlobalState. Actual stack switching uses ThreadStacks.

@[reducible, inline]

abbrev Miri.Interpreter.LinuxFutexMachine.User (U : Type) : Type

Equations

• Miri.Interpreter.LinuxFutexMachine.User = Miri.Interpreter.ExecutionStateTransport.Inner

@[reducible, inline]

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

Equations

• Miri.Interpreter.LinuxFutexMachine.State K U = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.LinuxFutexMachine.User U)

@[reducible, inline]

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

Equations

• Miri.Interpreter.LinuxFutexMachine.M K U A = Miri.Interpreter.MachineHooks.M K (Miri.Interpreter.LinuxFutexMachine.User U) A

@[reducible, inline]

abbrev Miri.Interpreter.LinuxFutexMachine.Captures : Type

Equations

• Miri.Interpreter.LinuxFutexMachine.Captures = Miri.Concurrency.FutexRuntime.Storage (Miri.Interpreter.MPlaceTy Miri.Memory.Provenance)

structure Miri.Interpreter.LinuxFutexMachine.Views (U : Type) : Type

• storage : U → Captures
• putStorage : U → Captures → U
• nextCallback : U → Nat

  The same supply used for TLS/join/source thread callbacks.

• putNextCallback : U → Nat → U

structure Miri.Interpreter.LinuxFutexMachine.Payload (P : Type) : Type

• inject : Concurrency.FutexRuntime.Ref → P
• project : P → Option Concurrency.FutexRuntime.Ref
• projectInject (ref : Concurrency.FutexRuntime.Ref) : self.project (self.inject ref) = some ref

structure Miri.Interpreter.LinuxFutexMachine.Hooks (K U C P O B Host System TZ Timestamp ErrorHost : Type) : Type

• views : Views U
• payload : Payload P
• access : PlaceMachine.AccessConfig K (User U)
• allocation : PlaceMachine.AllocationConfig K (User U)
• compiler : PlaceMachine.CompilerHooks K (User U) C
• pointers : PointerMachine.Hooks K (ValidityMachine.Control (ThreadStacks.Storage U))
• pointerCompiler : PointerPlaceMachine.Compiler K (ThreadStacks.Storage U) C
• dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C
• vtable : VTableHooks Memory.Provenance (State K U) C (FnVal O) (ABI.FnAbi MIR.TyId)
• dynamicFuel : Nat
• atomic : AtomicAccessHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)
• backend : State K U → Except StepError (RaceMode.Handler B)
• extras : MemoryExtras.Hooks K (User U) P
• i32Layout : LocalLayout
• readTimespec : MPlaceTy Memory.Provenance → M K U (Option Clock.Duration)

  Compiler-checked guest timespec reader. This is the only time-shim operation consumed by futex; clock/deadline state is carried separately.

• deadline : DeadlineMachine.Hooks K (User U) Host System
• errors : IoError.Hooks (State K U) ErrorHost
• communicate : M K U Bool

structure Miri.Interpreter.LinuxFutexMachine.ObjectHooks (K U C P O B : Type) : Type

The real memory/backend projection needed to construct and use allocation-local typed synchronization objects. It intentionally excludes time, deadline, errno, and isolation capabilities: pthread mutexes/attributes do not need those host effects, while timed operations remain supplied by the separately constructed dispatch hooks.

• views : Views U
• payload : Payload P
• access : PlaceMachine.AccessConfig K (User U)
• allocation : PlaceMachine.AllocationConfig K (User U)
• compiler : PlaceMachine.CompilerHooks K (User U) C
• pointers : PointerMachine.Hooks K (ValidityMachine.Control (ThreadStacks.Storage U))
• pointerCompiler : PointerPlaceMachine.Compiler K (ThreadStacks.Storage U) C
• dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C
• vtable : VTableHooks Memory.Provenance (State K U) C (FnVal O) (ABI.FnAbi MIR.TyId)
• dynamicFuel : Nat
• atomic : AtomicAccessHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)
• backend : State K U → Except StepError (RaceMode.Handler B)
• extras : MemoryExtras.Hooks K (User U) P

def Miri.Interpreter.LinuxFutexMachine.objectHooks {K U C P O B Host System TZ Timestamp ErrorHost : Type} (h : Hooks K U C P O B Host System TZ Timestamp ErrorHost) : ObjectHooks K U C P O B

A full futex capability always contains the same genuine physical fields. Projecting them supports time-independent pthread object construction without creating a second memory, backend, atomic, or metadata state.

Equations

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

def Miri.Interpreter.LinuxFutexMachine.ioErrors {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : Hooks K U C P O B H Y Z T E) (choice : C) : IoError.Hooks (State K U) E

Equations

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

def Miri.Interpreter.LinuxFutexMachine.newFutex {K U C P O B H Y Z T E : Type} (h : Hooks K U C P O B H Y Z T E) : M K U Concurrency.FutexRuntime.Ref

Equations

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

def Miri.Interpreter.LinuxFutexMachine.sourceError : Concurrency.SyncError → StepError

Equations

• Miri.Interpreter.LinuxFutexMachine.sourceError x✝ = Miri.Interpreter.StepError.invalidProgram (toString "futex synchronization invariant: " ++ toString (reprStr x✝))

def Miri.Interpreter.LinuxFutexMachine.runtime {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : Hooks K U C P O B H Y Z T E) (choice : C) : Concurrency.FutexRuntime.Hooks (State K U) (MPlaceTy Memory.Provenance)

Equations

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

def Miri.Interpreter.LinuxFutexMachine.onAccess {P K U : Type} (embedding : Payload P) (other : P → Concurrency.SyncObject.AccessKind → PlaceMachine.MachineM K (User U) Unit) (value : P) (kind : Concurrency.SyncObject.AccessKind) : PlaceMachine.MachineM K (User U) Unit

Futex metadata's source on_access and provenance visitor are empty. Other payload variants keep their actual existing synchronization behavior.

Equations

• Miri.Interpreter.LinuxFutexMachine.onAccess embedding other value kind = match embedding.project value with | some val => pure () | none => other value kind

def Miri.Interpreter.LinuxFutexMachine.metadataFromObjectHooks {K U C P O B : Type} [DecidableEq K] (h : ObjectHooks K U C P O B) : Concurrency.SyncObject.MetadataHooks (State K U) Concurrency.FutexRuntime.Ref

Equations

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

def Miri.Interpreter.LinuxFutexMachine.metadata {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : Hooks K U C P O B H Y Z T E) : Concurrency.SyncObject.MetadataHooks (State K U) Concurrency.FutexRuntime.Ref

Equations

• Miri.Interpreter.LinuxFutexMachine.metadata h = Miri.Interpreter.LinuxFutexMachine.metadataFromObjectHooks (Miri.Interpreter.LinuxFutexMachine.objectHooks h)

def Miri.Interpreter.LinuxFutexMachine.bind {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : Hooks K U C P O B H Y Z T E) (choice : C) (base : LinuxFutex.Hooks (State K U) Concurrency.FutexRuntime.Ref) : LinuxFutex.Hooks (State K U) Concurrency.FutexRuntime.Ref

Equations

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

def Miri.Interpreter.LinuxFutexMachine.bindForSyscall {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : Hooks K U C P O B H Y Z T E) (choice : C) (takeArgs : Array LinuxFutex.ArgType → ShimSignatures.Varargs Memory.Provenance → EStateM StepError (State K U) (Array (OpTy Memory.Provenance))) (libcI32 : String → EStateM StepError (State K U) Int32) (hostUsizeBits : Nat) : LinuxFutex.Hooks (State K U) Concurrency.FutexRuntime.Ref

Build the source syscall-facing futex hooks directly from the physical futex constructor. The syscall ABI checker and target constants remain explicit inputs; all memory, atomic, callback, deadline, and errno effects come from this same runtime-owned machine hook record.

Equations

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