Documentation

Miri.Input.EvalSyncObjectAccess

Canonical source SyncObj metadata and access semantics for the actual EvalWorld. This lower module is shared by Core and callback construction; it does not depend on EvalConfigurationCore or startup assembly.

source
@[reducible, inline]
abbrev Miri.Input.EvalSyncObjectAccess.Payload :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalSyncObjectAccess.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.EvalSyncObjectAccess.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.EvalSyncObjectAccess.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.EvalSyncObjectAccess.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.EvalSyncObjectAccess.typedEmbedding :
            Interpreter.TypedSyncObjectMachine.Payload EvalSyncPayload.Payload
            Equations
            Instances For
              source
              def Miri.Input.EvalSyncObjectAccess.linuxFutexEmbedding :
              Interpreter.LinuxFutexMachine.Payload EvalSyncPayload.Payload
              Equations
              Instances For
                source
                def Miri.Input.EvalSyncObjectAccess.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

                Typed pthread/Windows/macOS metadata checks its live wait queue for all access kinds. Linux futex metadata has Miri's default empty SyncObj callback; unknown payloads cannot enter this source-owned sum.

                Equations
                Instances For
                  source
                  def Miri.Input.EvalSyncObjectAccess.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
                  Equations
                  Instances For