McMini

McMini is an explicit-state model checker, based on DPOR. It analyzes a target that is a multi-threaded executable (binary), and identifies thread schedules that produce deadlock, segfaults, assertion failures, and other errors. (See the McMini paper for technical details of its design.)

Unlike some model checkers, McMini runs directly on a Linux binary. It is as easy to use as:

mcmini ./a.out

Installation

McMini is installed as follows.

git clone https://github.com/mcminickpt/mcmini.git
cd mcmini
./configure
make -j8

If you are debugging, use ./configure --enable-debug, but McMini will then be compiled with -g3 -O0, which implies lower performance.

Quick Start

The formal ‘man page’ for McMini follows in the next subsection. However, this subsection may be all that you need to gain a basic understanding of McMini. If McMini appeals to you, we recommend also looking at the section: Tutorial: Running McMini.

To begin, copy the following program into a file, deadlock.c.

#include <stdio.h>
#include <pthread.h>
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;

void *child_thread(void *dummy) {
  pthread_mutex_lock(&mutex2);
  pthread_mutex_lock(&mutex1);
  printf("child thread: I have both mutexes.  I win!\n");
  pthread_mutex_unlock(&mutex1);
  pthread_mutex_unlock(&mutex2);
  return NULL;
}

int main() {
  pthread_t thread;
  pthread_create(&thread, NULL, child_thread, NULL);
  pthread_mutex_lock(&mutex1);
  pthread_mutex_lock(&mutex2);
  printf("parent thread: I have both mutexes.  I win!\n");
  pthread_mutex_unlock(&mutex2);
  pthread_mutex_unlock(&mutex1);
  pthread_join(thread, NULL);
  printf("*** Done.\n");
  return 0;
}

Now compile it:

gcc deadlock.c -o deadlock -pthread
./deadlock

When we run it, we see:

parent thread: I have both mutexes.  I win!
child thread: I have both mutexes.  I win!
*** Done.

Now let’s test this code with McMini, to see if there’s a bug. We execute:

./mcmini -f -q -m15 ./deadlock

McMini then uncovers the following deadlock:

About to exec into ./deadlock
TraceId 1, *** DEADLOCK DETECTED ***
THREAD BACKTRACE
 1. thread 0: starts
 2. thread 0: pthread_create(thr:1, _, _, _)
 3. thread 0: pthread_mutex_lock(mut:1)
 4. thread 1: starts
 5. thread 1: pthread_mutex_lock(mut:2)
0, 0, 0, 1, 1,
END
THREAD PENDING OPERATIONS
 * thread 0: pthread_mutex_lock(mut:2) [ Blocked ]
   thread 1: pthread_mutex_lock(mut:1) [ Blocked ]
END
***** Model checking completed! *****
*** DEADLOCK DETECTED ***
(Trace number (traceId): 1)
  Number of traces: 2
Total number of transitions: 15
Elapsed time: 0 seconds

Before analyzing this, we introduce some terminology.

Definition: transition

A thread transition (or “transition”, for short) is a thread operation. As seen above, McMini supports pthread_create, pthread_join, starts (thread start), exits (thread exit), operations for mutex, semaphore, condition variables, and others.

Definition: trace

An execution trace (or “trace”, for short) is a particular thread schedule for a single execution of a target program. The target above is for the program a.out (deadlock, in our case). The trace above is for traceId number 1. (The traceId’s begin at traceId 0.)

We see that McMini found a deadlock (sometimes known as a “deadly embrace”). (And McMini can similarly diagnose if some trace causes a segmentation fault or an assertion failure.) Here is a guide to McMini’s report of this deadlock:

• Line 2 (and also line 17): This thread schedule is for traceId 1.

• Line 3: The “THREAD BACKTRACE” (thread schedule) is shown compactly as a single line: one threadId for each transition of a thread.

• Line 9: A more concise summary of the sequence of threads shown from line 3.

• Analysis of the transitions (thread operations) for this trace:

  • Lines 6 and 12: The parent thread acquired mutex 1 (line 6) and waits for mutex 1 (line 12) in its pending operation.

  • Lines 8 and 13: The child thread acquired mutex 2 (line 8) and waits for mutex 1 (line 13) in its pending operation.

  • In summary, Lines 12 and 13 show that both threads are “Blocked”. So, this is true deadlock.

So, why didn’t we see this deadlock when executing ./a.out by itself? It’s because the operating system scheduled the threads according to traceId 0. To verify this, let’s ask McMini to print a more “common” thread schedule. Let’s inspect traceId 0.

USER% ./mcmini -t0 -q -m15 ./deadlock

About to exec into ./deadlock
*** -t or --trace requested.  Printing trace:
THREAD BACKTRACE
 1. thread 0: starts
 2. thread 0: pthread_create(thr:1, _, _, _)
 3. thread 0: pthread_mutex_lock(mut:1)
 4. thread 0: pthread_mutex_lock(mut:2)
 5. thread 0: pthread_mutex_unlock(mut:2)
 6. thread 0: pthread_mutex_unlock(mut:1)
 7. thread 1: starts
 8. thread 1: pthread_mutex_lock(mut:2)
 9. thread 1: pthread_mutex_lock(mut:1)
10. thread 1: pthread_mutex_unlock(mut:1)
11. thread 1: pthread_mutex_unlock(mut:2)
12. thread 1: exits
13. thread 0: pthread_join(thr:1, _)
0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0,
END
THREAD PENDING OPERATIONS
 * thread 0: exits [ Done ]
   thread 1: exits [ Done ]
END
***** Model checking completed! *****
      (NO FAILURE DETECTED)
Number of traces: 1
Total number of transitions: 13
Elapsed time: 0 seconds

This is the end of the quick start. If you want to dig deeper into McMini, it’s time to dig into:

1. The McMini man page: sec-man

2. Next, to analyze a non-trivial multithreaded program, consider the Tutorial: Analyzing a Subtle Bug section.

McMini man page

NAME

mcmini - McMini is a full-featured, in-situ, extensible model checker.

SYNOPSIS

mcmini [-m <num>] [-f] [-q] [-t <traceId|traceSeq>] [-v [-v]] [-h] target_executable

-m <num>, --max-depth-per-thread <num>

Maximum number of transitions executed for any given thread. If a thread reaches this maximum depth of transitions, then no further transitions for this thread will be considered. But transitions by other threads can continue to extend the current trace.

-f, --first, --first-deadlock

Stop search at the first deadlock found, and print that trace.

-q, --quiet

Don’t print the target executable to standard output, while executing traces.

-t <traceId|traceSeq>, --trace <traceId|traceSeq>

There are two forms, depending on whether traceId or traceSeq is supplied. If traceId (a number) is supplied, then the search of traces will stop after it completes traceId. If traceSeq, see below.

-v, --verbose

For each trace explored, print its trace sequence. If ‘-v -v’, print all.

-h, --help

Display the command-line options and exit.

target_executable

Target multi-threaded executable (binary)

 

ADDITIONAL PROGRAMS

mcmini-gdb ...<same as mcmini args>...
mcmini-annotate -t <traceSeq> ...<same as mcmini args>...

 

DESCRIPTION

McMini searches all possible traces within certain constraints. A trace is a sequences of transitions (thread operations). McMini searches in lexicographic order according to the id of the thread executing the thread operation. Certain branches of the search are pruned if it can be proved that a different branch produces identical semantics. Each trace is numbered sequentially.

McMini stops its search according to three stop criteria:

1. when a trace number is reached, as specified by -t <traceId>; or

2. when a trace results in deadlock, if -f was specified; or

3. when a specific trace sequence is specified by -t <traceSeq>.

(See the subsection on McMini advanced features using trace sequences for a description of trace sequences for -t.)

The three stop criteria can also be used in combination, including (for example) -t 2 -t '0,0,1,2' . In this example, McMini begins each trace with the prefix given by thread ids ‘0,0,1,2’ running in sequence. Within those searches for that prefix, McMini -t 3 will examine thread traces: traceId 0, 1, and finally stopping at traceID 2.

TODO: Check if assertion and segfault also stop the search when :option:`-f` is specified.

Another option, which modifies the traces that McMini searches, is -m (the maximum depth, or number of transitions, executed by any one thread). Any traces reaching this maximum depth are then truncated, and the following branch is then searched.

Finally -v (verbose) prints the trace sequence for each trace that is searched. The option -v -v also prints out the full transitions encountered for that trace.

And -q (quiet) discards any output to the screen (stdout and stderr).

McMini advanced features using trace sequences

McMini -t flag using a traceSeq:

mcmini -t 0 -t <traceSeq> [-m <num>] [-f] [-q] target_executable

In this variation, a trace sequence is supplied (such as the trace sequence 0, 0, 0, 1, 1, from line 9 of the McMini output in the Quick Start section). The option -t 0 was supplied to ensure that only this one trace sequence is explored. If -t 0 is omitted, then the trace sequence will be viewed as a prefix, and McMini will search all traces with this prefix.

TODO: mcmini break and mcmini continue: Declare user breakpoints, and then McMini uses continue_until to stop on user breakpoint while ignoring ‘mcmini forward’, etc. After this, ‘mcmini where’ will still work.

TODO: mcmini printTraceSequence: call programState->printTraceSequence(). But Python can parse it. If it’s too long, then print it in abbreviated form:

> ..[transitionId:].. 1, 2, 1, 1, 2, 1, …

TODO: In future, have a one-line window for TUI to display the trace sequence dynamically, and always.

TODO: Add to the mcmini-gdb tutorial on the next page, describing also break and continue, and including some pictures of the GDB TUI at certain stages. Start with something like:

Annotated addition to the McMini output:

python3 mcmini-annotate -t <traceSeq> [-q] target_executable

In this variation, a more expansive description of the McMini output is produced, including the function, file and line number at which each transition occurred.

McMini extensions to GDB for analyzing a trace:

mcmini-gdb -t <traceSeq> [-q] target_executable

In this variation, the command opens a GDB session. Additional GDB commands are provided. Each new GDB command requires the prefix mcmini. For a quick orientation, do:

> (gdb) mcmini help

mcmini -- mcmini <TAB> : show all mcmini commands
mcmini back -- Go back one transition of current trace, by re-executing
mcmini forward -- Execute until next transition; Accepts optional arg: <count>; or: end
mcmini help -- Prints help for getting started in McMini
mcmini printTransitions -- Prints the transitions currently on the stack
mcmini where -- Execute where, while hiding McMini internal call frames

For further details, see:

• advanced features of McMini

---

Citations

[mcmini_paper]

- “McMini: A Programmable DPOR-based Model Checker for Multithreaded Programs”, Maxwell Pirtle, Luka Jovanovic, and Gene Cooperman, The Art, Science, and Engineering of Programming 8(1), Jun. 15, 2023, https://programming-journal.org/2024/8/1/

[dpor]

- “Dynamic Partial-order Reduction for Model Checking Software”, Cormac Flanagan and Patrice Godefroid, ACM Sigplan Notices 40.1 (2005): pp. 110-121.

Search page

• Search Page