Documentation

Miri.Concurrency.Termination

Miri termination and reporting categories #

This is the pinned diagnostics.rs::TerminationInfo classification boundary. It distinguishes program exit, abnormal termination, user interruption, unsupported operations, UB reports and deadlock reports. report_result labels only DataRace, StackedBorrowsUb, and TreeBorrowsUb as UB among these machine-stop variants. This is a reporting taxonomy, not a proof that a program is safe or a model of all interpreter errors.

source
inductive Miri.Concurrency.TerminationInfo :
Type

The machine-stop variants in pinned Miri's TerminationInfo. Diagnostic-only payloads are retained as strings; pointer/span/history fields do not affect the report_result category.

Instances For
    source
    @[instance_reducible]
    instance Miri.Concurrency.instDecidableEqTerminationInfo :
    DecidableEq TerminationInfo
    Equations
    source
    def Miri.Concurrency.instDecidableEqTerminationInfo.decEq (x✝ x✝¹ : TerminationInfo) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Miri.Concurrency.instReprTerminationInfo :
      Repr TerminationInfo
      Equations
      source
      def Miri.Concurrency.instReprTerminationInfo.repr :
      TerminationInfo → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        inductive Miri.Concurrency.TerminationReport :
        Type

        Observable category used by report_result; diagnostic rendering details and spans are deliberately outside this classification.

        Instances For
          source
          @[instance_reducible]
          instance Miri.Concurrency.instDecidableEqTerminationReport :
          DecidableEq TerminationReport
          Equations
          source
          def Miri.Concurrency.instDecidableEqTerminationReport.decEq (x✝ x✝¹ : TerminationReport) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            def Miri.Concurrency.instReprTerminationReport.repr :
            TerminationReport → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Miri.Concurrency.instReprTerminationReport :
              Repr TerminationReport
              Equations
              source
              def Miri.Concurrency.TerminationInfo.report :
              TerminationInfo → TerminationReport

              Classification from the pinned diagnostics.rs::report_result match.

              Equations
              Instances For
                source
                def Miri.Concurrency.TerminationInfo.isUbReport (info : TerminationInfo) :
                Bool

                Only actual borrow-checker UB and data-race termination variants receive the Undefined Behavior report label in report_result.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Miri.Concurrency.TerminationInfo.deadlocks_are_not_ub (info : TerminationInfo) (h : info = globalDeadlock ∨ info = localDeadlock) :
                  info.isUbReport = false
                  source
                  @[simp]
                  theorem Miri.Concurrency.TerminationInfo.abort_is_not_ub (message : String) :
                  (abort message).isUbReport = false
                  source
                  @[simp]
                  theorem Miri.Concurrency.TerminationInfo.unsupported_is_not_ub (message : String) :
                  (unsupportedInIsolation message).isUbReport = false