Documentation

Miri.Input.EvalSyncObjectConstruction

Canonical source synchronization metadata access for the actual EvalWorld. Every pinned Miri SyncObj family is represented by either its typed source object in HostRuntime.sync or the Linux futex marker (whose source on_access implementation is the trait default). There is no caller-provided access callback and no successful fallback for an unrecognized metadata payload.

source
@[reducible, inline]
abbrev Miri.Input.EvalSyncObjectConstruction.Payload :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalSyncObjectConstruction.World (Os R 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
      @[reducible, inline]
      abbrev Miri.Input.EvalSyncObjectConstruction.User (Os R 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
        @[reducible, inline]
        abbrev Miri.Input.EvalSyncObjectConstruction.Machine (Os R 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
          @[reducible, inline]
          abbrev Miri.Input.EvalSyncObjectConstruction.M (Os R H D O Aff B Poll Instant System Native Profiler A : Type) :
          Type
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.EvalSyncObjectConstruction.typedEmbedding :
            Interpreter.TypedSyncObjectMachine.Payload Payload
            Equations
            Instances For
              source
              def Miri.Input.EvalSyncObjectConstruction.linuxFutexEmbedding :
              Interpreter.LinuxFutexMachine.Payload Payload
              Equations
              Instances For
                source
                def Miri.Input.EvalSyncObjectConstruction.onAccess {Os R H D O Aff B Poll Instant System Native Profiler : Type} :
                Payload → Concurrency.SyncObject.AccessKind → M Os R H D O Aff B Poll Instant System Native Profiler Unit
                Equations
                Instances For
                  source
                  def Miri.Input.EvalSyncObjectConstruction.linuxFutexOnAccess {Os R H D O Aff B Poll Instant System Native Profiler : Type} :
                  Payload → Concurrency.SyncObject.AccessKind → M Os R H D O Aff B Poll Instant System Native Profiler Unit

                  Compose the same canonical dispatcher with Miri's Linux futex-specific default implementation. This is used when building LinuxFutexMachine hooks; other source synchronization objects continue through onAccess.

                  Equations
                  Instances For
                    source
                    def Miri.Input.EvalSyncObjectConstruction.withCanonicalAccess {Os R H D O Aff B Poll Instant System Native Profiler C ClockHost : Type} (leaves : EvalConfigurationCore.Leaves Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost) :
                    EvalConfigurationCore.Leaves Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost

                    Install the source-owned SyncObj access behavior into the rest of a real EvalConfigurationCore input. The incoming sync field is intentionally overwritten; it cannot choose memory semantics.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Miri.Input.EvalSyncObjectConstruction.withCanonicalSourceAccess {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path C ClockHost I AddrIter : Type} (leaves : EvalConfigurationCore.SourceLeaves Os R Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter) :
                      EvalConfigurationCore.SourceLeaves Os R Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter

                      Source-specialized leaf binder. Its compiler/host state is the canonical Unix SourceHost, and its synchronization payload is fixed to Miri's typed objects plus Linux futex metadata. The source constructor cannot retain a caller-selected synchronization policy.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Miri.Input.EvalSyncObjectConstruction.makeFromSource {Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path C ClockHost I AddrIter : Type} [DecidableEq Os] (prepared : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter) (choice : C) :
                        Nat → Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalConfigurationCore.SourceUser Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (EvalConfigurationCore.SourceOther Raw Listener TcpStream Error) ABI.ExternAbi ClockHost)

                        Final source Core closure with its synchronization access callback constructed here. This is the production source-entry adapter: arbitrary SourceLeaves.sync values are discarded before Core builds its fixed MIR configuration.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Miri.Input.EvalSyncObjectConstruction.configuration {Os R H D O Aff B Poll Instant System Native Profiler C ClockHost : Type} (prepared : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (leaves : EvalConfigurationCore.Leaves Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost) (choice : C) :
                          Nat → Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R H D O Aff B Poll Instant System Native Profiler) C O ABI.ExternAbi ClockHost)

                          Source configuration constructor: all other compiler, memory, backend, and host inputs are unchanged, while the per-object access callback is derived from the actual world and source metadata sum.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Miri.Input.EvalSyncObjectConstruction.step {Os R H D O Aff B Poll Instant System Native Profiler C ClockHost : Type} (prepared : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (leaves : EvalConfigurationCore.Leaves Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost) (choice : C) (state : Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (World Os R H D O Aff B Poll Instant System Native Profiler))) :
                            Interpreter.StepResult (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (World Os R H D O Aff B Poll Instant System Native Profiler))) Bool
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def Miri.Input.EvalSyncObjectConstruction.validateInitialization {Os R H D O Aff B Poll Instant System Native Profiler C ClockHost : Type} (leaves : EvalConfigurationCore.Leaves Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost) :
                              EvalConfigurationCore.M Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) Unit
                              Equations
                              Instances For
                                source
                                def Miri.Input.EvalSyncObjectConstruction.environmentMemory {Os R H D O Aff B Poll Instant System Native Profiler C ClockHost : Type} [DecidableEq Memory.MiriMemoryKind] (prepared : EvalPreparation.Prepared) (execution : EvalExecutable.Core Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost) (leaves : EvalConfigurationCore.Leaves Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C ClockHost) (spans : Interpreter.AllocationDriver.SpanHooks) (choice : C) (alignment : Interpreter.ValidityMachine.AlignmentCheck) (stringScanBudget : Nat) :
                                EvalHostRuntimeConstruction.EnvironmentMemory (EvalStartupMemoryConstruction.InnerControl Os R Payload H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler)) C Payload

                                Startup argument/environment operations reuse the same metadata callback as MIR stepping, allocation, and deallocation.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def Miri.Input.EvalSyncObjectConstruction.sourceEnvironmentMemory {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C ClockHost ErrorHost Meta Path I AddrIter : Type} [DecidableEq Memory.MiriMemoryKind] (prepared : EvalPreparation.Prepared) (execution : EvalExecutable.Core Os R Payload H D (EvalConfigurationCore.SourceOther Raw Listener TcpStream Error) Aff B (EvalConfigurationCore.SourceHost Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C ClockHost) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter) (spans : Interpreter.AllocationDriver.SpanHooks) (choice : C) (alignment : Interpreter.ValidityMachine.AlignmentCheck) (stringScanBudget : Nat) :
                                  EvalHostRuntimeConstruction.EnvironmentMemory (EvalStartupMemoryConstruction.InnerControl Os R Payload H D (EvalConfigurationCore.SourceOther Raw Listener TcpStream Error) Aff B (EvalConfigurationCore.SourceHost Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) C Payload
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For