Modality Basics

In this document we will tour the CLI using the example system to get familiar with Modality.

The example system we use in this guide is included in the Modality downloads. Check the appropriate section of the Installation guide for your install method to see where the example system source code is installed.

# Getting an Overview of Your System

First, we'll look at the SUT definition data to get an idea of what our system under test looks like. We'll start by checking the list of SUTs that Modality knows about and selecting the example one as the default.

$ modality sut list
NAME         TAGS                           COMPONENTS  SESSIONS
example-sut  [consumer, monitor, producer]  4           1

$ modality sut use example-sut

Here we see that the example SUT has 4 components (including the modality internal component), and that one session has been collected for it.

# Components

Core Concept: Components

Components are logical groupings of functionality that you define when you run the manifest generation tool, usually as part of your build. Typically each component is a sub-tree of your source code.

Now, let's look at the components in this SUT.

$ modality sut component list
NAME                TAGS  PROBES  EVENTS
consumer-component  []    1       5
monitor-component   []    1       8
producer-component  []    1       5

This shows us that the example SUT has 3 components that we have defined, each with a single probe and a handful of defined events. You may remember that the SUT has 4 total components—that includes the component that modality uses to track its internal data.

# Probes

Core Concept: Probes

Probes are important machinery for Modality instrumentation—you need a handle to a probe anywhere you'd like to record an event, and recorded events get stored in the probe's buffer until they're collected in a report and sent to Modality's backend daemon.

Many Modality commands have verbosity flags (-v, -vv, etc...) to control the output. Here we'll use one to see additional useful information when listing the probes in the SUT.

$ modality sut probe list
NAME      TAGS
CONSUMER  [c-example, consumer]
MONITOR   [c-example, monitor]
PRODUCER  [c-example, producer]

$ modality sut probe list -v
NAME      TAGS                   COMPONENT           SOURCE
CONSUMER  [c-example, consumer]  consumer-component  c-example/src/consumer/main.c#L66
MONITOR   [c-example, monitor]   monitor-component   c-example/src/monitor/main.c#L65
PRODUCER  [c-example, producer]  producer-component  c-example/src/producer/main.c#L67

As expected, we see one probe per component, along with each probe's tags and the location in source where it is initialized.

# Events

Core Concept: Events

Events are the unit of data that Modality collects from your system. Events indicate that something happened, and can additionally carry a user-defined payload to record interesting values or a failure indicator that Modality's analysis tools automatically take into account.

Next let's do the same for events. We'll look at events in the SUT with verbose output so we can see some additional metadata along with the place the event is defined in source.

$ modality sut event list -vv
NAME                 TAGS                                    KIND         SEVERITY  SOURCE
CONSUMER_REGISTERED  [heartbeat, monitor]                    event                  c-example/src/monitor/main.c#L189
CONSUMER_TIMEOUT     [heartbeat, monitor, timeout]           failure      10        c-example/src/monitor/main.c#L228
DEINIT               [producer]                              event                  c-example/src/producer/main.c#L94
DEINIT               [consumer]                              event                  c-example/src/consumer/main.c#L93
DEINIT               [monitor]                               event                  c-example/src/monitor/main.c#L96
HEARTBEAT_ID_CHECK   [heartbeat, monitor]                    expectation  10        c-example/src/monitor/main.c#L159
INIT                 [producer]                              event                  c-example/src/producer/main.c#L80
INIT                 [consumer]                              event                  c-example/src/consumer/main.c#L79
INIT                 [monitor]                               event                  c-example/src/monitor/main.c#L78
PRODUCER_REGISTERED  [heartbeat, monitor]                    event                  c-example/src/monitor/main.c#L174
PRODUCER_TIMEOUT     [heartbeat, monitor, timeout]           failure      10        c-example/src/monitor/main.c#L212
RECVD_MSG            [communication, consumer, measurement]  event                  c-example/src/consumer/main.c#L176
RECVD_MSG            [communication, heartbeat, monitor]     event                  c-example/src/monitor/main.c#L150
SAMPLED              [measurement, producer, sample]         event                  c-example/src/producer/main.c#L131
SENT_HEARTBEAT       [communication, heartbeat, producer]    event                  c-example/src/producer/main.c#L194
SENT_HEARTBEAT       [communication, consumer, heartbeat]    event                  c-example/src/consumer/main.c#L198
SENT_MEASUREMENT     [communication, measurement, producer]  event                  c-example/src/producer/main.c#L167
TASK_LOOP            [consumer, process-loop]                event                  c-example/src/consumer/main.c#L128

