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.
Core Concept: Components
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.
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 (
-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.
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.
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 ...
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.
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.
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.
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.
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:4are 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 @ MONITORis the event and probe name. We use the shorthand
@notation to say that this is an occurrence of the
HEARTBEAT_ID_CHECKevent which has been recorded to the
outcome=PASStells 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 @ CONSUMERevent 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
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
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
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
--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.