Futex/clock views into the final World.host and shared callback supply. No callback closure arena, clock, address map or futex table is duplicated.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

def Miri.Input.EvalSyncMachine.views {Os R P H D O Aff B Poll Instant System Native Profiler : Type} : Interpreter.LinuxFutexMachine.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.EvalSyncMachine.deadlines {Instant System Os R P H D O Aff B Poll Native Profiler : Type} (host : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (communicate : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Bool) (systemDurationSince : System → System → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) (invoke : Nat → Concurrency.UnblockKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit) : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Instant System

Equations

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

def Miri.Input.EvalSyncMachine.errors {Os R P H D O Aff B Poll Instant System Native Profiler E : Type} (u32Layout : Interpreter.LocalLayout) (base : Interpreter.IoError.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) E) : Interpreter.IoError.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) E

Actual per-thread errno references are held by the source thread record, with typed pointers in the one shared runtime side table. The caller's machine allocation provider remains required; byte reads/writes are closed by bind.

Equations

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

def Miri.Input.EvalSyncMachine.hooks {Os R P H D O Aff B Poll Instant System Native Profiler C X TermHost Z T E : Type} (prepared : CompilerFactAdapters.Prepared) (core : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) C O X TermHost) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (World Os R P H D O Aff B Poll Instant System Native Profiler)))) (embedding : Interpreter.LinuxFutexMachine.Payload P) (sync : P → Concurrency.SyncObject.AccessKind → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (weakError : Concurrency.StoreBufferAllocError → Interpreter.StepError) (time : Interpreter.TimeShims.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Instant System Z T) (deadline : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Instant System) (io : Interpreter.IoError.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) E) (communicate : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Bool) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) (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)

Install final World-owned storage and physical dictionaries from the already closed core. Remaining arguments are typed compiler/host policies.

Equations

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

def Miri.Input.EvalSyncMachine.runtime {Os R P H D O Aff B Poll Instant System Native Profiler Ref V Dest : Type} (base : Concurrency.SyncRuntime.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Ref V Dest) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User 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) Ref V Dest)

The general pthread/Windows/init-once/readiness runtime uses the same source backend sum, optional clocks and actual thread stack manager as futex.

Equations

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

def Miri.Input.EvalSyncMachine.invoke {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) (choice : C) (other : Nat → Concurrency.UnblockKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (token : Nat) (kind : Concurrency.UnblockKind) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Called by the actual callback dispatcher after it selects the callback's thread. Other callback families retain their source interpreter.

Equations

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