Documentation

Miri.Input.EvalWindowsSyncTimeConstruction

Canonical source construction for Windows time and synchronization. Time delegates its guest memory, environment, clock and typed-runtime wiring to the shared source time constructor. Windows INIT_ONCE/WaitOnAddress hooks are derived here from exact compiler facts, Main memory, the shared typed sync arena, the source atomic backend and the canonical deadline registry.

source
@[reducible, inline]
abbrev Miri.Input.EvalWindowsSyncTimeConstruction.Payload (Os R P H D O Aff B Host : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalWindowsSyncTimeConstruction.State (Os R P H D O Aff B Host : Type) :
    Type
    Equations
    Instances For
      source
      def Miri.Input.EvalWindowsSyncTimeConstruction.syncFromSource {Os R P H D O Aff B Host C Error Instant System : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (objects : Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Host)) (atomic : Interpreter.AtomicAccessHooks Memory.Provenance (State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (deadline : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Inner (EvalCoreMachine.World Os R P H D O Aff B Host)) Instant System) (errors : Interpreter.IoError.Hooks (State Os R P H D O Aff B Host) Error) (compatibilityBudget : Nat) :
      Except Interpreter.StepError (Interpreter.WindowsSyncDispatch.Hooks (State Os R P H D O Aff B Host) Concurrency.TypedSyncRuntime.Ref)

      Build Windows synchronization behavior over the canonical Main state and the one typed synchronization arena. The supplied atomic and deadline hooks are the physical source leaves already selected for that Main machine; all guest pointers, constants, layouts, ABI checks and transmutation are derived from main and p.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Miri.Input.EvalWindowsSyncTimeConstruction.timeFromSource {Os R P H D O Aff B Poll Instant System Native Profiler C Error TZ Timestamp : Type} [DecidableEq Memory.MiriMemoryKind] [DecidableEq Os] (p : CompilerProviders.Prepared) (memory : EvalWindowsEnvironmentConstruction.Memory Os R P H D O Aff B (EvalTimeConstruction.Host Poll Instant System H D O Native Profiler) C) (environmentHost : EvalHostRuntimeConstruction.EnvironmentHostEffects (EvalWindowsEnvironmentConstruction.InnerControl Os R P H D O Aff B (EvalTimeConstruction.Host Poll Instant System H D O Native Profiler))) (osHost : EvalHostRuntimeConstruction.OsHostEffects Os) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState (EvalTimeConstruction.Stored Os R P H D O Aff B Poll Instant System Native Profiler)) O) (syncEffects : Interpreter.TypedSyncMachine.Effects (EvalTypedSyncMachine.State Os R P H D O Aff B Poll Instant System Native Profiler)) (errors : Interpreter.IoError.Hooks (EvalTimeConstruction.State Os R P H D O Aff B Poll Instant System Native Profiler) Error) (clock : Interpreter.Clock.HostHooks Instant System (EvalTimeConstruction.State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → EStateM Interpreter.StepError (EvalTimeConstruction.State Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) (timezoneString : Os → Except Unit String) (communicate : Bool) (host : EvalTimeConstruction.HostEffects (EvalTimeConstruction.State Os R P H D O Aff B Poll Instant System Native Profiler) TZ Timestamp) :
        Except Interpreter.StepError (Interpreter.TimeShims.Hooks (State Os R P H D O Aff B (EvalTimeConstruction.Host Poll Instant System H D O Native Profiler)) Instant System TZ Timestamp)

        Construct Windows time shims from the same initialized environment and memory bundle used by the source Windows components. Only chrono's UTC/timezone operations and host OsString conversion remain explicit leaves.

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