Concrete return and OS-thread-ID effects for the pthread wrapper family. Shared ThreadStacks supplies the authoritative active thread and liveness.

def Miri.Interpreter.UnixThreadDispatchMachine.bind {K U C D B I : Type} (place : PlaceHooks Memory.Provenance (ThreadStacks.State K U) C MachineHooks.FrameExtra) (choice : C) (thread : UnixThread.Hooks (ThreadStacks.State K U)) (base : UnixThreadDispatch.Hooks (ThreadStacks.State K U) D B I) : UnixThreadDispatch.Hooks (ThreadStacks.State K U) D B I

Equations

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