Source construction for Unix pthread and pthread-TLS bindings over the initialized MainMachine and its actual ThreadManager/TLS arena. Thread create, join, detach, names, current IDs, pthread keys, destructor identities and errno all use the shared execution state.

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.Payload (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalUnixThreadTlsConstruction.Payload Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalCoreMachine.World Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalUnixThreadTlsConstruction.State Os R P H D O Aff B Host = Miri.Interpreter.MainMachine.State (Miri.Input.EvalUnixThreadTlsConstruction.Payload Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.M (Os R P H D O Aff B Host A : Type) : Type

Equations

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

structure Miri.Input.EvalUnixThreadTlsConstruction.Components (S D B I : Type) : Type

• thread : Interpreter.UnixThreadDispatch.Hooks S D B I
• tls : Interpreter.UnixTlsDispatch.Hooks S D B I

def Miri.Input.EvalUnixThreadTlsConstruction.fromRuntime {Os R P H D O Aff B Host C E I : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (State Os R P H D O Aff B Host) Os E Interpreter.EnvVars.Kind) (signatures : Interpreter.ShimSignatures.Hooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.MPlaceTy Memory.Provenance) (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (hostUsizeBits stringScanBudget : Nat) : Except Interpreter.StepError (Components (State Os R P H D O Aff B Host) (Interpreter.MPlaceTy Memory.Provenance) B I)

Build source thread and pthread-TLS dispatch fields from compiler facts, the canonical main execution component, and its shared TLS arena. hostUsizeBits is the actual interpreter-host width used only at source host-size conversion boundaries; the guest usize layout is still compiler-derived.

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.SourceWorld (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.SourceUser (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.SourceState (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixThreadTlsConstruction.OuterSourceState (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

Unlike the legacy startup builder, this constructor is called at the actual source foreign boundary. Its function-call thunk is the bounded nested MIR configuration used by Core; the runtime thread manager, allocation, memory, errno, TLS arena, and backend are all the live EvalWorld fields.

def Miri.Input.EvalUnixThreadTlsConstruction.fromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error E C I : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os E Interpreter.EnvVars.Kind) (signatures : Interpreter.ShimSignatures.PrimitiveHooks Memory.Provenance (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (place : Interpreter.PlaceHooks Memory.Provenance (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (threadFunctions : Unit → Except Interpreter.StepError (Interpreter.FunctionCalls.Hooks Memory.Provenance (Interpreter.ThreadMachine.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState (SourceWorld Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error))) C Interpreter.MachineHooks.FrameExtra (EvalSocketStorage.Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId))) (spans : Interpreter.AllocationDriver.SpanHooks) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (EvalSocketStorage.Other Raw Listener TcpStream Error)) (hostUsizeBits stringScanBudget : Nat) : Except Interpreter.StepError (Components (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.MPlaceTy Memory.Provenance) B I)

Equations

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