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

Design synchronous trace logging for TLA+ Trace Checker

    XMLWordPrintableJSON

Details

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

    Description

      When multiple mongods on one machine log events with different timestamps, do we really know in what order they executed these logging statements? If not, can we create a logging mode (enabled only in certain test suites) that provides this guarantee?

      Besides ensuring that all mongods use the same clock, also consider logging higher-precision timestamps.

      Note: there is also the problem of multiple mongods logging events with the same timestamp. We guess that if the timestamp is high-precision and the clock is shared among mongods, that events with the same timestamp can fairly be considered "concurrent". If several events have the same timestamp, then run the trace checker on the execution traces resulting from each possible ordering of the apparently simultaneous events, per Jard & Bochmann 1983 "An approach to testing specifications".

      Attachments

        Activity

          People

            judah.schvimer@mongodb.com Judah Schvimer
            jesse@mongodb.com A. Jesse Jiryu Davis
            Votes:
            0 Vote for this issue
            Watchers:
            4 Start watching this issue

            Dates

              Created:
              Updated:
              Resolved: