[SERVER-44851] Update TLA+ model of heartbeat safe reconfig Created: 26/Nov/19 Updated: 29/Oct/23 Resolved: 07/Feb/20 |
|
| Status: | Closed |
| Project: | Core Server |
| Component/s: | Replication |
| Affects Version/s: | None |
| Fix Version/s: | 4.3.4 |
| Type: | Task | Priority: | Major - P3 |
| Reporter: | Siyuan Zhou | Assignee: | Siyuan Zhou |
| Resolution: | Fixed | Votes: | 0 |
| Labels: | None | ||
| Remaining Estimate: | Not Specified | ||
| Time Spent: | Not Specified | ||
| Original Estimate: | Not Specified | ||
| Issue Links: |
|
||||||||
| Backwards Compatibility: | Fully Compatible | ||||||||
| Sprint: | Repl 2019-12-16, Repl 2019-12-30, Repl 2020-01-13, Repl 2020-01-27, Repl 2020-02-10 | ||||||||
| Participants: | |||||||||
| Description |
|
We need to update the model to check the final design.
"force" reconfig may also be included in the model, but the correctness is tricky, so it's a stretch goal. |
| Comments |
| Comment by Githook User [ 06/Feb/20 ] |
|
Author: {'username': 'visualzhou', 'name': 'Siyuan Zhou', 'email': 'siyuan.zhou@mongodb.com'}Message: |
| Comment by Siyuan Zhou [ 27/Jan/20 ] |
|
We didn't model arbiters as it's of low risk and low priority. |
| Comment by Githook User [ 23/Jan/20 ] |
|
Author: {'username': 'visualzhou', 'name': 'Siyuan Zhou', 'email': 'siyuan.zhou@mongodb.com'}Message: |