[SERVER-48226] Improve TLA+ CI Created: 14/May/20  Updated: 29/Oct/23  Resolved: 15/May/20

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

Type: Improvement Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: pull-request
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
Related
is related to SERVER-45416 TLA+ specs are not continuously tested Closed
Backwards Compatibility: Fully Compatible
Participants:

 Description   

Improvements to model-check.sh, the script we use in Evergreen to run the TLA+ model-checker on our formal specifications. From PR description:

"-workers auto" introduced in https://github.com/tlaplus/tlaplus/commit/4111431a169b96d0b2eb850fd6fb4416cf5af4ff

OffHeapDiskFPSet: https://lemmster.de/talks/MSc_MarkusAKuppe_1497363471.pdf

Data that is shared as part of exec stats:
https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/util/ExecutionStatisticsCollector.md



 Comments   
Comment by Githook User [ 14/May/20 ]

Author:

{'name': 'Markus Alexander Kuppe', 'email': 'github.com@lemmster.de', 'username': 'lemmy'}

Message: SERVER-48226 Improve TLA+ CI

"-workers auto" automatically detects available parallelism,
"OffHeapDiskFPSet" uses a concurrency optimised fingerprint set, and
ExecutionStatisticsCollector sends usage stats to exec-stats.tlapl.us

Closes #1361

Signed-off-by: A. Jesse Jiryu Davis <jesse@mongodb.com>
Branch: master
https://github.com/mongodb/mongo/commit/34ca0408f8b2b4ac7b96cfcbe0a8604f4b3fc244

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