Canonical pthread synchronization source hooks. The caller supplies the actual shared typed-sync object bundle and narrow machine/source leaves; this constructor derives pthread objects, memory checks, libc constants, timespec reads, deadlines, errno handling, shim signatures, and checked transmutation. It does not accept a completed PthreadSync or PthreadDispatch dictionary.

structure Miri.Input.EvalUnixPthreadConstruction.Leaves (K U C ErrorHost Instant System : Type) : Type

• objects : Interpreter.ForeignSyncMachine.Objects (Interpreter.ValidityMachine.State K U)
• access : Interpreter.ValidityMachine.Access K U
• projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C Interpreter.MachineHooks.FrameExtra
• place : Interpreter.PlaceHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C Interpreter.MachineHooks.FrameExtra
• choice : C
• deadline : Interpreter.DeadlineMachine.Hooks K (Interpreter.ValidityMachine.UserState U) Instant System
• ioError : Interpreter.IoError.Hooks (Interpreter.ValidityMachine.State K U) ErrorHost
• noIsolation : String → EStateM Interpreter.StepError (Interpreter.ValidityMachine.State K U) Unit
• checkSymbolClash : String → EStateM Interpreter.StepError (Interpreter.ValidityMachine.State K U) Unit

def Miri.Input.EvalUnixPthreadConstruction.fromSource {U C ErrorHost Instant System : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (compatibilityBudget : Nat) (leaves : Leaves Memory.MiriMemoryKind U C ErrorHost Instant System) : EStateM Interpreter.StepError (Interpreter.ValidityMachine.State Memory.MiriMemoryKind U) (Interpreter.PthreadDispatch.Hooks (Interpreter.ValidityMachine.State Memory.MiriMemoryKind U) Concurrency.TypedSyncRuntime.Ref Interpreter.Clock.Duration)

Assemble the portable pthread sync ABI over the actual shared object arena. Attribute/object writes use canonical guest memory, timed waits use the source HostRuntime deadline registry, and each ABI signature comes from the exact compiler shim table.

Equations

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