Documentation

Miri.Input.EvalUnixAffinityConstruction

Source CPU-affinity shims over the canonical thread runtime and guest memory. The mask state is the same MachineGCRoots.Storage.threads.affinity field inherited by newly created threads; no host-derived mask or shadow thread table is introduced.

@[reducible, inline]
abbrev Miri.Input.EvalUnixAffinityConstruction.Other (Raw Listener TcpStream Error : Type) :
Equations
Instances For
    @[reducible, inline]
    abbrev Miri.Input.EvalUnixAffinityConstruction.World (Os R P H D B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]
      abbrev Miri.Input.EvalUnixAffinityConstruction.Stored (Os R P H D B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Miri.Input.EvalUnixAffinityConstruction.handlerFromSource {Os R P H D B Poll Instant System Native Profiler Raw Listener TcpStream Error C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control (Stored Os R P H D B Poll Instant System Native Profiler Raw Listener TcpStream Error)) C Payload) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (EvalUnixSourceConstruction.State Os R P H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error Interpreter.EnvVars.Kind) (place : Interpreter.PlaceHooks Memory.Provenance (EvalUnixSourceConstruction.State Os R P H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (EvalUnixSourceConstruction.State Os R P H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) :
        Interpreter.UnixForeign.OptionalHandler (EvalUnixSourceConstruction.State Os R P H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error)

        Build the recognized affinity handler at the final source rebind seam. Only the canonical EnvironmentMemory, environment, common foreign Core, place writer and execution choice enter. Scalar/pointer reads, guest bytes, thread-mask storage, TID mapping, errno, compiler layouts/constants and shim ABI are all derived here from those source owners.

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