# 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.

## 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.

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:

• char short int long unsigned int8_t int16_t int32_t int64_t uint8_t uint16_t uint32_t uint64_t
• 1-dimensional array of above types

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:

• sizeof(short) = 2
• sizeof(int) = 4
• sizeof(long) = 8

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.

• NULL regarded as integer 0.
• true regarded as integer 1.
• false regarded as integer 0.

## 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 <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.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.

### 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.

## 1.6  Functions

Recursive functions are not supported. ** Assertions

Pthread Model Checker supports two types of assertions:

• assert
• global assert

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

• printf
• sleep
• usleep

## 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;

{
count++;
return NULL;
}

int main(void)
{
void *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
------------------------


## 2.2  State part

• 'global vars' shows the values of each global variables in this state.
• 'mutex' shows the status of mutexes. (it is empty since this example uses no mutex.)
• 'thread' shows the location and the values of each local variables of each thread. The location is indicated as a state id on the state transition graph.
------------------------
global vars:
count = 0
mutex:
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.

------------------------
12: count++;
------------------------
global vars:
count = 0
mutex:
0 main 3
1 pth1 9
t5 = 0
2 pth2 9
t5 = 0
------------------------
#5 pth1 store count
12: count++;
------------------------
global vars:
count = 1
mutex:
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

int count;
...


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

------------------------
global vars:
count = 0
mutex:
mutex <unlocked>
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]