SpeQTr Language Overview

The Modality Specification, Query, and Trigger (SpeQTr) Language is a powerful tool for interacting with your collected trace 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. Modality 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 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 Modality should wait for before injecting a mutation.

# What's in a Trace?

In Modality, a system trace consists of a collection of related events. These events are logged using the modality-probe library, and collected from many probes into a session. The session data is stored by Modality, which can evaluate specifications and queries over it.

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. Instead, Modality uses the snapshot data passed between modality-probe instances to establish before-and-after relationships between events on different probes. 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 for a session 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.

# What's a Specification?

Modality specifications give you a way to use that graph to check things about your system. The modality check command evaluates specifications over specific regions of observed behavior, and specifications are said to pass if the system conforms to the specification. When appropriate, modality check can call out counterexamples to your specification or help you narrow down which parts of a non-passing specification are not fulfilled by the system. Specifications are also used in objectives as measurements to be taken for each run of generative testing.

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:

FOR EACH radar_on@control AS radar_on
  VERIFY radar_on -> WITHIN 250 ms radar_reading@radar(0.2 <= _.payload <= 0.8)

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 command takes a query expression 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:

  • Specify event and probe names, or use wildcards.
  • Filter matches with a variety of operators on a large number of event fields.
  • Describe causal relationships between events, i.e. "event1 FOLLOWED BY event2"

# Basic Query Example

Here is an example of a query:

*@PRODUCER AS first -> *@CONSUMER AS second AND first.payload = second.payload

In English, you might describe this as:

Plain english description:

Match pairs of events where an event on the PRODUCER probe is followed by an event on the CONSUMER probe with the same payload.

Running the above query gives the following results:

$ modality query '*@PRODUCER AS first -> *@CONSUMER AS second AND first.payload = second.payload'
Result 1:
═════════
*  │  first(636316639:0:0:6, SENT_MEASUREMENT @ PRODUCER, payload=0)
│    description="Producer sent measurement message"
»╗  
│  *  second(945766127:2:1:3, RECVD_MSG @ CONSUMER, payload=0)
│    description="Consumer received measurement message"

Result 2:
═════════
*  │  first(636316639:4:2:6, SENT_MEASUREMENT @ PRODUCER, payload=2)
│    description="Producer sent measurement message"
»╗  
│  *  second(945766127:4:5:3, RECVD_MSG @ CONSUMER, payload=2)
│    description="Consumer received measurement message"
...

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 probe, communication from the PRODUCER to the CONSUMER establishing a causal link, and then the event on the CONSUMER probe.
  • Matched events are shown with the label they were assigned, e.g. first and second.
  • Event information is shown in the parentheses:
    • 636316639:0:0:6 are the first event's coordinates—a sequence of colon-separated numbers which constitute a unique ID for a specific occurrence of an event.
    • SENT_MEASUREMENT @ PRODUCER shows the event's name, SENT_MEASUREMENT, and the probe name, PRODUCER.
    • payload=0 shows the payload value. For expectations the pass/fail outcome is shown here.
  • The event description is shown below.

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

# 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, 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:

INIT@MONITOR

This is more or less the simplest possible trigger, saying that no mutations should be injected until Modality sees the INIT event on the MONITOR probe.

For more details about writing triggers see the syntax reference.