Introduction

The Auxon Specification and Query Trace Language (SpeQTr) is a powerful tool for interacting with your collected data.

# Two Use Cases in One

The SpeQTr language has two 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.

# 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 (opens new window) 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.

For more details about writing specifications see the syntax reference. For examples of common specifications see the cookbook.

# 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.

Query features:

  • Match by event and timeline name/ID, or use wildcards.
  • Filter matches with a variety of operators on any event or timeline attribute.
  • Describe causal relationships between events, i.e. "event1 FOLLOWED BY event2".
  • Calculate aggregate statistics 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 producer timeline, communication from the producer to the consumer establishing a causal link, and then the event on the consumer timeline.
  • Matched events are shown with the label they were assigned as the query.label attribute, e.g. first and second.
  • 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.

For more details about writing queries see the syntax reference. For examples of common queries see the cookbook.

# 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)

Syntax →