MySQL 8.0.29
Source Code Documentation
ut::Stateful_latching_rules< Node, LATCHES_COUNT > Class Template Reference

This is a generic mechanism for verifying correctness of latching rules for state transitions and quering for state of a system. More...

#include <ut0stateful_latching_rules.h>

Classes

struct  edge_t
 The type for a possible transition from one state to another while holding at least a given set of latches. More...
 

Public Types

using node_t = Node
 The type for a state in our automata. More...
 
using nodes_set_t = std::set< node_t >
 The type for a set of states. More...
 
using latches_set_t = std::bitset< LATCHES_COUNT >
 The type for a set of latches - there are LATCHES_COUNT distinct latches, each one corresponds to a fixed position in a bitset. More...
 

Public Member Functions

 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. More...
 
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 question if current state belongs to set A as opposed to set B. More...
 
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. More...
 
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. More...
 

Private Member Functions

template<typename T >
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 (such as our ib::logger). More...
 
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. More...
 
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. More...
 
bool can_leave (const latches_set_t &forbiden_latches, const nodes_set_t &source) const
 A convenience function for the special case of. More...
 

Private Attributes

const nodes_set_t m_states
 The set of all possible states. More...
 
const std::vector< edge_tm_edges
 The list of allowed state transitions. More...
 

Detailed Description

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 quering 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:

  1. 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.
  2. 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")
  3. 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 sates 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:

  1. 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).
  2. 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.

Member Typedef Documentation

◆ latches_set_t

template<typename Node , size_t LATCHES_COUNT>
using ut::Stateful_latching_rules< Node, LATCHES_COUNT >::latches_set_t = std::bitset<LATCHES_COUNT>

The type for a set of latches - there are LATCHES_COUNT distinct latches, each one corresponds to a fixed position in a bitset.

The mapping is up to the user of this class - just be consistent.

◆ node_t

template<typename Node , size_t LATCHES_COUNT>
using ut::Stateful_latching_rules< Node, LATCHES_COUNT >::node_t = Node

The type for a state in our automata.

◆ nodes_set_t

template<typename Node , size_t LATCHES_COUNT>
using ut::Stateful_latching_rules< Node, LATCHES_COUNT >::nodes_set_t = std::set<node_t>

The type for a set of states.

Constructor & Destructor Documentation

◆ Stateful_latching_rules()

template<typename Node , size_t LATCHES_COUNT>
ut::Stateful_latching_rules< Node, LATCHES_COUNT >::Stateful_latching_rules ( nodes_set_t  all_states,
std::vector< edge_t allowed_transitions 
)
inline

Creates a set of rules for allowed_transitions between all_states.

Parameters
[in]all_statesThe set of all possible states of the system
[in]allowed_transitionsThe set of allowed transitions. There might be multiple edges between the same pare of states which is interpreted as an alternative: {{x, {0,2}, y}, {x, {1}, y}} would mean, that a thread which holds just latch #2 can't transition from x to y, but a thread which holds #0 and #2 can, and so does a thread which holds just #1 or #0 and #1 or #1 and #2 or all three or even more.

Member Function Documentation

◆ assert_latches_let_distinguish() [1/2]

template<typename Node , size_t LATCHES_COUNT>
void ut::Stateful_latching_rules< Node, LATCHES_COUNT >::assert_latches_let_distinguish ( const latches_set_t owned_latches,
const nodes_set_t A 
) const
inline

A convenience function for the special case of.

See also
assert_latches_let_distinguish(owned_latches, A, complement(A)). In other words, it checks if the current thread's owned_latches prevent state transitions to and from the set A.
Parameters
[in]owned_latchesThe latches the current thread owns
[in]AThe set of latches

◆ assert_latches_let_distinguish() [2/2]

template<typename Node , size_t LATCHES_COUNT>
void ut::Stateful_latching_rules< Node, LATCHES_COUNT >::assert_latches_let_distinguish ( const latches_set_t owned_latches,
const nodes_set_t A,
const nodes_set_t B 
) const
inline

