Actual ThreadStacks creation, non-exclusive Windows joining, vector clocks, and the same TLS storage used by ThreadTlsMachine's destructor engine.

def Miri.Interpreter.WindowsThreadMachine.join {K U C O X F A Aff : Type} (h : ThreadMachine.Hooks K U C O X F A Aff) (choice : C) (joined : Concurrency.ThreadId) (value : Memory.Scalar Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : ThreadMachine.M K U Unit

Unlike pthread join, Windows permits repeated joins and joining oneself blocks. A closed/detached handle remains UB. Continuations use the canonical ThreadMachine join arena and resumeJoin consumes them before invocation.

Equations

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

def Miri.Interpreter.WindowsThreadMachine.bind {K U C O X F A Aff FD : Type} [DecidableEq K] (h : ThreadMachine.Hooks K U C O X F A Aff) (choice : C) (systemAbi : X) (reuseClock : Option Concurrency.VectorIdx) (base : WindowsThread.Hooks (ThreadStacks.State K U) FD) : WindowsThread.Hooks (ThreadStacks.State K U) FD

System ABI is a required target/compiler value, including x86 stdcall.

Equations

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

def Miri.Interpreter.WindowsThreadMachine.bindTls {U C O X F A Aff FD : Type} (h : ThreadTlsMachine.Hooks U C O X F A Aff) (base : WindowsThread.Hooks (ThreadTlsMachine.State U) FD) : WindowsThread.Hooks (ThreadTlsMachine.State U) FD

TLS and fiber-local keys share exactly the destructor engine's map.

Equations

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

def Miri.Interpreter.WindowsThreadMachine.bindNames {S Os Kind FD : Type} (strings : OsStrings.Hooks Memory.Provenance S Os Kind) (winLocal : Kind) (base : WindowsThread.Hooks S FD) : WindowsThread.Hooks S FD

Name allocation uses actual lossless host bytes conversion and WinLocal allocation; no UTF-8-only substitute or invented allocation identity.

Equations

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