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

Add logging to be used by TLA+ trace checker for RaftMongo.tla

    XMLWordPrintableJSON

Details

    • Icon: New Feature New Feature
    • Resolution: Fixed
    • Icon: Major - P3 Major - P3
    • 4.3.3
    • None
    • Replication
    • None
    • Fully Compatible
    • Repl 2019-11-04, Repl 2019-11-18, Repl 2019-12-02, Repl 2019-12-16

    Description

      Add logging statements to mongod. These statements will be executed each time mongod performs an action modeled by any of our specs. They will output all internal state that is modeled by any of the TLA+ specs we plan to check against our implementation. For example, each time the server changes state (among primary, secondary, recovering, etc.), it must output the entire oplog, the current term, and the server state.

      These logging statements will be in a new component, disabled by default. The statements must add no overhead when the log component is disabled.

      Attachments

        Activity

          People

            jesse@mongodb.com A. Jesse Jiryu Davis
            jesse@mongodb.com A. Jesse Jiryu Davis
            Votes:
            0 Vote for this issue
            Watchers:
            3 Start watching this issue

            Dates

              Created:
              Updated:
              Resolved: