-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathSafetySynchronization.p
More file actions
95 lines (89 loc) · 4.72 KB
/
SafetySynchronization.p
File metadata and controls
95 lines (89 loc) · 4.72 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
spec SafetySynchronization observes eClientPutRequest, eClientGetRequest, eRaftGetResponse, eRaftPutResponse, eBecomeLeader {
var localKVStore: KVStore;
var requestResultMap: map[Client, map[int, Result]];
var getRequestMap: map[Client, map[TransId, KeyT]];
var putRequestMap: map[Client, map[TransId, (key: KeyT, value: ValueT)]];
var seenId: map[Client, set[int]];
var respondedId : map[Client, set[int]];
var currentLeader: Server;
var term: TermId;
start state Init {
entry {
localKVStore = newStore();
requestResultMap = default(map[Client, map[int, Result]]);
getRequestMap = default(map[Client, map[TransId, KeyT]]);
putRequestMap = default(map[Client, map[TransId, (key: KeyT, value: ValueT)]]);
seenId = default(map[Client, set[int]]);
respondedId = default(map[Client, set[int]]);
currentLeader = null as Server;
term = -1;
goto Listening;
}
}
state Listening {
on eBecomeLeader do (payload: tBecomeLeader) {
if (payload.term > term) {
currentLeader = payload.leader;
term = payload.term;
}
}
on eClientGetRequest do (payload: tClientGetRequest) {
if (!(payload.client in keys(seenId))) {
seenId[payload.client] = default(set[int]);
}
if (!(payload.client in keys(respondedId))) {
respondedId[payload.client] = default(set[int]);
}
if (!(payload.client in keys(getRequestMap))) {
getRequestMap[payload.client] = default(map[TransId, KeyT]);
}
if (payload.client == payload.sender && !(payload.transId in seenId[payload.client])) {
seenId[payload.client] += (payload.transId);
}
getRequestMap[payload.client][payload.transId] = payload.key;
}
on eClientPutRequest do (payload: tClientPutRequest) {
if (!(payload.client in keys(seenId))) {
seenId[payload.client] = default(set[int]);
}
if (!(payload.client in keys(respondedId))) {
respondedId[payload.client] = default(set[int]);
}
if (!(payload.client in keys(putRequestMap))) {
putRequestMap[payload.client] = default(map[TransId, (key: KeyT, value: ValueT)]);
}
if (payload.client == payload.sender && !(payload.transId in seenId[payload.client])) {
seenId[payload.client] += (payload.transId);
}
putRequestMap[payload.client][payload.transId] = (key=payload.key, value=payload.value);
}
on eRaftGetResponse do (payload: tRaftGetResponse) {
var execResult: ExecutionResult;
checkResponseValid(payload.client, payload.sender, payload.transId);
if (!(payload.client in keys(respondedId)) && currentLeader == payload.sender) {
respondedId[payload.client] += (payload.transId);
execResult = executeGet(localKVStore, getRequestMap[payload.client][payload.transId]);
assert execResult.result.success == payload.success, format("Inconsistent status: {0}", getRequestMap[payload.client][payload.transId]);
assert execResult.result.value == payload.value, format("Inconsistent Get result! Expected {0}, got {1}", execResult.result.value, payload.value);
}
}
on eRaftPutResponse do (payload: tRaftPutResponse) {
var execResult: ExecutionResult;
checkResponseValid(payload.client, payload.sender, payload.transId);
if (!(payload.client in keys(respondedId)) && currentLeader == payload.sender) {
respondedId[payload.client] += (payload.transId);
assert payload.client in keys(putRequestMap);
execResult = executePut(localKVStore, putRequestMap[payload.client][payload.transId].key, putRequestMap[payload.client][payload.transId].value);
localKVStore = execResult.newState;
// assert execResult.result.value == payload.value, format("Inconsistent Get result! Expected {0}, got {1}", execResult.result.value, payload.value);
}
}
}
fun checkResponseValid(client: Client, sender: Server, tId: TransId) {
assert currentLeader != null, "Leader is null but got an eRaftResponse!";
if (currentLeader == sender) {
assert client in keys(seenId), format("Responding to a client that has not sent any request: {0}", client);
assert tId in seenId[client], format("Responding to a non-existing transactionId {0} sent by {1}", tId, client);
}
}
}