Checks if owned_latches (presumably held by the current thread) are enough to meaningfully ask a question if current state belongs to set A as opposed to set B.

In other words it checks if owned_latches prevent other threads from performing state transition from the inside of set A outside, and from the inside of set B outside. Otherwise it prints debug information as fatal error.

Parameters
[in]owned_latchesThe latches the current thread owns
[in]AThe first set of latches
[in]BThe second set of latches

◆ can_leave()

template<typename Node , size_t LATCHES_COUNT>
bool ut::Stateful_latching_rules< Node, LATCHES_COUNT >::can_leave ( const latches_set_t forbiden_latches,
const nodes_set_t source 
) const
inlineprivate

A convenience function for the special case of.

See also
is_transition_possible(forbiden_latches, A,B) where B=complement(A). In other words, it checks if another thread can cause the state to leave the given set of states even though we hold a set of forbiden_latches.
Parameters
[in]forbiden_latchesThe set of latches which the hypothetical transitioning thread can't hold (because we are holding them).
[in]sourceThe set of source states
Returns
true iff there is at least one edge from a state inside source to a state outside of source labeled with a set of latches disjoint with forbiden_latches.

◆ complement()

template<typename Node , size_t LATCHES_COUNT>
nodes_set_t ut::Stateful_latching_rules< Node, LATCHES_COUNT >::complement ( const nodes_set_t states) const
inlineprivate

Computes the complement of the given set of states, that is a set of all of the other states.

Parameters
[in]statesThe set of states
Returns
the complement of the set of states

◆ is_transition_possible()

template<typename Node , size_t LATCHES_COUNT>
bool ut::Stateful_latching_rules< Node, LATCHES_COUNT >::is_transition_possible ( const latches_set_t forbiden_latches,
const nodes_set_t source,
const nodes_set_t destination 
) const
inlineprivate

Checks if another thread could change the state even though we hold some latches.

In other words, checks if the rules allow a thread which ISN'T holding any of the forbiden_latches to transition from at least one state inside source to at least one state inside destination, where source and destination are sets of states. It prints an error if transition is possible.

Parameters
[in]forbiden_latchesThe set of latches which the hypothetical transitioning thread can't hold (because we are holding them).
[in]sourceThe set of source states
[in]destinationThe set of destination states
Returns
true iff there is at least one edge from a state inside source to a state inside destination labeled with a set of latches disjoint with forbiden_latches.

◆ on_transition()

template<typename Node , size_t LATCHES_COUNT>
void ut::Stateful_latching_rules< Node, LATCHES_COUNT >::on_transition ( const node_t from,
const node_t to,
const latches_set_t owned_latches 
) const
inline

Checks if the transition between given states holding specified latches is allowed by the rules.

In other words it checks if there is at least one edge between from and to nodes labeled with a subset of ownwed_latches. It prints a debug information as fatal error if rules are violated.

◆ print()

template<typename Node , size_t LATCHES_COUNT>
template<typename T >
void ut::Stateful_latching_rules< Node, LATCHES_COUNT >::print ( T &  sout,
const latches_set_t latches 
) const
inlineprivate

A helper function which prints the ids of latches from the set of latches to an ostream-like object (such as our ib::logger).

Parameters
[in]soutthe ostream-like object to print latches to
[in]latchesa set of latches to print to sout @

Member Data Documentation

◆ m_edges

template<typename Node , size_t LATCHES_COUNT>
const std::vector<edge_t> ut::Stateful_latching_rules< Node, LATCHES_COUNT >::m_edges
private

The list of allowed state transitions.

◆ m_states

template<typename Node , size_t LATCHES_COUNT>
const nodes_set_t ut::Stateful_latching_rules< Node, LATCHES_COUNT >::m_states
private

The set of all possible states.

Useful for computing the complement of any given set


The documentation for this class was generated from the following file: