Documentation

Miri.Input.EvalForeignSocketMachine

Terminal Unix source dispatcher: owned socket/file IO uses the same final HostRuntime arena as eventfd, poll and epoll.

source
@[reducible, inline]
abbrev Miri.Input.EvalForeignSocketMachine.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalForeignSocketMachine.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.EvalForeignSocketMachine.FD (H D O : Type) :
      Type
      Equations
      Instances For
        source
        def Miri.Input.EvalForeignSocketMachine.bind {Os R P H D O Aff B Poll Instant System Native Profiler E Iter Raw Listener TcpStream Host AddrIter HM Place Time Kind ReadDir DirEntry Duration TZ Timestamp Block Instance : Type} (io : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (sockets : EvalOwnedIoMachine.SocketBindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host AddrIter) (descriptor : Interpreter.SocketMachine.Descriptor O) (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) (resource : Nat) (sourceFiles : Interpreter.Files.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) H D O E HM) (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 Iter AddrIter Instant System TZ Timestamp Block Instance) :
        Interpreter.UnixForeign.Hooks (EvalForeignIoMachine.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 Iter AddrIter Instant System TZ Timestamp Block Instance
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Miri.Input.EvalForeignSocketMachine.unix {Os R P H D O Aff B Poll Instant System Native Profiler E Iter Raw Listener TcpStream Host AddrIter HM Place Time Kind ReadDir DirEntry Duration TZ Timestamp Block Instance : Type} (io : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (sockets : EvalOwnedIoMachine.SocketBindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host AddrIter) (descriptor : Interpreter.SocketMachine.Descriptor O) (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) (resource : Nat) (sourceFiles : Interpreter.Files.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) H D O E HM) (sync : 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 Iter 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 (EvalForeignIoMachine.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
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.EvalForeignSocketMachine.invoke {Os R P H D O Aff B Poll Instant System Native Profiler E Iter Raw Listener TcpStream Host AddrIter : Type} (io : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (sockets : EvalOwnedIoMachine.SocketBindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host AddrIter) (resource : Nat) (other : Nat → Concurrency.UnblockKind → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (token : Nat) (kind : Concurrency.UnblockKind) :
            EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For