Pthread Model Checker Reference Manual

Table of Contents

0  How to use Pthread Model Checker

The process to use Pthread Model Checker consists of four steps:

  1. Write a model in C.
  2. Perform ptmc command which translates the model into another C code.
  3. Compile the translated code by gcc and link with libptmc.a.
  4. Run the executable. It performs checks and makes a report file.

ptmc command also generates a state transition graph in a Graphviz dot format. Please convert it to any graphic format you like such as PNG or PDF with dot command. It helps you consult the report file.

0.0  Perform ptmc command

ptmc reads the specified model file model, then generates a C source code check-src and a state transition graph file model.dot.

ptmc [option ...] model check-src

0.0.0  Command line options

-D <id>=<value>

define the constant <id> as defined in a model with #define.

0.1  Compile the C source code

Compile the C source code generated by ptmc command and link it with libptmc.a.

gcc -O3 -o check-prog check-src [ptmc_license.o] -L libpath -lptmc -pthread

If you have a license file ptmc_license.o, link it here.

0.2  Perform the executable

check-prog [option ...]

0.2.0  Command line options

-o report-filename

Specify the name of report file. If not specified, <model-filename>+ .report is used.

-n num-threads

Specify the number of threads performing checks in parallel. The default is 1.

-m heap-size

Specify the maximum size of memory which can be used in checking in GiB. Note that each thread uses this size of memory, not total.

-t hashtable-size

Specify the number of entries of the hash table internally used to record states.

-s

turn on spurious wakeups on pthread_cond_wait.

-v

If this option is specified, the checking progress is shown as a pair of the distance from the initial state and the number of states at the distance.

1  The definition of the C subset (modeling language)

1.0  Types

The following types are supported:

pointer types, structures, unions, and enums are not supported.

As an exception, since the type pointer to 'void' is used in pthread_create, pthread_join, and thread functions, 'void *' can be used in function parameters and local variables. They are interpreted as 'int8_t'.

In addition, the types intptr_t and uintptr_t are used in cast expressions when mutually converting pointer to void and integer types in order to avoid compiler warnings.

The sizes of integer types are defined as follows:

It is strongly recommended to use as small types as possible to reduce the size of states.

1.1  Constants

The following constants are predefined.

1.2  Preprocessor directives

The Preprocessor directive #define can be used to define integer constants. Macros with parameters cannot be defined.

Exmaples:

#define N   16
#define N1  (N + 1)

The directives other than #define are ignored. To make a model runnable, The following lines can be placed at the top of the model.

#include <stdio.h>
#include <stdbool.h>
#include <stdint.h>
#include <inttypes.h>
#include <pthread.h>
#include <assert.h>

1.3  Constant definition with enum

Although enum type is not supported, enum can be used to define a series of constants. It is not possible to name the enum and specify the value of each constant.

Example:

enum { REQ, ACK, NAK };

1.4  Variables

The type of local variables must be integer or array of integers.

1.5  Suppoerted pthread functions

1.5.0  Thread creation and termination

The thread attributes are not supported. The second argument of pthread_create must be NULL. As a result, all threads are PTHREAD_CREATE_JOINABLE and they must be get joined eventually.

1.5.1  Mutexes

Variables declared with type pthread_mutex_t are regardeds as initialized. The mutex attributes are not supported. In paricular, recursive locking is not supported.

If you would like to make models runnable, the initializer PTHREAD_MUTEX_INITIALIZER or the function pthread_mutex_init can be used. Pthread Model Checker just ignores them.

pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;

1.5.2  Condition variables

Variables declared with type pthread_cond_t are regardeds as initialized. The attributes of condition variables are not supported.

If you would like to make models runnable, the initializer PTHREAD_COND_INITIALIZER or the function pthread_cond_init can be used. Pthread Model Checker just ignores them.

pthread_cond_t condvar = PTHREAD_COND_INITIALIZER;

1.6  Functions

Recursive functions are not supported. ** Assertions

Pthread Model Checker supports two types of assertions:

1.6.0  assert

This is so-called 'assert' defined in the standard header 'assert.h'.

You can specify any condition at any place.

δΎ‹:

int main(void)
{
    int x = 12;
    assert(x == 12);
    return 0;
}

1.6.1  Global assert

Global assert is a condition in terms of global variables which are checked at all of states regardless of the location of each thread. This assertion can be used to describe safety condition.

Global asserts are specified in comments in the following format:

// @ASSERT(expression)

The following exmaple shows the condition that "the global variable count never be 2."

int8_t count;
// @ASSERT(count != 2)

1.7  Ignored functions

Pthread Model Checker ignores the following function calls:

1.8  Nondeterministic choice statement AMB

The AMB statement makes it possible to describe nondeterministic choice. It has the following format.

AMB stmt1 OR stmt2

The semantics of the AMB statement is that one of the branches stmt1 or stmt2 is nondeterministically chosen and is executed.

For example, the following statement results in x = 0 or x = 1. In the checking context, both possibilities are checked.

AMB x = 0; OR x = 1;
assert(x == 0 || x == 1);

In order to make models exeuctable, the following header file can be used.

amb.h

#include <stdlib.h>

#define AMB if (rand() % 2)
#define OR  else

2  Report file

When a defect is found as a result of checking, a report file is generated and the shortest path from the initial state to the problematic state is shown.

Example:

A global variable count is defined. Two threads independently increment count. After the termination of the threads, check if the value of count is 2 by assert.

pthread_t pth1, pth2;
int count;

void *thread(void *arg)
{
    count++;
    return NULL;
}

int main(void)
{
    void *r;
    pthread_create(&pth1, NULL, &thread, NULL);
    pthread_create(&pth2, NULL, &thread, NULL);
    pthread_join(pth1, &r);
    pthread_join(pth2, &r);
    assert(count == 2);
    return 0;
}

The assertion violation is reported:

$ ptmc increment.c increment.ptmc.c
$ gcc -o increment increment.ptmc.c -lptmc -pthread
$ ./increment
assertion violation
increment.c:23: assert(count == 2);

The contents of the report file is as follows:

version: 1.x.x
model_filename: "increment.c"
num_workers: 1
heap_size: 134217728 bytes
hashtable_size: 4000037 entries
assertion violation
increment.c:23: assert(count == 2);
num-of-states: 40

#0 main nil
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 1
------------------------
#1 main create pth1
19: pthread_create(&pth1, NULL, &thread, NULL);
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 2
1 pth1 8
    arg = 0
------------------------
#2 main create pth2
20: pthread_create(&pth2, NULL, &thread, NULL);
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 8
    arg = 0
2 pth2 8
    arg = 0
------------------------
#3 pth2 load count
12: count++;
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 8
    arg = 0
2 pth2 9
    t5 = 0
------------------------
#4 pth1 load count
12: count++;
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 9
    t5 = 0
2 pth2 9
    t5 = 0
------------------------
#5 pth1 store count
12: count++;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 10
2 pth2 9
    t5 = 0
------------------------
#6 pth1 exit
13: return NULL;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 0
    retval = 0
2 pth2 9
    t5 = 0
------------------------
#7 pth2 store count
12: count++;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 0
    retval = 0
2 pth2 10
------------------------
#8 main join pth1
21: pthread_join(pth1, &r);
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 4
1 pth1 ---
2 pth2 10
------------------------
#9 pth2 exit
13: return NULL;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 4
1 pth1 ---
2 pth2 0
    retval = 0
------------------------
#10 main join pth2
22: pthread_join(pth2, &r);
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 5
------------------------
#11 main load count
23: assert(count == 2);
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 6
    t6 = 1
------------------------

2.0  A State Transition graph

You can see the state transition graph generated by ptmc command by running dot command as follows: (make sure Graphviz is installed.)

$ dot -T png -o increment.png increment.c.dot

The boxes indicates states. IN and OUT means a list of local variables live at the entry/exit of the state respectively.

The number shown after the transition label is the line number in the model file corresponding to the transition.

2.1  Transition part

The path consists of two parts: transition part and state part.

The part starting with hash sign # indicates a transition. The number following the hash sign indicates the number of steps from the initial state. This example shows that the main thread has created a new thread named 'pth2.

The next line is a line of model correspoinding to this transition.

------------------------
#2 main create pth2
20: pthread_create(&pth2, NULL, &thread, NULL);
------------------------

2.2  State part

------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 8
    arg = 0
2 pth2 8
    arg = 0
------------------------

Some statement like count++ is divided into more than one transitions, which indicates the actual behavior of CPUs.

In this example, count++ is divided into load and store.

------------------------
#4 pth1 load count
12: count++;
------------------------
global vars:
    count = 0
mutex:
thread:
0 main 3
1 pth1 9
    t5 = 0
2 pth2 9
    t5 = 0
------------------------
#5 pth1 store count
12: count++;
------------------------
global vars:
    count = 1
mutex:
thread:
0 main 3
1 pth1 10
2 pth2 9
    t5 = 0
------------------------

2.3  Example for mutexes and condition variables

#define N   1
#define NP  1
#define NC  2

pthread_t pthp[NP];
pthread_t pthc[NC];
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
pthread_cond_t cv = PTHREAD_COND_INITIALIZER;
int count;
...

A mutex which is not locked is show as '<unlocked>'.

------------------------
global vars:
    count = 0
mutex:
    mutex <unlocked>
thread:
0 main 9
    i = 1
1 pthp[0] 34 wait cv
2 pthc[0] 24
3 pthc[1] 19
------------------------

On the other hand, a locked mutex is shown with the name of the owner thread.

The thread waiting a condition variable is annotated with the 'wait' sign and the name of the condition variable.

------------------------
global vars:
    count = 0
mutex:
    mutex pthc[0]
thread:
0 main 8
1 pthp[0] 34 wait cv
2 pthc[0] 21
    t14 = 0
3 pthc[1] 24 wait cv
------------------------
© 2017 PRINCIPIA Limied