[SERVER-44076] Design synchronous trace logging for TLA+ Trace Checker Created: 17/Oct/19  Updated: 29/Oct/23  Resolved: 14/Nov/19

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.3.2

Type: New Feature Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: Judah Schvimer
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Backwards Compatibility: Fully Compatible
Sprint: Repl 2019-11-04, Repl 2019-11-18
Participants:

 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".



 Comments   
Comment by Githook User [ 29/Jan/20 ]

Author:

{'username': 'ajdavis', 'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com'}

Message: SERVER-45558 Revert logging additions for TLA+ Trace Checker project

This is a combination of 6 commits.

Revert "SERVER-44458 Add RaftMongo.tla spec"

This reverts commit 88aaa47b815507e3ddd9a3a79f00d0eaca3ae071.

Revert "SERVER-45184 Ban TLA+ tracing with inMemory"

This reverts commit e57438bd024d04f82dcbcbe68fe223b3f3aec838.

Revert "SERVER-43589 Trace logging for RaftMongo.tla"

This reverts commit f515d2ad5494e64c3be80189e7ea6bceaf267421.

Revert "SERVER-44076 create TLA+ Trace Checking logging framework"

This reverts commit 744200de5f5667334457ee35abfa3747e2e26d55.

Revert "SERVER-43589 Failpoint to log TLA+ trace events"

This reverts commit eda99cf7ca668908e5eb0498845b0270265c44e7.

Revert "SERVER-45106 Add TLA+ log component to logv2"

This reverts commit a60ce00707f0ffdb5d2ec5c3a72993cc2b2d2978.

delete mode 100644 jstests/replsets/tla_plus_trace_checking.js
delete mode 100644 src/mongo/db/repl/replication_coordinator_impl_tla_plus_trace.cpp
delete mode 100644 src/mongo/db/repl/tla_plus_trace_repl.idl
delete mode 100644 src/mongo/util/tla_plus_trace.cpp
delete mode 100644 src/mongo/util/tla_plus_trace.h
delete mode 100644 src/mongo/util/tla_plus_trace.idl
Branch: master
https://github.com/mongodb/mongo/commit/bcae9e6777408882b3d391721dea262c1cdcd16e

Comment by A. Jesse Jiryu Davis [ 03/Dec/19 ]

I vote we don't support Windows on Evergreen for now. I think testing multiple platforms won't be likely to reveal the spec transcription errors we're looking for.

Comment by Judah Schvimer [ 02/Dec/19 ]

Do we need trace logging to work on Windows, or can we "comment" that away as unsupported?

Comment by Mark Benvenuto [ 02/Dec/19 ]

On Windows, it depends on the operating system. On Windows 8+, we rely on the OS to get high quality timestamps. On Windows 2008R2, we estimate a high quality timestamp. But in general, it can go backwards when synced with NTP. For more details, see the Windows docs on the scary details.

Comment by A. Jesse Jiryu Davis [ 29/Nov/19 ]

mark.benvenuto, we have a question for you, originally from suganthi.mani in a related code review forĀ SERVER-43589. Here's the question: Have you observed clocks going backwards on our Windows builders in Evergreen?

We're trying to implement log messages with distinct timestamps in the simplest manner possible, only for certain tests in Evergreen. We've written this:

void logTlaPlusTraceEvent(const TlaPlusTraceEvent& event) {
    Date_t beforeTime = Date_t::now();
    Date_t afterTime = Date_t::now();
    while (afterTime == beforeTime) {
        sleepmillis(1);
        afterTime = Date_t::now();
    }    invariant(afterTime > beforeTime, "Clock went backwards");
    log() << event.toBSON().jsonString();
} 

Comment by Githook User [ 14/Nov/19 ]

Author:

{'username': 'judahschvimer', 'email': 'judah.schvimer@10gen.com', 'name': 'Judah Schvimer'}

Message: SERVER-44076 create TLA+ Trace Checking logging framework
Branch: master
https://github.com/mongodb/mongo/commit/744200de5f5667334457ee35abfa3747e2e26d55

Comment by A. Jesse Jiryu Davis [ 04/Nov/19 ]

Terrific. We'll be careful when reviewing the logging statements I add in SERVER-43589 to ensure they finish logging about an event before the event is visible to another thread or process.

Generated at Thu Feb 08 05:04:56 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.