Documentation

Miri.Interpreter.TimeShimMachine

Canonical Clock/DeadlineMachine bindings for time and synchronization shims. Registry tokens retain actual typed clock values; they are never timestamps.

source
def Miri.Interpreter.TimeShimMachine.bind {K U H Y Z T : Type} (clock : DeadlineMachine.Hooks K U H Y) (base : TimeShims.Hooks (MachineHooks.State K U) H Y Z T) :
TimeShims.Hooks (MachineHooks.State K U) H Y Z T
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Interpreter.TimeShimMachine.bindWindows {K U H Y R : Type} (clock : DeadlineMachine.Hooks K U H Y) (base : WindowsSync.Hooks (MachineHooks.State K U) R) :
    WindowsSync.Hooks (MachineHooks.State K U) R
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Interpreter.TimeShimMachine.bindPthread {K U H Y R : Type} (clock : DeadlineMachine.Hooks K U H Y) (base : PthreadSync.Hooks (MachineHooks.State K U) R Clock.Duration) :
      PthreadSync.Hooks (MachineHooks.State K U) R Clock.Duration
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Miri.Interpreter.TimeShimMachine.invokeSyncCallback {K U R V D : Type} (runtime : Concurrency.SyncRuntime.Hooks (MachineHooks.State K U) R V D) (token : Nat) (kind : Concurrency.UnblockKind) :
        MachineHooks.M K U Unit

        DeadlineMachine already selects/restores the callback thread. This executes only the typed registered closure, avoiding a second restoration.

        Equations
        Instances For