Documentation/trace/rv/hybrid_automata.rst

Source file repositories/reference/linux-study-clean/Documentation/trace/rv/hybrid_automata.rst

File Facts

System
Linux kernel
Corpus path
Documentation/trace/rv/hybrid_automata.rst
Extension
.rst
Size
12678 bytes
Lines
342
Domain
Support Tooling And Documentation
Bucket
Documentation
Inferred role
Support Tooling And Documentation: documentation
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

struct automaton {
	char *state_names[state_max];                  // X: the set of states
	char *event_names[event_max];                  // E: the finite set of events
	char *env_names[env_max];                      // V: the finite set of env vars
	unsigned char function[state_max][event_max];  // f: transition function
	unsigned char initial_state;                   // x_0: the initial state
	bool final_states[state_max];                  // X_m: the set of marked states
  };

  struct automaton aut = {
	.state_names = {
		"dequeued",
		"enqueued",
		"running",
	},
	.event_names = {
		"dequeue",
		"enqueue",
		"switch_in",
	},
	.env_names = {
		"clk",
	},
	.function = {
		{ INVALID_STATE,      enqueued, INVALID_STATE },
		{ INVALID_STATE, INVALID_STATE,       running },
		{      dequeued, INVALID_STATE, INVALID_STATE },
	},
	.initial_state = dequeued,
	.final_states = { 1, 0, 0 },
  };

  static bool verify_constraint(enum states curr_state, enum events event,
                                enum states next_state)
  {
	bool res = true;

	/* Validate guards as part of f */
	if (curr_state == enqueued && event == switch_in)
		res = get_env(clk) < threshold;
	else if (curr_state == dequeued && event == enqueue)
		reset_env(clk);

	/* Validate invariants in i */
	if (next_state == curr_state || !res)
		return res;
	if (next_state == enqueued)
		ha_start_timer_jiffy(ha_mon, clk, threshold_jiffies);
	else if (curr_state == enqueued)
		res = !ha_cancel_timer(ha_mon);
	return res;
  }

The function ``verify_constraint``, here reported as simplified, checks guards,
performs resets and starts timers to validate invariants according to
specification, those cannot easily be represented in the automaton struct.
Due to the complex nature of environment variables, the user needs to provide
functions to get and reset environment variables that are not common clocks
(e.g. clocks with ns or jiffy granularity).
Since invariants are only defined as clock expirations (e.g. *clk <
threshold*), reaching the expiration of a timer armed when entering the state
is in fact a failure in the model and triggers a reaction. Leaving the state
stops the timer.

It is important to note that timers implemented with hrtimers introduce
overhead, if the monitor has several instances (e.g. all tasks) this can become
an issue. The impact can be decreased using the timer wheel (``HA_TIMER_TYPE``
set to ``HA_TIMER_WHEEL``), this lowers the responsiveness of the timer without
damaging the accuracy of the model, since the invariant condition is checked
before disabling the timer in case the callback is late.

Annotation

Implementation Notes