因果时钟与日志投票推演 · 同源完整文件至先作答,再核对
前置:能区分消息发送与接收、读写调用与返回,理解副本和网络分区;Python 3.10+ 仅用于离线时钟与日志推演。教学范围为Lamport1978;Gilbert/Lynch2002与2012回顾;Python 3.10+。核对日期2026-10-17。示例未执行,本轮没有安装依赖、生成协议代码、启动服务或浏览器预览。完整源码和输入文件见下方「同源完整文件」;推演结论只适用于写明的模型。
同源完整文件
以下README含前置、输入、读者自跑步骤、预期结果、失败、恢复与清理;只做静态核对,没有执行。
model.py
python
import json
import sys
def trace(nodes, events):
if not isinstance(nodes, list) or not nodes or len(set(nodes)) != len(nodes):
raise ValueError('unique nodes required')
clocks = {node: [0] * len(nodes) for node in nodes}
messages, output = {}, []
for event in events:
node, op = event['node'], event['op']
clock, index = clocks[node], nodes.index(node)
if op == 'recv':
sent = messages[event['message']]
clock[:] = [max(a, b) for a, b in zip(clock, sent)]
elif op not in ('local', 'send'):
raise ValueError('unknown event')
clock[index] += 1
if op == 'send':
key = event['message']
if key in messages:
raise ValueError('duplicate message id')
messages[key] = clock.copy()
output.append({'node': node, 'op': op, 'clock': clock.copy()})
return output
if __name__ == '__main__':
try:
data = json.load(sys.stdin)
print(json.dumps(trace(data['nodes'], data['events'])))
except (ValueError, TypeError, KeyError) as error:
print(str(error), file=sys.stderr)
sys.exit(2)log_walk.py与具体输入
python
"""Offline message-order walk, not a Raft server. No clocks, IO or RPC."""
import json
import sys
def integer(value, name, minimum=0):
if type(value) is not int or value < minimum:
raise ValueError(name + ' must be an integer >= ' + str(minimum))
return value
def walk(data):
initial = data['nodes']
if not isinstance(initial, dict) or not initial:
raise ValueError('nonempty node mapping required')
nodes = {}
for name, spec in initial.items():
if not isinstance(name, str) or not name:
raise ValueError('nonempty node names required')
term = integer(spec['term'], 'term')
log = []
previous = 0
for entry in spec['log']:
entry_term = integer(entry['term'], 'entry term', 1)
if not previous <= entry_term <= term or type(entry['delta']) is not int:
raise ValueError('ordered terms and integer deltas required')
log.append(dict(term=entry_term, delta=entry['delta']))
previous = entry_term
nodes[name] = dict(term=term, voted_for=None, role='follower', log=log,
commit=0, applied=0, value=0, votes=[], match={})
majority = len(nodes) // 2 + 1
def higher(node, term):
if term > node['term']:
node.update(term=term, voted_for=None, role='follower', votes=[], match={})
def last(node):
return (node['log'][-1]['term'] if node['log'] else 0, len(node['log']))
def apply(node):
while node['applied'] < node['commit']:
node['value'] += node['log'][node['applied']]['delta']
node['applied'] += 1
history = []
for event in data['events']:
op = event['op']
result = {}
if op == 'elect':
name = event['node']
candidate = nodes[name]
candidate.update(term=candidate['term'] + 1, role='candidate',
voted_for=name, votes=[name], match={})
if majority == 1:
candidate.update(role='leader', match={name: len(candidate['log'])})
result = dict(candidate=name, term=candidate['term'])
elif op == 'vote':
name, voter_name = event['candidate'], event['voter']
candidate, voter = nodes[name], nodes[voter_name]
if candidate['role'] != 'candidate' or name == voter_name:
raise ValueError('distinct candidate and voter required')
higher(voter, candidate['term'])
granted = (candidate['term'] == voter['term']
and voter['voted_for'] in (None, name)
and last(candidate) >= last(voter))
if granted:
voter['voted_for'] = name
candidate['votes'] = sorted(set(candidate['votes'] + [voter_name]))
higher(candidate, voter['term'])
if candidate['role'] == 'candidate' and len(candidate['votes']) >= majority:
candidate['role'] = 'leader'
candidate['match'] = {peer: len(candidate['log']) if peer == name else 0
for peer in nodes}
result = dict(granted=granted, candidate_role=candidate['role'])
elif op == 'propose':
name = event['leader']
leader = nodes[name]
if leader['role'] != 'leader' or type(event['delta']) is not int:
raise ValueError('leader and integer delta required')
leader['log'].append(dict(term=leader['term'], delta=event['delta']))
leader['match'][name] = len(leader['log'])
result = dict(index=len(leader['log']), term=leader['term'])
elif op == 'append':
name, peer = event['leader'], event['follower']
leader, follower = nodes[name], nodes[peer]
if name == peer or leader['role'] != 'leader':
raise ValueError('distinct leader and follower required')
prev = integer(event['prev_index'], 'prev_index')
if prev > len(leader['log']):
raise ValueError('leader prefix missing')
prev_term = leader['log'][prev - 1]['term'] if prev else 0
higher(follower, leader['term'])
if leader['term'] == follower['term']:
follower['role'] = 'follower'
accepted = (leader['term'] == follower['term'] and prev <= len(follower['log'])
and (prev == 0 or follower['log'][prev - 1]['term'] == prev_term))
if accepted:
# The exercise sends the entire suffix after prev, not partial batches.
for index in range(prev, len(leader['log'])):
entry = leader['log'][index]
if index < len(follower['log']):
existing = follower['log'][index]
if existing['term'] == entry['term']:
if existing['delta'] != entry['delta']:
raise ValueError('invalid initial history: equal term/index differs')
continue
if index < follower['commit']:
raise ValueError('cannot overwrite committed entry')
del follower['log'][index:]
follower['log'].append(entry.copy())
leader['match'][peer] = max(leader['match'][peer], len(leader['log']))
follower['commit'] = max(follower['commit'], min(leader['commit'], len(leader['log'])))
apply(follower)
higher(leader, follower['term'])
result = dict(accepted=accepted, previous_index=prev)
elif op == 'commit':
leader = nodes[event['leader']]
if leader['role'] != 'leader':
raise ValueError('leader required')
eligible = [index for index in range(leader['commit'] + 1, len(leader['log']) + 1)
if leader['log'][index - 1]['term'] == leader['term']
and sum(match >= index for match in leader['match'].values()) >= majority]
if eligible:
leader['commit'] = max(eligible)
apply(leader)
result = dict(commit=leader['commit'], advanced=bool(eligible))
else:
raise ValueError('unknown operation')
# Serialize every state: later changes must not rewrite earlier snapshots.
history.append(json.loads(json.dumps(dict(event=event, result=result, nodes=nodes))))
return dict(majority=majority, history=history, final=nodes)
if __name__ == '__main__':
try:
print(json.dumps(walk(json.load(sys.stdin))))
except (ValueError, TypeError, KeyError) as error:
print(str(error), file=sys.stderr)
sys.exit(2)json
{
"nodes": {
"A": {"term": 1, "log": [{"term": 1, "delta": 5}]},
"B": {"term": 1, "log": [{"term": 1, "delta": 5}]},
"C": {"term": 1, "log": []}
},
"events": [
{"op": "elect", "node": "A"},
{"op": "vote", "candidate": "A", "voter": "B"},
{"op": "append", "leader": "A", "follower": "B", "prev_index": 1},
{"op": "commit", "leader": "A"},
{"op": "propose", "leader": "A", "delta": 7},
{"op": "append", "leader": "A", "follower": "C", "prev_index": 1},
{"op": "append", "leader": "A", "follower": "C", "prev_index": 0},
{"op": "commit", "leader": "A"},
{"op": "append", "leader": "A", "follower": "C", "prev_index": 2},
{"op": "append", "leader": "A", "follower": "B", "prev_index": 1}
]
}json
{
"nodes": {
"A": {"term": 2, "log": [{"term": 1, "delta": 5}]},
"B": {"term": 2, "log": [{"term": 1, "delta": 5}, {"term": 2, "delta": 7}]},
"C": {"term": 2, "log": [{"term": 1, "delta": 5}, {"term": 2, "delta": 7}]}
},
"events": [
{"op": "elect", "node": "A"},
{"op": "vote", "candidate": "A", "voter": "B"},
{"op": "vote", "candidate": "A", "voter": "C"}
]
}json
{
"nodes": {
"A": {"term": 1, "log": []},
"B": {"term": 1, "log": []},
"C": {"term": 1, "log": []}
},
"events": [
{"op": "elect", "node": "A"},
{"op": "vote", "candidate": "A", "voter": "B"},
{"op": "elect", "node": "C"},
{"op": "propose", "leader": "A", "delta": 7},
{"op": "append", "leader": "A", "follower": "C", "prev_index": 1}
]
}requirements.txt
text
# Python 3.10+ standard library only; no third-party dependency.README.md
md
# 一致性与分布式协作:完整示例
示例未执行。核对日期2026-10-17。教学版本族:Lamport1978;Gilbert/Lynch2002与2012回顾;Python 3.10+。
## 文件与依赖
文件:model.py、log_walk.py、log-input.json、vote-counterexample.json、candidate-stepdown.json、requirements.txt。requirements.txt为同源依赖声明;两个程序都仅用Python3.10+标准库,源码和全部输入文件均在实践正文同源展示。
## 输入与前置
前置:理解本地事件、消息发送/接收及向量逐分量比较。使用 Python 3.10+ 标准库,不需要网络或存储服务。时钟模型输入包含 nodes 与按顺序描述的 events;具体输入和快照见下节。日志投票模型的输入与边界见后文独立章节。
读者将来自跑(本轮未执行):在本目录以Python 3.10+读取input.json,PowerShell示意`Get-Content -Raw input.json | python model.py`;Bash示意`python3 model.py < input.json`。把下面输入手工保存为UTF-8文件,输出按预期逐项比较。无需安装依赖,没有服务或网络调用;程序只读标准输入并写标准输出,不改原文件。失败信息写标准错误且退出2。恢复是修正输入后重读,清理只删除自己创建的input.json与输出文件,勿递归删除工作目录。
## 预期结果、失败与恢复
输入 {"nodes":["A","B"],"events":[{"node":"A","op":"send","message":"m"},{"node":"B","op":"local"},{"node":"B","op":"recv","message":"m"}]};三个快照预期[1,0]、[0,1]、[1,2]。接收未知消息拒绝;重复发送消息ID拒绝。
失败要保留输入和错误,先与正文的不变量及边界核对。没有真实服务或性能验证,不以这些模型输出证明生产可用性。
## 独立练习
在上述历史后让A发生local,B发送reply,再让A接收reply,写出三个快照。
参考答案:A本地从[1,0]到[2,0];B发送从[1,2]到[1,3];A接收先合并[2,3]再递增自身,得到[3,3]。A本地[2,0]与B发送[1,3]并发,接收事件则在两者之后。
## 离线日志与投票推演
示例未执行。理论依据为Ongaro/Ousterhout 2014扩展论文图2及§5.2–5.4,核对日期2026-10-17:[作者原文](https://raft.github.io/raft.pdf)。本例是选举、追加和提交核心规则的顺序推演器,并非Raft服务器;没有时钟、RPC、磁盘、崩溃恢复、动态成员、快照、部分消息批次或线性一致读。假定初始日志来自合法历史,初始commit为0;持久投票与日志是正式协议安全前提,本程序内存变量不能代替它们。
输入nodes映射给出每节点term与日志(每条含term和整数delta)。events显式排列elect、vote、propose、append、commit;append的prev_index选定前缀,程序复制完整后缀,返回accepted及每步全节点状态。发送成功才更新matchIndex;投票不算复制确认。每步快照独立复制,最后final保存每个节点角色、日志、提交索引和已应用累加器,不只返回布尔值。
读者未来从本目录按自己的Python路径运行,以下命令仅为文本,本轮未运行:
```text
PowerShell: Get-Content -Raw log-input.json | python log_walk.py
Bash: python3 log_walk.py < log-input.json
PowerShell: Get-Content -Raw vote-counterexample.json | python log_walk.py
Bash: python3 log_walk.py < vote-counterexample.json
```
log-input.json预期:A在任期2取得两票;向B确认索引1后,虽然旧条目已知在多数上,首次commit仍为0/advanced=false。A追加索引2的任期2条目;C缺索引1,第一次append拒绝;改prev_index=0后C接收两条。第二次commit为2/advanced=true,A应用5+7得到12。最后通知C并补齐B,三节点final均term2、commit2、applied2、value12、相同两条日志;只有A为leader,majority为2。vote-counterexample.json预期两次granted=false,A仍candidate、votes=[A],B/C的任期更新为3但不投给日志较旧的A。
练习:删去向C补前缀的成功append及最后给B追加,保留第二次commit,会发生什么?答案:A的索引2只在自己被确认,B的matchIndex仍1,C仍0;commit不推进且value仍0。再把候选日志比较条件去掉,旧日志A会取得B票而错误当选,说明任期大不能替代日志新旧限制。请只在复制文件中修改,不改作为参照的原输入。无效节点ID或操作、负索引、非法日志次序等退出2;拒绝投票/追加属于合法推演结果,不是程序崩溃。
恢复是修正输入重新推演,没有后台状态需要清理;只删除自己另存的输出文件,不删除原schema/源码或工作目录。没有执行程序,以上为手推预期,未验证故障恢复与完整协议安全。
## 同任期领导消息触发候选退选
candidate-stepdown.json初始A/B/C任期均1、日志均空。A选举升任期2,B投票后A为leader;C尚未获知领导,开始自己的任期2选举,暂为candidate。A追加delta7到索引1,随后向C发prev_index=1的AppendEntries。C的日志为空,前缀不匹配,因此accepted=false;它仍先因同任期合法领导消息退为follower,保留任期2及本任期voted_for=C,日志与提交索引不变。若只在accepted分支退选,C会错误继续竞选。修正规则在任期检查之后、前缀匹配之前执行角色转换。
读者未来可将前述log_walk.py的输入文件改为candidate-stepdown.json,例如Bash文字步骤为`python3 log_walk.py < candidate-stepdown.json`,PowerShell为`Get-Content -Raw candidate-stepdown.json | python log_walk.py`。本轮没有执行。最后一步预期result.accepted=false,final.C.role=follower、term=2、log=[]、commit=0、voted_for=C;退选不等于删除当前任期的投票记录,也不证明收到的新日志已匹配。先作答,再核对
在上述历史后让A发生local,B发送reply,再让A接收reply,写出三个快照。
逐步参考解答
A本地从[1,0]到[2,0];B发送从[1,2]到[1,3];A接收先合并[2,3]再递增自身,得到[3,3]。A本地[2,0]与B发送[1,3]并发,接收事件则在两者之后。
继续阅读
- 历史与因果模型
- 向量时钟推演
- 向量时钟推演