Documentation

Miri.Interpreter.WindowsForeignMachine

Production composition on the canonical full ThreadStacks machine state. Main startup, ExitCalled, FLS/TLS destructors and function-pointer resolution share the same registries, memory and actual thread stacks.

source
def Miri.Interpreter.WindowsForeignMachine.bindSynchronization {S Place FD H D Os HM T E Kind Host System TZ Timestamp B I : Type} (objects : ForeignSyncMachine.Objects S) (h : WindowsForeign.Hooks S Place FD H D Os HM T E Kind Concurrency.TypedSyncRuntime.Ref Host System TZ Timestamp B I) :
WindowsForeign.Hooks S Place FD H D Os HM T E Kind Concurrency.TypedSyncRuntime.Ref Host System TZ Timestamp B I

Select canonical typed init-once/futex objects in the actual Windows foreign dispatcher; no legacy function registry is supplied.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Interpreter.WindowsForeignMachine.bind {Os U C Other X FnABI ArgABI Aff P Kind Place FD H D HM T E R Host System TZ Timestamp B I : Type} [DecidableEq Os] (exit : WindowsExitMachine.Hooks U C Other X FnABI ArgABI Aff P) (choice : C) (systemAbi : X) (reuseClock : Option Concurrency.VectorIdx) (winLocal : Kind) (unwind : Unwind.Hooks Memory.MiriMemoryKind (ThreadStacks.Storage U) C Other) (embedDynamic : WindowsPlatform.DynamicSymbol → Other) (h : WindowsForeign.Hooks (MainMachine.State U) Place FD H D Os HM T E Kind R Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance (MainMachine.State U) Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) :
    ForeignItems.Hooks Memory.Provenance (MainMachine.State U) Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Interpreter.WindowsForeignMachine.bindLoop {U C Other X FnABI ArgABI Aff P : Type} (exit : WindowsExitMachine.Hooks U C Other X FnABI ArgABI Aff P) (base : RunLoopHooks (MainMachine.State U) C WindowsExitMachine.Callback) (scheduler : C → ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) :
      RunLoopHooks (WindowsExitMachine.State U) C WindowsExitMachine.Callback

      Pair the composed foreign chain with this scheduler adapter. Its callback sum includes main startup, ordinary TLS and ExitCalled; no callback stage is reconstructed from a different memory-only snapshot.

      Equations
      Instances For