Documentation

Miri.Input.EvalForeignSyncMachine

Final World/HostRuntime synchronization selection in the foreign-item chain. Source handler selection and object construction precede the ordinary Unix/Windows source dispatch; no function-valued registry enters production.

source
@[reducible, inline]
abbrev Miri.Input.EvalForeignSyncMachine.World (Os R P H D O Aff B Poll Instant System Native Profiler : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalForeignSyncMachine.User (Os R P H D O Aff B Poll Instant System Native Profiler : Type) :
    Type
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Miri.Input.EvalForeignSyncMachine.Inner (Os R P H D O Aff B Poll Instant System Native Profiler : Type) :
      Type
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Miri.Input.EvalForeignSyncMachine.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) :
        Type
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Miri.Input.EvalForeignSyncMachine.objectsFromPhysical {Os R P H D O Aff B Poll Instant System Native Profiler C : Type} (h : Interpreter.LinuxFutexMachine.ObjectHooks Memory.MiriMemoryKind (World Os R P H D O Aff B Poll Instant System Native Profiler) C P O B) (embedding : Interpreter.TypedSyncObjectMachine.Payload P) (e : Interpreter.TypedSyncMachine.Effects (Inner Os R P H D O Aff B Poll Instant System Native Profiler)) (choice : C) (u8Layout : Interpreter.LocalLayout) (os : String) (namedGlobals : CompilerNamedGlobals.Prepared) (globalMemory : CompilerLinkSections.Memory Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) O) :
          EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Poll Instant System Native Profiler))
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.EvalForeignSyncMachine.objects {Os R P H D O Aff B Poll Instant System Native Profiler C Z T E : Type} (h : Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind (World Os R P H D O Aff B Poll Instant System Native Profiler) C P O B Instant System Z T E) (embedding : Interpreter.TypedSyncObjectMachine.Payload P) (e : Interpreter.TypedSyncMachine.Effects (Inner Os R P H D O Aff B Poll Instant System Native Profiler)) (choice : C) (u8Layout : Interpreter.LocalLayout) (os : String) (namedGlobals : CompilerNamedGlobals.Prepared) (globalMemory : CompilerLinkSections.Memory Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) O) :
            EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Poll Instant System Native Profiler))
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Miri.Input.EvalForeignSyncMachine.unix {Os R P H D O Aff B Poll Instant System Native Profiler Place HM Time E Kind ReadDir DirEntry Duration PollIter AddrIter TZ Timestamp Block Instance : Type} (objects : Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (h : Interpreter.UnixForeign.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Place H D O Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration PollIter AddrIter Instant System TZ Timestamp Block Instance) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place Concurrency.TypedSyncRuntime.Dest (Memory.Pointer (Option Memory.Provenance)) Block Instance) :
              Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Block Instance

              This returns the actual foreign dispatch dictionary consumed by calls, with every Unix synchronization family selected from the canonical factory.

              Equations
              Instances For
                source
                def Miri.Input.EvalForeignSyncMachine.windows {Os R P H D O Aff B Poll Instant System Native Profiler Place FD HM Time E Kind TZ Timestamp Block Instance : Type} [DecidableEq Os] (objects : Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (h : Interpreter.WindowsForeign.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Place FD H D Os HM Time E Kind Concurrency.TypedSyncRuntime.Ref Instant System TZ Timestamp Block Instance) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place Concurrency.TypedSyncRuntime.Dest (Memory.Pointer (Option Memory.Provenance)) Block Instance) :
                Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Block Instance
                Equations
                Instances For