This gives us a list of every event defined in our SUT, i.e. every event that Modality is aware of associated with this SUT. As we'll see below, each session of data collection has its own stats on which events were actually observed (and how often) during that session.

Core Concept: Metadata

Tags are arbitrary strings that you can use to add semantic meaning to your instrumentation. You can later use tags as filters when querying a collected trace. Tags can be added to SUTs, components, probes, all types of events, mutators, and objectives. Tags, severity, and description are all metadata for use in the CLI—they compile away and will never be included in your binary.

Most of the commands we've looked at also have an inspect subcommand to get more detailed information. Let's first look at the SAMPLED event in the PRODUCER component to see an example of a basic event with a payload.

$ modality sut event inspect SAMPLED
Name: SAMPLED
Description: Producer sampled raw measurement
ID: 3
Type Hint: I8
Kind: event
Component: producer-component
Source: c-example/src/producer/main.c#L131
Tags: [measurement, producer, sample]

This shows us several interesting things. We see the event's ID, which was automatically generated by the manifest and header generation tools and mapped to the name we gave it, SAMPLED. We also see the various metadata we've provided for it, and where it's defined in source. Lastly, since this is an event with a payload, we are shown a hint of the type that this event expects for its payload.

# Expectations

Core Concept: Expectations

Expectations are a special type of event with a conditional failure expression. If, when the expectation is recorded, the expression is true, the expectation passes. When expectations fail they are highlighted in CLI output, and failing expectations also drive some of Modality's automated analysis features.

Next we'll go back to the list and look at HEARTBEAT_ID_CHECK to see an example of an expectation.

$ modality sut event list -v
NAME                 TAGS                                    KIND         SEVERITY
...
HEARTBEAT_ID_CHECK   [heartbeat, monitor]                    expectation  10
...

The KIND column helpfully points out that this is an expectation. Its name and tags work the same as for a regular event. In addition, SEVERITY is a piece of metadata which can be added to expectations and failures to indicate how serious they are on a scale from 1 to 10.

TIP

You may have noticed that there are also failure events. These are equivalent to an expectation whose condition is simply false. Besides making it convenient to record events which always represent a failure, failure events can also have implications on more advanced use cases like generative testing.

# Mutators

Thus far, we have looked at all the different Modality concepts that allow you to collect data about what your system is doing. The missing piece for taking testing and verification to the next level is a way to change the behavior of the SUT in controlled ways. This enables you to test specific hypotheses or explore the space of system states looking for problems before they arise.

Core Concept: Mutators

Mutators are pieces of instrumentation that give Modality an entry point to modify the behavior of the system. Basic mutators do things like alter the value of a specific variable or introduce a delay at a given point. You can also write your own mutator implementation to allow Modality to manipulate your system however you choose.

Let's list the mutators defined in this SUT and then take a closer look at one.

$ modality sut mutator list
NAME                 TAGS
sample-data-mutator  [sample]

$ modality sut mutator inspect sample-data-mutator
Name: sample-data-mutator
ID Hash: 931521712542889512
Source: src/producer/main.c#L141
Tags: [sample]
Probes:
  PRODUCER
Parameters:
  Name: sample
    Type: i8
    Minimum Effect Value: 0
    Nominal: [-50..50]
    Safety: [-120..120]
    Hard: [-128..127]

This SUT only has a single mutator defined. The source line shows us where this mutator is in code—if a mutation is injected for this mutator it will take effect when execution passes through this line. Since this is a data mutator, i.e. a mutator which alters the value of a variable, we also see information about this mutator's parameters. Data mutators have nominal, safety, and hard ranges so you can define the space of possible mutation values that Modality can explore in different scenarios.

Generative Testing

You can use mutators to manually introduce mutations, picking the mutation value yourself or having Modality choose. To drastically reduce the time required to do exploratory testing of your system, Modality's generative testing can automatically create large numbers of test cases of system behavior.

Now that we've gotten familiar with the example SUT let's take a look at interacting with a session.

# Digging in to Collected Data

Everything we looked at above was static, definitional data about our System Under Test. Now we'll look at the example session that comes pre-loaded in the Modality database when you install.

Core Concept: Sessions

A session represents a single continuous run of data collection from your SUT.

First, we'll list the sessions Modality knows about and select the example one as default for the rest of our commands.

$ modality session list
NAME             SUT          STATUS
example-session  example-sut  CLOSED

$ modality session use example-session

Since we just installed we see only the example session. It is closed, meaning that data collection is not ongoing.

Now, let's look at the lists of probes and events that we observed during this session.

$ modality session probe list
NAME      TAGS                   EVENTS
CONSUMER  [c-example, consumer]  13858
MONITOR   [c-example, monitor]   842
PRODUCER  [c-example, producer]  4079

$ modality session event list
NAME                 TAGS                                    COUNT
CONSUMER_REGISTERED  [heartbeat, monitor]                    17
CONSUMER_TIMEOUT     [heartbeat, monitor, timeout]           26
DEINIT               [consumer]                              17
DEINIT               [monitor]                               17
DEINIT               [producer]                              17
HEARTBEAT_ID_CHECK   [heartbeat, monitor]                    374
INIT                 [producer]                              17
INIT                 [consumer]                              17
INIT                 [monitor]                               17
PRODUCER_REGISTERED  [heartbeat, monitor]                    17
RECVD_MSG            [communication, consumer, measurement]  806
RECVD_MSG            [communication, heartbeat, monitor]     374
SAMPLED              [measurement, producer, sample]         2821
SENT_HEARTBEAT       [communication, consumer, heartbeat]    185
SENT_HEARTBEAT       [communication, heartbeat, producer]    204
SENT_MEASUREMENT     [communication, measurement, producer]  1020
TASK_LOOP            [consumer, process-loop]                12833

Here we see the events that are defined in the SUT, along with how many times each event was observed. The events column in the probe list shows the total number of observed events from each probe.

# Viewing the Trace

To get a better sense of our collected data we'll use the log command to actually see what the trace looks like.

TIP

The output of modality log is generally quite large. An easy way to get started exploring the trace is to pipe the output to less, i.e. modality log | less -r.

Here we see a snippet of log output from after the system has initialized. This sample system has 3 components. The producer takes measurements and periodically sends them to the consumer on a socket. The consumer receives measurement messages and does some work (represented by the TASK_LOOP event). The monitor listens for heartbeats from both the consumer and producer to make sure they stay online.

$ modality log
...
      *  (956819952:1:0:4, HEARTBEAT_ID_CHECK @ MONITOR, outcome=PASS)
          description="Monitor heartbeat sender ID check"
      
  »    PRODUCER interacted with CONSUMER
      
    *    (444045962:2:1:3, RECVD_MSG @ CONSUMER, payload=2)
          description="Consumer received measurement message"
      
      *  (956819952:1:0:5, CONSUMER_REGISTERED @ MONITOR)
          description="Monitor has observed the consumer"
      
  *      (101425052:1:0:1, SENT_HEARTBEAT @ PRODUCER, payload=1)
          description="Producer sent heartbeat message"
      
    *    (444045962:2:1:4, TASK_LOOP @ CONSUMER)
          description="Consumer expensive task loop iteration"
      
    *    (444045962:2:2:3, TASK_LOOP @ CONSUMER)
          description="Consumer expensive task loop iteration"
      
  ════»  PRODUCER interacted with MONITOR
      
    *    (444045962:2:2:4, TASK_LOOP @ CONSUMER)
          description="Consumer expensive task loop iteration"
...

A few things to note about log output:

  • The left side is an ASCII art representation of the trace graph. Each colored vertical line represents a probe, i.e. a thread of execution or a separate device in your system.
  • Asterisks represent individual events. Information about that event is printed alongside, in the color corresponding to the probe the event is on.
  • Communication between threads or devices is shown with horizontal lines in the graph representation. Use snapshots to tell Modality about communication between threads or devices.

Let's look at the first event in the output above and break down the different things Modality is telling us.

