This tutorial aims to reproduce all bugs found during the model checking stage. Makefile targets starting with check-
and replay-
are provided to reproduce bugs at the specification and implementation levels (please refer to each Makefile located in the systems directories for more details).
For detailed descriptions and analysis of the bugs, please refer to Bugs-Descriptions.pdf (in Chinese) or its translated English version.
Link: bakwc/PySyncObj#166
To reproduce:
make check_pysyncobj_non_monotonic_commit_idx_bug
make replay_pysyncobj_non_monotonic_commit_idx_bug
Link: bakwc/PySyncObj#167
To reproduce:
make check_pysyncobj_next_idx_no_greater_than_match_idx_bug
make replay_pysyncobj_next_idx_no_greater_than_match_idx_bug
Link: bakwc/PySyncObj#167
To reproduce:
make check_pysyncobj_non_monotonic_match_idx_bug
make replay_pysyncobj_non_monotonic_match_idx_bug
Link: bakwc/PySyncObj#169
To reproduce:
make check_pysyncobj_leader_commits_older_terms_bug
make replay_pysyncobj_leader_commits_older_terms_bug
Link: willemt/raft#118
To reproduce:
make check_wraft_incorrect_appending_entries_bug
make replay_wraft_incorrect_appending_entries_bug
To reproduce:
make check_wraft_inconsistent_committed_log_bug
make replay_wraft_inconsistent_committed_log_bug
To reproduce:
make check_wraft_non_monotonic_current_term_bug
make replay_wraft_non_monotonic_current_term_bug
To reproduce:
make check_wraft_retry_empty_logs_bug
make replay_wraft_retry_empty_logs_bug
To reproduce:
make check_wraft_next_idx_no_greater_than_match_idx_bug
make replay_wraft_next_idx_no_greater_than_match_idx_bug
Link: daos-stack/raft#70
To reproduce:
make check_daosraft_leader_votes_for_others_bug
make replay_daosraft_leader_votes_for_others_bug
Link: zhebrak/raftos#25
To reproduce:
make check_raftos_non_monotonic_match_idx_bug
make replay_raftos_non_monotonic_match_idx_bug
Link: zhebrak/raftos#26
To reproduce:
make check_raftos_incorrect_erasing_entries_bug
make replay_raftos_incorrect_erasing_entries_bug
Link: zhebrak/raftos#30
To reproduce:
make check_raftos_commitment_not_advanced_bug
make replay_raftos_commitment_not_advanced_bug
Note: sleeps are used between actions. Although the bugs can be reproduced on our computer, sleep times may not be sufficient on other machines.
Link: xnnyygn/xraft#33
To reproduce:
make check_xraft_election_safety_bug
make replay_xraft_election_safety_bug
It will display information about the bug (two leaders within the same term):
build/mount/systems/Xraft-series/bugs/election_safety/test/log.1:2022-06-04 05:36:58.200 [node] INFO node.NodeImpl - become leader, term 2
build/mount/systems/Xraft-series/bugs/election_safety/test/log.3:2022-06-04 05:36:54.100 [node] INFO node.NodeImpl - become leader, term 2
Link: xnnyygn/xraft#40
To reproduce:
make check_xraft_kv_linearizability_bug
make replay_xraft_kv_linearizability_bug
It will display information about the bug (client reads stale value):
[DETL] Shell cmd finished: "/root/sandtable/systems/Xraft-series/bugs/linearizability/kv-store/cli.sh n2 put v1", result: (EOF)
[DETL] Shell cmd finished: "/root/sandtable/systems/Xraft-series/bugs/linearizability/kv-store/cli.sh n1 get", result: null
Note: sleeps are used between actions. Although the bugs can be reproduced on our computer, sleep times may not be sufficient on other machines.
Link: https://issues.apache.org/jira/browse/ZOOKEEPER-1419
To reproduce:
make check_zookeeper_vote_circle_bug
make replay_zookeeper_vote_circle_bug
It will display information about the bug (the last 3 updating proposals form a vote circle):
2022-06-04 13:36:50,000 [myid:1] - DEBUG [QuorumPeer[myid=1]/0.0.0.0:2180:FastLeaderElection@631] - Updating proposal: 1 (newleader), 0x0 (newzxid), -1 (oldleader), 0xffffffffffffffff (oldzxid)
2022-06-04 13:36:50,002 [myid:1] - DEBUG [QuorumPeer[myid=1]/0.0.0.0:2180:FastLeaderElection@631] - Updating proposal: 2 (newleader), 0x0 (newzxid), 1 (oldleader), 0x0 (oldzxid)
2022-06-04 13:36:50,002 [myid:1] - DEBUG [QuorumPeer[myid=1]/0.0.0.0:2180:FastLeaderElection@631] - Updating proposal: 3 (newleader), 0x0 (newzxid), 2 (oldleader), 0x0 (oldzxid)
2022-06-04 13:36:50,007 [myid:1] - DEBUG [QuorumPeer[myid=1]/0.0.0.0:2180:FastLeaderElection@631] - Updating proposal: 2 (newleader), 0x0 (newzxid), 3 (oldleader), 0x0 (oldzxid)
2022-06-04 13:36:50,007 [myid:1] - DEBUG [QuorumPeer[myid=1]/0.0.0.0:2180:FastLeaderElection@631] - Updating proposal: 3 (newleader), 0x0 (newzxid), 2 (oldleader), 0x0 (oldzxid)