Uploaded image for project: 'Core Server'
  1. Core Server
  2. SERVER-43593

Deploy TLA+ trace checker to Evergreen

    XMLWordPrintableJSON

Details

    • Icon: New Feature New Feature
    • Resolution: Won't Fix
    • Icon: Major - P3 Major - P3
    • None
    • None
    • Replication
    • None
    • Replication

    Description

      Select some/all replication fuzz tests for checking. At the beginning of these fuzz tests, disable oplog truncation and enable the logging component that is introduced for the sake of trace checking. At the end of these tests, run the scripts that extract an execution trace and compare it to our selected TLA+ specs. Output a useful report and fail the test if the actual trace is not permitted by one of the specs.

      Attachments

        Activity

          People

            backlog-server-repl Backlog - Replication Team
            jesse@mongodb.com A. Jesse Jiryu Davis
            Votes:
            0 Vote for this issue
            Watchers:
            2 Start watching this issue

            Dates

              Created:
              Updated:
              Resolved: