Canonical callback-aware futex construction. Futex requires only a checked compiler timespec reader plus the real shared deadline registry; constructing it does not require chrono, UTC, or a full TimeShims dictionary. The source callback builder supplies the already-routed deadline in the inner state that owns the futex/deadline stores.
@[reducible, inline]
abbrev
Miri.Input.EvalCallbackFutexConstruction.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.EvalCallbackFutexConstruction.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.EvalCallbackFutexConstruction.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
def
Miri.Input.EvalCallbackFutexConstruction.readTimespecFromSource
{Os R H D O Aff B Poll Instant System Native Profiler C : Type}
(runtime : RuntimeMetadata)
(access :
Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind
(User Os R H D O Aff B Poll Instant System Native Profiler))
(projection :
Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
Interpreter.MachineHooks.FrameExtra)
(choice : C)
(place : Interpreter.MPlaceTy Memory.Provenance)
:
EStateM Interpreter.StepError (State Os R H D O Aff B Poll Instant System Native Profiler)
(Option Interpreter.Clock.Duration)
Parse a Linux futex timespec using the actual pointee layout supplied by
compiler-checked shim transmutation and the same effectful field projection as
source memory. Invalid nanoseconds retain TimeShims.readTimespec's
none result; negative seconds and overflow remain visible failures.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalCallbackFutexConstruction.fromSource
{Os R H D O Aff B Poll Instant System Native Profiler C ErrorHost Zone Timestamp : 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)
(projection :
Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R H D O Aff B Poll Instant System Native Profiler) C
Interpreter.MachineHooks.FrameExtra)
(choice : C)
(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)
:
EStateM Interpreter.StepError (State 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 Zone
Timestamp ErrorHost)
Assemble physical futex hooks from the exact Core projections, its callback-aware inner-state deadline and compiler layout. Core constructs that deadline once from the final callback router. The result shares HostRuntime futex/deadline registries, real memory/atomic state, and typed sync effects.
Equations
- One or more equations did not get rendered due to their size.