[SERVER-43589] Add logging to be used by TLA+ trace checker for RaftMongo.tla Created: 24/Sep/19 Updated: 29/Oct/23 Resolved: 11/Dec/19 |
|
| Status: | Closed |
| Project: | Core Server |
| Component/s: | Replication |
| Affects Version/s: | None |
| Fix Version/s: | 4.3.3 |
| Type: | New Feature | Priority: | Major - P3 |
| Reporter: | A. Jesse Jiryu Davis | Assignee: | A. Jesse Jiryu Davis |
| 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, Repl 2019-12-02, Repl 2019-12-16 |
| Participants: |
| 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. |
| Comments |
| Comment by Githook User [ 29/Jan/20 ] |
|
Author: {'username': 'ajdavis', 'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com'}Message: This is a combination of 6 commits. Revert " This reverts commit 88aaa47b815507e3ddd9a3a79f00d0eaca3ae071. Revert " This reverts commit e57438bd024d04f82dcbcbe68fe223b3f3aec838. Revert " This reverts commit f515d2ad5494e64c3be80189e7ea6bceaf267421. Revert " This reverts commit 744200de5f5667334457ee35abfa3747e2e26d55. Revert " This reverts commit eda99cf7ca668908e5eb0498845b0270265c44e7. Revert " This reverts commit a60ce00707f0ffdb5d2ec5c3a72993cc2b2d2978. delete mode 100644 jstests/replsets/tla_plus_trace_checking.js |
| Comment by A. Jesse Jiryu Davis [ 11/Dec/19 ] |
|
Nevermind, the difficulty of writing such a test is too great. When we test logging code in a JSTest we read log lines from the RAMLog, which are truncated at 1024 chars. TLA+ Trace Logging easily exceeds that limit, so we'd need new infrastructure to test it. |
| Comment by A. Jesse Jiryu Davis [ 10/Dec/19 ] |
|
Before closing, write a test that checks that oplog visibility rules are obeyed on the primary when logging ClientWrite actions. |
| Comment by Githook User [ 10/Dec/19 ] |
|
Author: {'email': 'jesse@mongodb.com', 'name': 'A. Jesse Jiryu Davis', 'username': 'ajdavis'}Message: |
| Comment by Githook User [ 07/Nov/19 ] |
|
Author: {'name': 'A. Jesse Jiryu Davis', 'username': 'ajdavis', 'email': 'jesse@mongodb.com'}Message: |