This is a generic mechanism for verifying correctness of latching rules for state transitions and querying for state of a system.
More...
template<typename Node, size_t LATCHES_COUNT>
class ut::Stateful_latching_rules< Node, LATCHES_COUNT >
This is a generic mechanism for verifying correctness of latching rules for state transitions and querying for state of a system.
It was created for io_fix field of buf_page_t, but can be configured via template instantiation for other usages as long as they fit into the following model:
- The object can be in one of fixed possible states. In case of io_fix, these states were io_fix values, but in general the state can be a tuple of several important, perhaps abstract, properties of the object, for example it could be a std::pair<io_fix, is_in_page_hash>. As long you can pass the list of possible states to constructor, you're good to go.
- There is a fixed set of latches which are relevant to protecting the state. In case of io_fix there were 3: each page has a latch, and its buffer pool has a latch, and there is also a more abstract property of "being the thread which
is responsible for IO operation for this page", which is fine, as long as you can quickly determine which of the three the current thread has, and you can prove that no two threads can hold a given "latch" at the same time (which is trivial for regular mutexes, but puts a burden of proof on you in case of abstract concepts like "IO responsibility")
- For each pair of states you can specify what latches a thread must hold to perform it. For example a thread can change io_fix from BUF_IO_NONE to BUF_IO_WRITE only while holding latches #0, #1 and #2. But the rule could be more complex, for example "you either must hold 1 and 2, or just 0" - as long as you can express it as an alternative of conjunctions (without negation) it's OK.
In other words, we model the situation as a graph, with states as nodes, and edges being possible transitions, where each edge is labeled with a subset of latches (and there might be zero or more edges between any pair of states).
For example: +—+ +—+ +—+ | a | —{0,2}--> | b | <–{2}--> | c | | | <—{0,2}– | | —{2}--> | | | | <—{1}-— | | | | +—+ +—+ +—+
If we know that current state MUST be 'a' or 'c', and want to determine which of the two it is, then it is sufficient to hold just latch #2, because edges going out of 'a' and edges going out of 'c' all require latch #2. OTOH if we don't know what the current state is, but want to determine if the state belongs to the set {b,c}, then it is sufficient to hold just latches #0 and #1, because there are only three edges going in or out of {b,c}, namely a-{0,2}->b, a<-{0,2}-b, a<-{1}-b, and each of them requires #0 or #1. I hope this example shows that verifying correctness case by case like that is possible to do manually, but seems error prone, subject to code rot, and would benefit from automation.
You specify the type of nodes and number of latches by template instatiation, and shape of the graph in the constructor.
This class then can then offer you two things:
- If you call on_transition(from, to, owned_latches) it will verify for you that such transition is allowed as at least one of the edges requires a subset of owned_latches. This way you can verify that the model you described matches reality. For example we call it from buf_page_set_io_fix(page,state).
- If you call assert_latches_let_distinguish(owned_latches,A,B) where A and B are two disjoint sets of states, it will tell you if the current thread holds enough latches to make it possible to determine if state belongs to A or to B in a meaningful way - that is the answer to such question can not change while being asked, because each edge going out from A and out from B has at least one of the owned_latches. For example if a thread knows that io_fix is BUF_IO_READ or BUF_IO_WRITE but is unsure which one of them it is, it might check io_fix state, but only if it has latches which prevent a change from BUF_IO_READ to BUF_IO_PIN or BUF_IO_NONE or BUF_IO_WRITE, and from BUF_IO_WRITE to BUF_IO_PIN or BUF_IO_NONE or BUF_IO_READ
- otherwise the answer could change during query. Note that this might be a smaller set of latches than needed to prevent any activity at all. For example we don't care about changes from BUF_IO_PIN to BUF_IO_FIX. Also, in this example A and B are both singletons, but the mechanism works for arbitrarily large sets.
1.9.2