The Modality Specification, Query, and Trigger (SpeQTr) Language is a powerful tool for interacting with your collected data.
# Three Use Cases in One
As the name suggests, the SpeQTr language has three main use cases.
Specifications let you describe the expected behavior of a system composed of multiple interacting components. You can specify both local behavior and interactions which span multiple components. Auxon Conform can then check your specifications over any region of recorded history, telling you whether your system behaves as expected and, when it doesn't, helping you figure out why.
Queries let you directly interact with system trace data acquired with Auxon Modality. Where specifications evaluate to a boolean result (and further analysis of that result if requested), queries return a list of all portions of the trace which match the given pattern. You can also compute a variety of aggregations over selected parts of the trace.
Triggers are a subset of queries which can be evaluated during live system execution. Triggers are used for mutation preconditions, letting you describe precise patterns Auxon Deviant should wait for before injecting a mutation.
# What's in a Trace?
In Modality (opens new window), a system trace consists of a collection of timelines. Each timeline is simply a list of events in order. Timelines represent some unit of sequential execution as defined by your system; a timeline could be a thread in a desktop application, a microprocessor in an embedded system, or a single drone in a fleet, to name a few examples. Trace data is stored in Modality, which can evaluate queries over it. Conform (opens new window) uses Modality's data but gives you the ability to evaluate specifications, and Deviant lets you go further and inject mutations into your running system.
Causality is central to Modality's tracing system - it's how Modality can tell if one event is before or after another. Unlike from other systems you may be used to, event ordering in Modality is not derived from a common time source (unless you specifically say it should be). Instead, Modality relies on the fact that events on a timeline are ordered, along with the timeline interaction data you report, to establish before-and-after relationships between events on different timelines. This means that event ordering in Modality is partial: given two events, one may be before or after the other, or they may have no known ordering at all (that is, they are logically concurrent).
This causal ordering is the backbone of the SpeQTr Language. Modality stores all the collected trace data in a causal graph, where each node is an event, and each edge represents a causal (happened-before, happened-after) relationship between the events. You can inspect this graph directly using the
modality log command. (opens new window)
# What's a Specification?
Conform specifications give you a way to use Modality's causal graph to check things about your system. The
conform spec eval (opens new window) command evaluates specifications over specific regions of observed behavior, and specifications are said to pass if the system behavior matches the specification. When appropriate, Conform can help you narrow down which parts of a failing specification are being violated and suggest values that could make the specification pass.
You might use a specification to:
- Assert that all values logged at a particular point in your software fall within a certain desired range.
- Assert that all the faults of a certain type are followed by an automatic remediation.
- Assert that some error conditions should never happen.
- Assert that a complex, distributed initialization sequence always occurs as specified.
# Basic Specification Example
Here is an example of a specification:
behavior "Radar initialization" when "The radar turns on" radar_on@control AS radar_on end nominal case "A valid reading is received within 250ms" radar_on FOLLOWED BY WITHIN 250 ms radar_reading@radar(0.2 <= _.payload <= 0.8) end end
In English, you might describe this as:
Plain english description:
Every time the radar turns on, there should be a reading logged within 250 milliseconds, where the payload is between 0.2 and 0.8.
# What's a Query?
Modality queries let you interrogate your collected trace data. The
modality query (opens new window) command takes a query and returns all the places in the trace that match it. This can be an invaluable tool in investigating bugs, showing you where to start looking or telling you how many times a certain pattern occurred. You can also use queries to perform aggregate calculations over matched events.
# Basic Query Example
Here is an example of a query:
*@producer AS first FOLLOWED BY *@consumer AS second AND first.sample = second.sample
In English, you might describe this as:
Plain english description:
Match pairs of events where an event on the producer timeline is followed by an event on the consumer timeline with the same sample value.
Running the above query gives the following results:
$ modality query '*@producer AS first FOLLOWED BY *@consumer AS second AND first.sample = second.sample' No explicit workspace provided. Using the default workspace. Result 1: ═════════ ■ ║ "Producer sampled raw measurement" @ producer [756e7d297d1741f9b84c0d57496b637e:1f3f77] ║ ║ sample=-1 ║ ║ severity=info ║ ║ source.file=tracing-modality/examples/monitored_pipeline.rs ║ ║ source.line=227 ║ ║ source.module=monitored_pipeline::producer ║ ║ timestamp=1660321309645915340ns ║ ║ query.label=first ║ ║ ╚═»╗ producer interacted with consumer at 1e39a67a05534c69b4f80a6a30469cf9:2d8694 ║ ║ ║ ■ "Received measurement message" @ consumer [1e39a67a05534c69b4f80a6a30469cf9:2d8694] ║ ║ interaction.remote_nonce=2218492899038441066 ║ ║ interaction.remote_timeline_id=756e7d29-7d17-41f9-b84c-0d57496b637e ║ ║ interaction.remote_timestamp=1660321309646241197ns ║ ║ sample=-1 ║ ║ severity=info ║ ║ source.file=tracing-modality/examples/monitored_pipeline.rs ║ ║ source.line=309 ║ ║ source.module=monitored_pipeline::consumer ║ ║ timestamp=1660321309647064839ns ║ ║ query.label=second ║ ║ Result 2: ═════════ ■ ║ "Producer sending measurement message" @ producer [756e7d297d1741f9b84c0d57496b637e:261981] ║ ║ destination=consumer ║ ║ nonce=2218492899038441066 ║ ║ sample=-1 ║ ║ severity=info ║ ║ source.file=tracing-modality/examples/monitored_pipeline.rs ║ ║ source.line=251 ║ ║ source.module=monitored_pipeline::producer ║ ║ timestamp=1660321309646416176ns ║ ║ query.label=first ║ ║ ╚═»╗ producer interacted with consumer at 1e39a67a05534c69b4f80a6a30469cf9:2d8694 ║ ║ ║ ■ "Received measurement message" @ consumer [1e39a67a05534c69b4f80a6a30469cf9:2d8694] ║ ║ interaction.remote_nonce=2218492899038441066 ║ ║ interaction.remote_timeline_id=756e7d29-7d17-41f9-b84c-0d57496b637e ║ ║ interaction.remote_timestamp=1660321309646241197ns ║ ║ sample=-1 ║ ║ severity=info ║ ║ source.file=tracing-modality/examples/monitored_pipeline.rs ║ ║ source.line=309 ║ ║ source.module=monitored_pipeline::consumer ║ ║ timestamp=1660321309647064839ns ║ ║ query.label=second ║ ║ ...
Let's briefly explain the output above. Looking at result 1, we see:
- On the left side is an ASCII art depiction of the causal graph. In this case we see the event on the
producertimeline, communication from the
consumerestablishing a causal link, and then the event on the
- Matched events are shown with the label they were assigned as the
- Each matched event displays
<event name> @ <timeline name> [<coordinates>]. Event coordinates constitute a unique ID for a specific occurrence of an event.
- Beneath the event and timeline name we see that event's attributes. This example shows the set of attributes Modality displays for these events by default, but you can control which attributes are printed with command line options.
# What's a Trigger?
Triggers are a subset of queries which can be evaluated live on a running system. They are used for mutation preconditions in Deviant, allowing you to specify exactly when a mutation should occur. Triggers have certain limitations compared to queries—for example, wildcards cannot be used in triggers.
# Basic Trigger Example
Here is an example of a mutation precondition:
This is more or less the simplest possible trigger, saying that no mutations should be injected until Deviant sees the
init event on the
# SpeQTr is made by the team at Auxon
If you'd like to start a discussion or schedule a demo, contact us. (opens new window)