Canonical source constructor for the FreeBSD _umtx_op platform arm. It consumes the already assembled Linux-futex physical projection and the same ForeignSyncMachine arena used by pthread and other synchronization. This does not add an object store, callback token supply, clock, or atomic backend.

def Miri.Input.EvalUnixFreeBsdConstruction.syncFromSource {U C P O B Instant System Zone Timestamp ErrorHost : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (objects : Interpreter.ForeignSyncMachine.Objects (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind U)) (choice : C) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind U) C Interpreter.MachineHooks.FrameExtra) (communicate : Bool) (futex : Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind U C P O B Instant System Zone Timestamp ErrorHost) : Interpreter.FreeBsdSync.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind U) Concurrency.TypedSyncRuntime.Ref

Construct the real FreeBSD synchronization dictionary on top of the exact same callback-aware atomic, deadline, error, memory, and typed-sync sources as the Linux futex constructor. time is the actual source time dictionary; a caller with no time capability must leave this platform arm unavailable and report Unsupported when _umtx_op is selected.

Equations

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

def Miri.Input.EvalUnixFreeBsdConstruction.handlerFromSource {S D B I ErrorHost : Type} (core : Interpreter.ForeignItems.Core Memory.Provenance S D (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (errors : Interpreter.IoError.Hooks S ErrorHost) (sync : Interpreter.FreeBsdSync.Hooks S Concurrency.TypedSyncRuntime.Ref) : String → ABI.FnAbi MIR.TyId → Array (Interpreter.OpTy Memory.Provenance) → Interpreter.MPlaceTy Memory.Provenance → EStateM Interpreter.StepError S (Option Interpreter.ForeignItems.EmulateItemResult)

Install the FreeBSD platform arm over the exact source ForeignItems.Core already selected by callback dispatch. The core is a source assembly result, not a caller-built platform hook record. With no actual time capability the untimed __error shim remains available and _umtx_op fails on demand.

Equations

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