[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: |
|
||||||||||||
| 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: |
| Comments |
| Comment by Githook User [ 14/May/20 ] |
|
Author: {'name': 'Markus Alexander Kuppe', 'email': 'github.com@lemmster.de', 'username': 'lemmy'}Message: "-workers auto" automatically detects available parallelism, Closes #1361 Signed-off-by: A. Jesse Jiryu Davis <jesse@mongodb.com> |