Connected Unix dispatch on canonical ThreadStacks state. Shared owned FD, readiness/event/poll registries and thread lifecycle effects remain authoritative.
@[reducible, inline]
Equations
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindSynchronization
{S Place H D Other Os HM Time E Kind ReadDir DirEntry Duration PollIter AddrIter Host System TZ Timestamp B I : Type}
(objects : ForeignSyncMachine.Objects S)
(h :
UnixForeign.Hooks S Place H D Other Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration
PollIter AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks S Place H D Other Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration
PollIter AddrIter Host System TZ Timestamp B I
Install actual HostRuntime-backed synchronization objects into every source Unix OS subchain before dispatch, including the macOS pthread aliases.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindIo
{K U H D Other Poll Host System ReadDir C E HM Place Os Time Kind DirEntry R Duration PollIter AddrIter TZ Timestamp B
I : Type}
[DecidableEq K]
(machine : ReadinessMachine.Hooks K (ThreadStacks.Storage U) H D Other)
(io : BlockingIo.Hooks (ThreadStacks.State K U) (FD H D Other) Poll Host)
(deadline : DeadlineMachine.Hooks K (ThreadStacks.Storage U) Host System)
(epoll : PollMachine.DescriptorHooks Other)
(directories : UnixFsMachine.DirectoryStore (ThreadStacks.Storage U) ReadDir)
(events : EventFdMachine.Store (ThreadStacks.Storage U) Other)
(access : PlaceMachine.AccessConfig K (ThreadStacks.Storage U))
(place : PlaceHooks Memory.Provenance (ThreadStacks.State K U) C MachineHooks.FrameExtra)
(choice : C)
(budget : Nat)
(otherMetadata : Other → ThreadStacks.M K U (Except (IoError.HostError E) HM ⊕ String))
(errorFromKind : IoError.ErrorKind → ThreadStacks.M K U (IoError.Error E))
(h :
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I
The outer poll executes actual blocking/readiness work in real thread contexts; all source family dispatchers then reuse this one result prefix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindSockets
{K U H D Other Receiver Listener Tcp E Poll Host AddrIter Place Os HM Time Kind ReadDir DirEntry R Duration PollIter
System TZ Timestamp B I : Type}
(machine : ReadinessMachine.Hooks K (ThreadStacks.Storage U) H D Other)
(descriptor : SocketMachine.Descriptor Other)
(store : SocketMachine.Store (ThreadStacks.Storage U) Receiver Listener Tcp E)
(blocking : ReadinessMachine.BlockingStore (ThreadStacks.Storage U) Poll)
(budget : Nat)
(tcp : TcpSocket.Hooks (ThreadStacks.State K U) (FD H D Other) Receiver Listener Tcp E Poll Host)
(options : SocketOptions.Hooks (ThreadStacks.State K U) (FD H D Other) E AddrIter)
(h :
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I × TcpSocket.Hooks (MachineHooks.State K (ThreadStacks.Storage U)) (SocketMachine.Ref H D Other) Receiver Listener Tcp E
Poll Host
Build socket protocol closures before the IO/FD adapter captures their actual vtable operations. Returns the bound TCP hooks so the caller can reuse that same BlockingIo manager for the single outer poll.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindThread
{K U C O X FnABI ArgABI Aff Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System
TZ Timestamp B I : Type}
[DecidableEq K]
(thread : ThreadMachine.Hooks K U C O X FnABI ArgABI Aff)
(access : PlaceMachine.AccessConfig K (ThreadStacks.Storage U))
(place : PlaceHooks Memory.Provenance (ThreadStacks.State K U) C MachineHooks.FrameExtra)
(choice : C)
(cAbi : X)
(reuseClock : Option Concurrency.VectorIdx)
(misalignment : Memory.Pointer (Option Memory.Provenance) → ABI.Align → ThreadStacks.M K U (Option Memory.Misalignment))
(h :
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I
Thread create/join/detach and current IDs bind real frames/clock state. System C ABI and optional reuse-clock choice are required source inputs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindAffinity
{K U C Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I :
Type}
[DecidableEq K]
(runtime : CpuAffinityMachine.Runtime U)
(access : PlaceMachine.AccessConfig K (ThreadStacks.Storage U))
(place : PlaceHooks Memory.Provenance (ThreadStacks.State K U) C MachineHooks.FrameExtra)
(choice : C)
(h :
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I
Canonical affinity masks, physical guest memory and actual Linux TID lookup share the thread adapter's PID communication policy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindMain
{U C O X FnABI ArgABI Aff P Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System
TZ Timestamp B I : Type}
(main : MainMachine.Hooks U C O X FnABI ArgABI Aff P)
(h :
UnixForeign.Hooks (MainMachine.State U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (MainMachine.State U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter
Host System TZ Timestamp B I
Actual macOS argc/argv cells, function-pointer resolution and late TLS atexit registration share the existing initialized MainMachine configuration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindTls
{U C O X FnABI ArgABI Aff P Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System
TZ Timestamp B I : Type}
(main : MainMachine.Hooks U C O X FnABI ArgABI Aff P)
(place : PlaceHooks Memory.Provenance (MainMachine.State U) C MachineHooks.FrameExtra)
(choice : C)
(misalignment : Memory.Pointer (Option Memory.Provenance) → ABI.Align → MainMachine.M U (Option Memory.Misalignment))
(h :
UnixForeign.Hooks (MainMachine.State U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (MainMachine.State U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter
Host System TZ Timestamp B I
Common pthread keys and macOS atexit use the same initialized TLS arena, actual source spans, compiler function identities and physical guest writes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindDynamic
{U C O X FnABI ArgABI Aff P Place B I H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host
System TZ Timestamp : Type}
(main : MainMachine.Hooks U C O X FnABI ArgABI Aff P)
(unwind : Unwind.Hooks Memory.MiriMemoryKind (ThreadStacks.Storage U) C O)
(choice : C)
(embed : UnixDynamic.Symbol → O)
(statics : U → ExternStatic.State)
(strings : MemoryShims.Hooks Memory.Provenance (MainMachine.State U) Place (MPlaceTy Memory.Provenance) B I)
(scanBudget : Nat)
(h :
UnixForeign.Hooks (MainMachine.State U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (MainMachine.State U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter
Host System TZ Timestamp B I
Dynamic functions, statics and unwind use the same function registry, initialized extern-static map and actual thread payload stack as execution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bindLinuxMemory
{U Payload C Host Extra Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter System TZ
Timestamp B I : Type}
(lens : FunctionPointers.AddressLens (ThreadStacks.Storage U) Payload)
(allocation : UnixMemoryMachine.Hooks Payload C Host Extra)
(choices : UnixMemoryMachine.Choices)
(h :
UnixForeign.Hooks (ThreadStacks.State Memory.MiriMemoryKind U) Place H D Other Os HM Time E Kind ReadDir DirEntry R
Duration PollIter AddrIter Host System TZ Timestamp B I)
:
UnixForeign.Hooks (ThreadStacks.State Memory.MiriMemoryKind U) Place H D Other Os HM Time E Kind ReadDir DirEntry R
Duration PollIter AddrIter Host System TZ Timestamp B I
Linux-specific Zero-growth realloc closes on the same physical address and allocation state through a checked, lawful user-record embedding.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.UnixForeignMachine.bind
{K U Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I :
Type}
(h :
UnixForeign.Hooks (ThreadStacks.State K U) Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter
AddrIter Host System TZ Timestamp B I)
(base :
ForeignItems.Hooks Memory.Provenance (ThreadStacks.State K U) Place (MPlaceTy Memory.Provenance)
(Memory.Pointer (Option Memory.Provenance)) B I)
:
ForeignItems.Hooks Memory.Provenance (ThreadStacks.State K U) Place (MPlaceTy Memory.Provenance)
(Memory.Pointer (Option Memory.Provenance)) B I
Final canonical chain; callers apply IO/thread/socket/compiler bindings before this operation, so no dispatcher captures an obsolete fallback chain.