Source-owned synchronization callback adapters. The selected backend, target word size, callback writes, memory access hooks, and callback shims are derived from the live source state and final execution configuration. Only host errno/Windows plumbing and host clock/time operations remain residuals.
@[reducible, inline]
abbrev
Miri.Input.EvalCallbackSyncConstruction.World
(Os R H D O Aff B Poll Instant System Native Profiler : Type)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Miri.Input.EvalCallbackSyncConstruction.User
(Os R H D O Aff B Poll Instant System Native Profiler : Type)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Miri.Input.EvalCallbackSyncConstruction.State
(Os R H D O Aff B Poll Instant System Native Profiler : Type)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Miri.Input.EvalCallbackSyncConstruction.M
(Os R H D O Aff B Poll Instant System Native Profiler A : Type)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
Miri.Input.EvalCallbackSyncConstruction.HostEffects
(Os R H D O Aff B Poll Instant System Native Profiler ErrorHost : Type)
:
Genuine platform residuals used by synchronization wrappers. Memory writes,
backend selection, pointer width, and source error-pointer ownership are bound
by sourceEffects; this record contains only actual host error translation and
Windows-specific return/error effects.
- ioError : Interpreter.IoError.Hooks (State Os R H D O Aff B Poll Instant System Native Profiler) ErrorHost
- windowsTrue : EStateM Interpreter.StepError (State Os R H D O Aff B Poll Instant System Native Profiler) Int32
- windowsFalse : EStateM Interpreter.StepError (State Os R H D O Aff B Poll Instant System Native Profiler) Int32
- windowsTimeoutError : EStateM Interpreter.StepError (State Os R H D O Aff B Poll Instant System Native Profiler) Unit
Instances For
def
Miri.Input.EvalCallbackSyncConstruction.sourceEffects
{Os R H D O Aff B Poll Instant System Native Profiler C ErrorHost : Type}
[DecidableEq Memory.MiriMemoryKind]
(prepared : CompilerFactAdapters.Prepared)
(configuration : HostRuntime.Configuration)
(place :
Interpreter.PlaceHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
Interpreter.MachineHooks.FrameExtra)
(choice : C)
(host : HostEffects Os R H D O Aff B Poll Instant System Native Profiler ErrorHost)
:
M Os R H D O Aff B Poll Instant System Native Profiler
(Interpreter.TypedSyncMachine.Effects
(Interpreter.MachineHooks.State Memory.MiriMemoryKind
(EvalSyncMachine.User Os R EvalSyncObjectAccess.Payload H D O Aff B Poll Instant System Native Profiler)))
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalCallbackSyncConstruction.objectHooksFromSource
{Os R H D O Aff B Poll Instant System Native Profiler C : Type}
[DecidableEq Memory.MiriMemoryKind]
(prepared : CompilerFactAdapters.Prepared)
(access :
Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(allocation :
Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(compiler :
Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler) C)
(dynamic :
Interpreter.DynamicLayoutHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C)
(vtable :
Interpreter.VTableHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
(Interpreter.FnVal O) (ABI.FnAbi MIR.TyId))
(dynamicFuel : Nat)
(atomic :
Interpreter.AtomicAccessHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
(Interpreter.RuntimePlace Memory.Provenance))
(extras :
Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R H D O Aff B Poll Instant System Native Profiler)
EvalSyncObjectAccess.Payload)
(pointers :
Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind
(Interpreter.ValidityMachine.Control
(Interpreter.ThreadStacks.Storage (World Os R H D O Aff B Poll Instant System Native Profiler))))
:
Interpreter.LinuxFutexMachine.ObjectHooks Memory.MiriMemoryKind
(World Os R H D O Aff B Poll Instant System Native Profiler) C EvalSyncObjectAccess.Payload O B
Build the actual time-independent physical synchronization projection from the live Core memory/backend fields. It has no futex clock, deadline, errno or isolation input, so pthread object metadata remains usable when optional time host capabilities are absent. The projected object storage is the existing HostRuntime.sync view, not a new registry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalCallbackSyncConstruction.futexHooksWithReader
{Os R H D O Aff B Poll Instant System Native Profiler C ErrorHost Z T : Type}
[DecidableEq Memory.MiriMemoryKind]
(prepared : CompilerFactAdapters.Prepared)
(access :
Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(allocation :
Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(compiler :
Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler) C)
(dynamic :
Interpreter.DynamicLayoutHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C)
(vtable :
Interpreter.VTableHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
(Interpreter.FnVal O) (ABI.FnAbi MIR.TyId))
(dynamicFuel : Nat)
(atomic :
Interpreter.AtomicAccessHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
(Interpreter.RuntimePlace Memory.Provenance))
(extras :
Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R H D O Aff B Poll Instant System Native Profiler)
EvalSyncObjectAccess.Payload)
(pointers :
Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind
(Interpreter.ValidityMachine.Control
(Interpreter.ThreadStacks.Storage (World Os R H D O Aff B Poll Instant System Native Profiler))))
(configuration : HostRuntime.Configuration)
(readTimespec :
Interpreter.MPlaceTy Memory.Provenance →
M Os R H D O Aff B Poll Instant System Native Profiler (Option Interpreter.Clock.Duration))
(deadline :
Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R H D O Aff B Poll Instant System Native Profiler)
Instant System)
(errors : Interpreter.IoError.Hooks (State Os R H D O Aff B Poll Instant System Native Profiler) ErrorHost)
:
M Os R H D O Aff B Poll Instant System Native Profiler
(Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind
(World Os R H D O Aff B Poll Instant System Native Profiler) C EvalSyncObjectAccess.Payload O B Instant System Z T
ErrorHost)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalCallbackSyncConstruction.futexHooks
{Os R H D O Aff B Poll Instant System Native Profiler C Z T ErrorHost : Type}
[DecidableEq Memory.MiriMemoryKind]
(prepared : CompilerFactAdapters.Prepared)
(access :
Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(allocation :
Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(compiler :
Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler) C)
(dynamic :
Interpreter.DynamicLayoutHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C)
(vtable :
Interpreter.VTableHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
(Interpreter.FnVal O) (ABI.FnAbi MIR.TyId))
(dynamicFuel : Nat)
(atomic :
Interpreter.AtomicAccessHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
(Interpreter.RuntimePlace Memory.Provenance))
(extras :
Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R H D O Aff B Poll Instant System Native Profiler)
EvalSyncObjectAccess.Payload)
(pointers :
Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind
(Interpreter.ValidityMachine.Control
(Interpreter.ThreadStacks.Storage (World Os R H D O Aff B Poll Instant System Native Profiler))))
(configuration : HostRuntime.Configuration)
(time : Interpreter.TimeShims.Hooks (State Os R H D O Aff B Poll Instant System Native Profiler) Instant System Z T)
(deadline :
Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R H D O Aff B Poll Instant System Native Profiler)
Instant System)
(errors : Interpreter.IoError.Hooks (State Os R H D O Aff B Poll Instant System Native Profiler) ErrorHost)
:
M Os R H D O Aff B Poll Instant System Native Profiler
(Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind
(World Os R H D O Aff B Poll Instant System Native Profiler) C EvalSyncObjectAccess.Payload O B Instant System Z T
ErrorHost)
Compatibility wrapper for callers with complete time-shim hooks. Futex only consumes the compiler-checked timespec reader; its deadline remains the separately supplied canonical DeadlineMachine capability.
Equations
- One or more equations did not get rendered due to their size.