-
Notifications
You must be signed in to change notification settings - Fork 26
/
Copy pathStorage.tla
179 lines (156 loc) · 8.05 KB
/
Storage.tla
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
------------------------------ MODULE Storage ------------------------------
EXTENDS Integers, FiniteSets, TLC
CONSTANTS
MaxNewMeta, \* maximum generation of newMeta to limit the state space
MetaDataContent \* content that is written to the metadata file
VARIABLES
metadata, \* metaData[i] = MetaDataContent if metadata of generation i is present
manifest, \* manifest[j] is generation of metadata j-th manifest is referencing
newMeta, \* generation of newly created metadata file
newManifest, \* generation of newly created manifest file
state, \* current state, describes what to do next
possibleStates \* set of generations of metadata that limits what can be read from disk
--------------------------------------------------------------------------
(*************************************************************************)
(* First we define some helper functions to work with files abstraction. *)
(* Files is a function from file generation to some content. *)
(*************************************************************************)
(*************************************************************************)
(* CurrentGeneration returns the maximum file generation. If there are *)
(* no files then -1 is returned. *)
(*************************************************************************)
CurrentGeneration(files) ==
IF DOMAIN files = {}
THEN -1
ELSE
CHOOSE gen \in DOMAIN files :
\A otherGen \in DOMAIN files : gen \geq otherGen
(*************************************************************************)
(* DeleteFile removes file with generation delGen. *)
(*************************************************************************)
DeleteFile(files, delGen) == [gen \in DOMAIN files \ {delGen} |-> files[gen]]
(*************************************************************************)
(* DeleteFilesExcept removes all files except keepGen. *)
(*************************************************************************)
DeleteFilesExcept(files, keepGen) == (keepGen :> files[keepGen])
(*************************************************************************)
(* WriteFile creates new file with specified generation and content. *)
(*************************************************************************)
WriteFile(files, gen, content) == (gen :> content) @@ files
--------------------------------------------------------------------------
(*************************************************************************)
(* Now we define functions to emulate write and cleanup of the metadata. *)
(*************************************************************************)
WriteMetaOk(gen) ==
/\ metadata' = WriteFile(metadata, gen, MetaDataContent)
/\ state' = "writeManifest"
WriteMetaFail(gen) ==
/\ metadata' = metadata
/\ state' = "writeMeta"
WriteMetaDirty(gen) ==
/\ \/ metadata' = WriteFile(metadata, gen, MetaDataContent)
\/ metadata' = metadata
/\ state' = "deleteNewMeta"
DeleteNewMeta ==
/\ \/ metadata' = DeleteFile(metadata, newMeta)
\/ metadata' = metadata
/\ state' = "writeMeta"
/\ UNCHANGED <<newMeta, newManifest, manifest, possibleStates>>
DeleteOldMeta ==
/\ \/ metadata' = DeleteFilesExcept(metadata, newMeta)
\/ metadata' = metadata
/\ state' = "writeMeta"
/\ UNCHANGED <<newMeta, newManifest, manifest, possibleStates>>
WriteMeta ==
LET gen == CurrentGeneration(metadata) + 1 IN
/\ newMeta' = gen
/\ \/ WriteMetaOk(gen)
\/ WriteMetaFail(gen)
\/ WriteMetaDirty(gen)
/\ UNCHANGED <<newManifest, manifest, possibleStates>>
--------------------------------------------------------------------------
(*************************************************************************)
(* Now we define functions to emulate write and cleanup of the manifest *)
(* file. *)
(*************************************************************************)
WriteManifestOk(gen) ==
/\ manifest' = WriteFile(manifest, gen, newMeta)
/\ state' = "deleteOldManifest"
/\ possibleStates' = {newMeta}
WriteManifestFail(gen) ==
/\ manifest' = manifest
/\ state' = "deleteNewMeta"
/\ possibleStates' = possibleStates
WriteManifestDirty(gen) ==
/\ \/ manifest' = WriteFile(manifest, gen, newMeta)
\/ manifest' = manifest
/\ state' = "deleteNewManifest"
/\ possibleStates' = possibleStates \union {newMeta}
WriteManifest ==
LET gen == CurrentGeneration(manifest) + 1 IN
/\ newManifest' = gen
/\ \/ WriteManifestOk(gen)
\/ WriteManifestFail(gen)
\/ WriteManifestDirty(gen)
/\ UNCHANGED <<newMeta, metadata>>
DeleteOldManifest ==
/\ \/ manifest' = DeleteFilesExcept(manifest, newManifest)
\/ manifest' = manifest
/\ state' = "deleteOldMeta"
/\ UNCHANGED <<newMeta, newManifest, metadata, possibleStates>>
--------------------------------------------------------------------------
(*************************************************************************)
(* Below are 3 versions of the same function, that is called when *)
(* manifest write was dirty. The buggy one was initially implemented and *)
(* was caught by https://github.com/elastic/elasticsearch/issues/39077. *)
(* Pick one and use in Next function. *)
(* https://github.com/elastic/elasticsearch/pull/40519 implements *)
(* DeleteNewManifestEasy. *)
(*************************************************************************)
DeleteNewManifestBuggy ==
/\ \/ manifest' = DeleteFile(manifest, newManifest)
\/ manifest' = manifest
/\ state' = "deleteNewMeta"
/\ UNCHANGED <<newMeta, newManifest, metadata, possibleStates>>
DeleteNewManifestEasy ==
/\ \/ manifest' = DeleteFile(manifest, newManifest)
\/ manifest' = manifest
/\ state' = "writeMeta"
/\ UNCHANGED <<newMeta, newManifest, possibleStates, metadata>>
DeleteNewManifestHard ==
/\ \/ /\ manifest' = DeleteFile(manifest, newManifest)
/\ state' = "deleteNewMeta"
\/ /\ manifest' = manifest
/\ state' = "writeMeta"
/\ UNCHANGED <<newMeta, newManifest, metadata, possibleStates>>
--------------------------------------------------------------------------
(*************************************************************************)
(* We can define Init and Next functions now. *)
(*************************************************************************)
Init ==
/\ metadata = <<>>
/\ manifest = <<>>
/\ newMeta = -1 \* no latest metadata file
/\ newManifest = -1 \* no latest manifest file
/\ state = "writeMeta" \* we start with writing metadata file
/\ possibleStates = {} \* no metadata can be read from disk
Next ==
\/ (state = "writeMeta" /\ WriteMeta)
\/ (state = "writeManifest" /\ WriteManifest)
\/ (state = "deleteOldManifest" /\ DeleteOldManifest)
\/ (state = "deleteOldMeta" /\ DeleteOldMeta)
\/ (state = "deleteNewManifest" /\ DeleteNewManifestEasy) \* try DeleteNewManifestBuggy and DeleteNewManifestHard
\/ (state = "deleteNewMeta" /\ DeleteNewMeta)
--------------------------------------------------------------------------
(*************************************************************************)
(* Our model has 2 invariants. *)
(*************************************************************************)
MetadataFileReferencedByManifestExists ==
CurrentGeneration(manifest) /= -1
=>
manifest[CurrentGeneration(manifest)] \in DOMAIN metadata
MetadataReferencedByManifestIsValid ==
CurrentGeneration(manifest) /= -1
=>
\E meta \in possibleStates : meta = manifest[CurrentGeneration(manifest)]
============