(956819952:1:0:4, HEARTBEAT_ID_CHECK @ MONITOR, outcome=PASS)
  description="Monitor heartbeat sender ID check"
  • 956819952:1:0:4 are coordinates. An event can occur many times in a session, so coordinates allow you to pinpoint a specific instance of an event in a session.
  • HEARTBEAT_ID_CHECK @ MONITOR is the event and probe name. We use the shorthand @ notation to say that this is an occurrence of the HEARTBEAT_ID_CHECK event which has been recorded to the MONITOR probe.
  • outcome=PASS tells us that this is an expectation and that this instance passed. For regular events with payloads the payload value will be shown here—see the RECVD_MSG @ CONSUMER event in the log output above.

# Querying the Trace

Log gives you a visual representation of the trace, but this can sometimes be difficult to pull meaning from on its own. The SpeQTr Language gives you a powerful way to ask questions of your collected traces.

First we'll look at the simplest possible query—getting all occurrences of a specific event:

$ modality query HEARTBEAT_ID_CHECK@MONITOR
Result 1:
═════════
HEARTBEAT_ID_CHECK@MONITOR(956819952:1:0:4, HEARTBEAT_ID_CHECK @ MONITOR, outcome=PASS)
  description="Monitor heartbeat sender ID check"

Result 2:
═════════
HEARTBEAT_ID_CHECK@MONITOR(956819952:2:1:5, HEARTBEAT_ID_CHECK @ MONITOR, outcome=PASS)
  description="Monitor heartbeat sender ID check"
...

Here we look for all occurrences of the HEARTBEAT_ID_CHECK event recorded to the MONITOR probe.

Core Concept: SpeQTr Language

The SpeQTr Language is a powerful tool for finding patterns and checking conditions in a trace. You can look for combinations of events, filter on numerous event properties, and check that your system always behaves as specified. The reference has much more information on writing queries and specifications.

# Checking System Behavior

Next, let's use the check command to see if the system's behavior is always within specification. The CONSUMER and PRODUCER components should be sending heartbeats at least every 600ms, so we'll write a specification to check that behavior.

# heartbeat-specification.txt
NEVER
    # 2 == HEARTBEAT_ID_CONSUMER
    RECVD_MSG @ MONITOR (_.payload = 2) 
    -> AFTER 600ms
    RECVD_MSG @ MONITOR (_.payload = 2)

In this system our instrumentation includes the ID of the component whose heartbeat has been received as the payload of the RECVD_MSG event. Thus, we say that we should never see a heartbeat for the consumer (i.e. a heartbeat with payload 2) followed by another consumer heartbeat after 600ms. In other words, each consumer heartbeat should have another consumer heartbeat after it within 600ms.

Core Concept: check

The check command checks a specification against a region of recorded execution. It returns false if there is at least one instance in the trace where the specification is violated.

Let's see if our system is performing correctly. Here we provide a specification in a file, and since we don't specify a region the specification will be checked against the entire default session.

$ modality check --file heartbeat-specification.txt
false

While it's useful to know that the consumer failed to send a heartbeat in time at least once, this still leaves a lot of investigative work to do. Since specifications can be quite complex it's not always obvious what could be causing one to fail. To speed up your investigations, modality check includes verbosity flags to include several pieces of helpful output.

$ modality check -vv --file failing-measurement-query.tq 
The given check had no matches. Analyzing why…

Violation: Exists
    NEVER
        RECVD_MSG @ MONITOR(_.payload = 2)
        -> AFTER 600ms
        ^^^^^^^^^^^^^^
        |
        Changing this limit to 3182ms causes this assertion to pass
        RECVD_MSG @ MONITOR(_.payload = 2)
    
    Counter-Example:
        *  RECVD_MSG@MONITOR(393359338:65560:23:6, RECVD_MSG@MONITOR, payload=2)
          
        :  (5 elided events)
          
        *  RECVD_MSG@MONITOR(393359338:131073:0:6, RECVD_MSG@MONITOR, payload=2)
    
    Counter-Query:
        RECVD_MSG @ MONITOR(_.payload = 2)
        -> AFTER 600ms
        RECVD_MSG @ MONITOR(_.payload = 2)

This output tells us that the maximum amount of time between heartbeats was over 3100ms. It also shows a specific spot in the trace where this occurred, which we could investigate in more detail using the --from and --radius options of modality log. Lastly, it gives us a query to find every spot in the trace where this specification is violated.

At this point you've looked at many of Modality's main concepts. Check out the other sections of the documentation to continue learning more.