MySQL 8.0.30
Source Code Documentation
ut0stateful_latching_rules.h
Go to the documentation of this file.
1/*****************************************************************************
2
3Copyright (c) 2021, 2022, Oracle and/or its affiliates.
4
5This program is free software; you can redistribute it and/or modify it under
6the terms of the GNU General Public License, version 2.0, as published by the
7Free Software Foundation.
8
9This program is also distributed with certain software (including but not
10limited to OpenSSL) that is licensed under separate terms, as designated in a
11particular file or component or in included license documentation. The authors
12of MySQL hereby grant you an additional permission to link the program and
13your derivative works with the separately licensed software that they have
14included with MySQL.
15
16This program is distributed in the hope that it will be useful, but WITHOUT
17ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
18FOR A PARTICULAR PURPOSE. See the GNU General Public License, version 2.0,
19for more details.
20
21You should have received a copy of the GNU General Public License along with
22this program; if not, write to the Free Software Foundation, Inc.,
2351 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
24
25*****************************************************************************/
26
27/** @file include/ut0stateful_latching_rules.h
28The Stateful_latching_rules class template which can be used to describe
29possible states, latches required to transition between them, and then validate
30if transitions performed by application take required latches, and that queries
31for the state are performed when holding enough latches to prevent state from
32changing. */
33
34#ifndef ut0stateful_latching_rules
35#define ut0stateful_latching_rules
36
37#include <bitset>
38
39namespace ut {
40/** This is a generic mechanism for verifying correctness of latching rules for
41state transitions and quering for state of a system. It was created for io_fix
42field of buf_page_t, but can be configured via template instantiation for other
43usages as long as they fit into the following model:
44
451. The object can be in one of fixed possible states. In case of io_fix, these
46states were io_fix values, but in general the state can be a tuple of several
47important, perhaps abstract, properties of the object, for example it could be
48a std::pair<io_fix, is_in_page_hash>. As long you can pass the list of possible
49states to constructor, you're good to go.
50
512. There is a fixed set of latches which are relevant to protecting the state.
52In case of io_fix there were 3: each page has a latch, and its buffer pool has
53a latch, and there is also a more abstract property of "being the thread which
54is responsible for IO operation for this page", which is fine, as long as you
55can quickly determine which of the three the current thread has, and you can
56prove that no two threads can hold a given "latch" at the same time (which is
57trivial for regular mutexes, but puts a burden of proof on you in case of
58abstract concepts like "IO responsibility")
59
603. For each pair of states you can specify what latches a thread must hold to
61perform it. For example a thread can change io_fix from BUF_IO_NONE to
62BUF_IO_WRITE only while holding latches #0, #1 and #2. But the rule could be
63more complex, for example "you either must hold 1 and 2, or just 0" - as long as
64you can express it as an alternative of conjunctions (without negation) it's OK.
65
66In other words, we model the situation as a graph, with sates as nodes, and
67edges being possible transitions, where each edge is labeled with a subset of
68latches (and there might be zero or more edges between any pair of states).
69
70For example:
71+---+ +---+ +---+
72| a | ---{0,2}--> | b | <--{2}--> | c |
73| | <---{0,2}-- | | ---{2}--> | |
74| | <---{1}---- | | | |
75+---+ +---+ +---+
76
77If we know that current state *MUST* be 'a' or 'c', and want to determine which
78of the two it is, then it is sufficient to hold just latch #2, because edges
79going out of 'a' and edges going out of 'c' all require latch #2.
80OTOH if we don't know what the current state is, but want to determine if the
81state belongs to the set {b,c}, then it is sufficient to hold just latches
82#0 and #1, because there are only three edges going in or out of {b,c}, namely
83a-{0,2}->b, a<-{0,2}-b, a<-{1}-b, and each of them requires #0 or #1.
84I hope this example shows that verifying correctness case by case like that is
85possible to do manually, but seems error prone, subject to code rot, and would
86benefit from automation.
87
88You specify the type of nodes and number of latches by template instatiation,
89and shape of the graph in the constructor.
90
91This class then can then offer you two things:
921. If you call on_transition(from, to, owned_latches) it will verify for you
93that such transition is allowed as at least one of the edges requires a subset
94of owned_latches. This way you can verify that the model you described matches
95reality. For example we call it from buf_page_set_io_fix(page,state).
96
972. If you call assert_latches_let_distinguish(owned_latches,A,B) where A and B
98are two disjoint sets of states, it will tell you if the current thread holds
99enough latches to make it possible to determine if state belongs to A or to B in
100a meaningful way - that is the answer to such question can not change while
101being asked, because each edge going out from A and out from B has at least one
102of the owned_latches.
103For example if a thread knows that io_fix is BUF_IO_READ or BUF_IO_WRITE but is
104unsure which one of them it is, it might check io_fix state, but only if it has
105latches which prevent a change from BUF_IO_READ to BUF_IO_PIN or BUF_IO_NONE or
106BUF_IO_WRITE, and from BUF_IO_WRITE to BUF_IO_PIN or BUF_IO_NONE or BUF_IO_READ
107- otherwise the answer could change during query.
108Note that this might be a smaller set of latches than needed to prevent any
109activity at all. For example we don't care about changes from BUF_IO_PIN to
110BUF_IO_FIX. Also, in this example A and B are both singletons, but the mechanism
111works for arbitrarily large sets. */
112template <typename Node, size_t LATCHES_COUNT>
114 public:
115 /** The type for a state in our automata */
116 using node_t = Node;
117
118 /** The type for a set of states */
119 using nodes_set_t = std::set<node_t>;
120
121 /** The type for a set of latches - there are LATCHES_COUNT distinct
122 latches, each one corresponds to a fixed position in a bitset. The mapping is
123 up to the user of this class - just be consistent. */
124 using latches_set_t = std::bitset<LATCHES_COUNT>;
125
126 /** The type for a possible transition from one state to another while holding
127 at least a given set of latches. */
128 struct edge_t {
129 /** The old state from which the transition starts. */
131
132 /** The required subset of latches for this particular transition. Note that
133 there might be several edges for the same from->to pair, which means that a
134 thread can pick any of them for which it has the required latches. */
136
137 /** The new state from to which the transition leads. */
139
140 /** Creates a description of one of allowed state transitions from given
141 state to another while holding given latches. For example
142 {BUF_IO_READ, {0, 2}, BUF_IO_NONE}
143 says a if a thread holds latches 0 and 2 then it can transition from
144 BUF_IO_READ to BUF_IO_NONE.
145 @param[in] from The old state from which the transition starts
146 @param[in] idxs The list of integers in range <0,LATCHES_COUNT) used to
147 construct set of latches for this edge.
148 @param[in] to The new state from to which the transition leads. */
149 edge_t(node_t from, std::initializer_list<int> &&idxs, node_t to)
150 : m_from(from), m_latches(), m_to(to) {
151 for (auto id : idxs) m_latches[id] = true;
152 }
153 };
154
155 private:
156 /** The set of all possible states. Useful for computing the complement of
157 any given set */
159
160 /** The list of allowed state transitions. */
161 const std::vector<edge_t> m_edges;
162
163 /** A helper function which prints the ids of latches from the set of latches
164 to an ostream-like object (such as our ib::logger).
165 @param[in] sout the ostream-like object to print latches to
166 @param[in] latches a set of latches to print to sout
167 @*/
168 template <typename T>
169 void print(T &sout, const latches_set_t &latches) const {
170 sout << '{';
171 bool first = true;
172 for (size_t i = 0; i < latches.size(); ++i) {
173 if (latches[i]) {
174 if (!first) {
175 sout << ", ";
176 }
177 sout << i;
178 first = false;
179 }
180 }
181 sout << '}';
182 }
183
184 /** Checks if another thread could change the state even though we hold some
185 latches. In other words, checks if the rules allow a thread which ISN'T
186 holding any of the `forbiden_latches` to transition from at least one state
187 inside `source` to at least one state inside `destination`, where `source`
188 and `destination` are sets of states.
189 It prints an error if transition is possible.
190 @param[in] forbiden_latches The set of latches which the hypothetical
191 transitioning thread can't hold (because we are
192 holding them).
193 @param[in] source The set of source states
194 @param[in] destination The set of destination states
195 @return true iff there is at least one edge from a state inside `source` to
196 a state inside `destination` labeled with a set of latches disjoint with
197 `forbiden_latches`. */
198 bool is_transition_possible(const latches_set_t &forbiden_latches,
199 const nodes_set_t &source,
200 const nodes_set_t &destination) const {
201 for (const edge_t &edge : m_edges) {
202 if (source.count(edge.m_from) && destination.count(edge.m_to) &&
203 (edge.m_latches & forbiden_latches) == 0) {
204 {
205 ib::error the_err{};
206 the_err << "It is possible to transition from " << edge.m_from
207 << " to " << edge.m_to << " holding just ";
208 print(the_err, edge.m_latches);
209 the_err << " even when we hold ";
210 print(the_err, forbiden_latches);
211 }
212
213 return true;
214 }
215 }
216 return false;
217 }
218
219 /** Computes the complement of the given set of states, that is a set of all
220 of the other states.
221 @param[in] states The set of states
222 @return the complement of the set of states */
223 nodes_set_t complement(const nodes_set_t &states) const {
224 nodes_set_t other_states;
225 std::set_difference(m_states.begin(), m_states.end(), states.begin(),
226 states.end(),
227 std::inserter(other_states, other_states.end()));
228 return other_states;
229 }
230
231 /** A convenience function for the special case of
232 @see is_transition_possible(forbiden_latches, A,B) where B=complement(A).
233 In other words, it checks if another thread can cause the state to leave the
234 given set of states even though we hold a set of `forbiden_latches`.
235 @param[in] forbiden_latches The set of latches which the hypothetical
236 transitioning thread can't hold (because we are
237 holding them).
238 @param[in] source The set of source states
239 @return true iff there is at least one edge from a state inside `source` to
240 a state outside of `source` labeled with a set of latches disjoint with
241 `forbiden_latches`.*/
242 bool can_leave(const latches_set_t &forbiden_latches,
243 const nodes_set_t &source) const {
244 return is_transition_possible(forbiden_latches, source, complement(source));
245 }
246
247 public:
248 /** Creates a set of rules for `allowed_transitions` between `all_states`.
249 @param[in] all_states The set of all possible states of the system
250 @param[in] allowed_transitions The set of allowed transitions. There might be
251 multiple edges between the same pare of states
252 which is interpreted as an alternative:
253 {{x, {0,2}, y}, {x, {1}, y}} would mean, that
254 a thread which holds just latch #2 can't
255 transition from x to y, but a thread which
256 holds #0 and #2 can, and so does a thread
257 which holds just #1 or #0 and #1 or #1 and #2
258 or all three or even more. */
260 std::vector<edge_t> allowed_transitions)
261 : m_states(std::move(all_states)),
262 m_edges(std::move(allowed_transitions)) {}
263
264 /** Checks if `owned_latches` (presumably held by the current thread) are
265 enough to meaningfully ask a question if current state belongs to set A as
266 opposed to set B. In other words it checks if `owned_latches` prevent other
267 threads from performing state transition from the inside of set A outside,
268 and from the inside of set B outside. Otherwise it prints debug information
269 as fatal error.
270 @param[in] owned_latches The latches the current thread owns
271 @param[in] A The first set of latches
272 @param[in] B The second set of latches */
274 const nodes_set_t &A,
275 const nodes_set_t &B) const {
276 const bool can_leave_A = can_leave(owned_latches, A);
277 const bool can_leave_B = can_leave(owned_latches, B);
278
279 if (can_leave_A || can_leave_B) {
281 the_err << "We can leave "
282 << (can_leave_A && can_leave_B ? "both A and B"
283 : (can_leave_A ? "A" : "B"))
284 << " as we only hold: ";
285 print(the_err, owned_latches);
286 }
287 }
288
289 /** A convenience function for the special case of
290 @see assert_latches_let_distinguish(owned_latches, A, complement(A)).
291 In other words, it checks if the current thread's owned_latches prevent state
292 transitions to and from the set A.
293 @param[in] owned_latches The latches the current thread owns
294 @param[in] A The set of latches*/
296 const nodes_set_t &A) const {
297 assert_latches_let_distinguish(owned_latches, A, complement(A));
298 }
299
300 /** Checks if the transition between given states holding specified latches is
301 allowed by the rules. In other words it checks if there is at least one edge
302 between `from` and `to` nodes labeled with a subset of `ownwed_latches`.
303 It prints a debug information as fatal error if rules are violated. */
304 void on_transition(const node_t &from, const node_t &to,
305 const latches_set_t &owned_latches) const {
306 if (from == to) {
307 return;
308 }
309 const auto missing_latches = ~owned_latches;
310
311 if (std::any_of(std::begin(m_edges), std::end(m_edges), [&](auto edge) {
312 return (edge.m_from == from && edge.m_to == to) &&
313 (edge.m_latches & missing_latches) == 0;
314 })) {
315 return;
316 }
318 the_err << "Disallowed transition FROM " << from << " TO " << to
319 << " WITH ";
320 print(the_err, owned_latches);
321 }
322};
323} // namespace ut
324#endif /* ut0stateful_latching_rules */
The class error is used to emit error messages.
Definition: ut0log.h:229
The class fatal is used to emit an error message and stop the server by crashing it.
Definition: ut0log.h:251
This is a generic mechanism for verifying correctness of latching rules for state transitions and que...
Definition: ut0stateful_latching_rules.h:113
const nodes_set_t m_states
The set of all possible states.
Definition: ut0stateful_latching_rules.h:158
const std::vector< edge_t > m_edges
The list of allowed state transitions.
Definition: ut0stateful_latching_rules.h:161
std::bitset< LATCHES_COUNT > latches_set_t
The type for a set of latches - there are LATCHES_COUNT distinct latches, each one corresponds to a f...
Definition: ut0stateful_latching_rules.h:124
bool is_transition_possible(const latches_set_t &forbiden_latches, const nodes_set_t &source, const nodes_set_t &destination) const
Checks if another thread could change the state even though we hold some latches.
Definition: ut0stateful_latching_rules.h:198
void assert_latches_let_distinguish(const latches_set_t &owned_latches, const nodes_set_t &A, const nodes_set_t &B) const
Checks if owned_latches (presumably held by the current thread) are enough to meaningfully ask a ques...
Definition: ut0stateful_latching_rules.h:273
Stateful_latching_rules(nodes_set_t all_states, std::vector< edge_t > allowed_transitions)
Creates a set of rules for allowed_transitions between all_states.
Definition: ut0stateful_latching_rules.h:259
nodes_set_t complement(const nodes_set_t &states) const
Computes the complement of the given set of states, that is a set of all of the other states.
Definition: ut0stateful_latching_rules.h:223
Node node_t
The type for a state in our automata.
Definition: ut0stateful_latching_rules.h:116
std::set< node_t > nodes_set_t
The type for a set of states.
Definition: ut0stateful_latching_rules.h:119
void assert_latches_let_distinguish(const latches_set_t &owned_latches, const nodes_set_t &A) const
A convenience function for the special case of.
Definition: ut0stateful_latching_rules.h:295
void on_transition(const node_t &from, const node_t &to, const latches_set_t &owned_latches) const
Checks if the transition between given states holding specified latches is allowed by the rules.
Definition: ut0stateful_latching_rules.h:304
void print(T &sout, const latches_set_t &latches) const
A helper function which prints the ids of latches from the set of latches to an ostream-like object (...
Definition: ut0stateful_latching_rules.h:169
bool can_leave(const latches_set_t &forbiden_latches, const nodes_set_t &source) const
A convenience function for the special case of.
Definition: ut0stateful_latching_rules.h:242
Cursor end()
A past-the-end Cursor.
Definition: rules_table_service.cc:191
Definition: varlen_sort.h:183
This file contains a set of libraries providing overloads for regular dynamic allocation routines whi...
Definition: aligned_alloc.h:47
repeated Source source
Definition: replication_asynchronous_connection_failover.proto:41
The type for a possible transition from one state to another while holding at least a given set of la...
Definition: ut0stateful_latching_rules.h:128
node_t m_to
The new state from to which the transition leads.
Definition: ut0stateful_latching_rules.h:138
edge_t(node_t from, std::initializer_list< int > &&idxs, node_t to)
Creates a description of one of allowed state transitions from given state to another while holding g...
Definition: ut0stateful_latching_rules.h:149
node_t m_from
The old state from which the transition starts.
Definition: ut0stateful_latching_rules.h:130
latches_set_t m_latches
The required subset of latches for this particular transition.
Definition: ut0stateful_latching_rules.h:135
#define UT_LOCATION_HERE
Definition: ut0core.h:46
unsigned long id[MAX_DEAD]
Definition: xcom_base.cc:506