One synchronization arena in the final HostRuntime, using the exact shared ThreadMachine token supply. This factory allocates no mirror clocks or stacks.

@[reducible, inline]

abbrev Miri.Input.EvalTypedSyncMachine.Host (Poll Instant System H D O Native Profiler : Type) : Type

Equations

• Miri.Input.EvalTypedSyncMachine.Host = Miri.Input.HostRuntime.Storage

@[reducible, inline]

abbrev Miri.Input.EvalTypedSyncMachine.World (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalTypedSyncMachine.World Os R P H D O Aff B Poll Instant System Native Profiler = Miri.Input.EvalSyncMachine.World Os R P H D O Aff B Poll Instant System Native Profiler

@[reducible, inline]

abbrev Miri.Input.EvalTypedSyncMachine.User (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalTypedSyncMachine.User Os R P H D O Aff B Poll Instant System Native Profiler = Miri.Input.EvalSyncMachine.User Os R P H D O Aff B Poll Instant System Native Profiler

@[reducible, inline]

abbrev Miri.Input.EvalTypedSyncMachine.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalTypedSyncMachine.State Os R P H D O Aff B Poll Instant System Native Profiler = Miri.Input.EvalSyncMachine.State Os R P H D O Aff B Poll Instant System Native Profiler

def Miri.Input.EvalTypedSyncMachine.views {Os R P H D O Aff B Poll Instant System Native Profiler : Type} : Interpreter.TypedSyncMachine.Views (World Os R P H D O Aff B Poll Instant System Native Profiler)

Equations

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

def Miri.Input.EvalTypedSyncMachine.effects {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (base : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler))

Validate actual None/VClock state when selecting the source handler; caller supplies concrete OS writes, not a registry or callback evaluator.

Equations

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

def Miri.Input.EvalTypedSyncMachine.runtime {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (e : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Concurrency.SyncRuntime.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest)

Equations

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

def Miri.Input.EvalTypedSyncMachine.invoke {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (e : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (other : Nat → Concurrency.UnblockKind → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (token : Nat) (kind : Concurrency.UnblockKind) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalTypedSyncMachine.Objects (S : Type) : Type

Equations

• Miri.Input.EvalTypedSyncMachine.Objects = Miri.Interpreter.ForeignSyncMachine.Objects

def Miri.Input.EvalTypedSyncMachine.objectsFromPhysical {Os R P H D O Aff B Poll Instant System Native Profiler C : Type} (h : Interpreter.LinuxFutexMachine.ObjectHooks Memory.MiriMemoryKind (World Os R P H D O Aff B Poll Instant System Native Profiler) C P O B) (embedding : Interpreter.TypedSyncObjectMachine.Payload P) (e : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (choice : C) (u8Layout : Interpreter.LocalLayout) (os : String) (namedGlobals : CompilerNamedGlobals.Prepared) (globalMemory : CompilerLinkSections.Memory Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) O) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Objects (State Os R P H D O Aff B Poll Instant System Native Profiler))

Final-World object factory from the actual physical memory/backend fields. It shares HostRuntime.sync and needs no clock, deadline or host-time input, so ordinary pthread operations do not wait for unused futex time support.

Equations

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

def Miri.Input.EvalTypedSyncMachine.objects {Os R P H D O Aff B Poll Instant System Native Profiler C Z T E : Type} (h : Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind (World Os R P H D O Aff B Poll Instant System Native Profiler) C P O B Instant System Z T E) (embedding : Interpreter.TypedSyncObjectMachine.Payload P) (e : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (choice : C) (u8Layout : Interpreter.LocalLayout) (os : String) (namedGlobals : CompilerNamedGlobals.Prepared) (globalMemory : CompilerLinkSections.Memory Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) O) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Objects (State Os R P H D O Aff B Poll Instant System Native Profiler))

Compatibility entry for callers that already have the full futex family; all physical object operations project to the same canonical state.

Equations

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