Pthread Model Checker is a model checking tool for multithreaded programs with POSIX thread (pthread). Using it, you can detect problems which could be difficult to find by testing, such as deadlocks and livelocks.
You can write models in the programming language C (a subset). You need not study yet another modeling language.
Pthread Model Checker automatically performs the following checks:
In addition, you can perform two types of assertion checks. One is general assertion defined in the standard header 'assert.h'. Another is called 'global assertion' which can monitor the values of global variables through the whole execution of a program. It is not needed to write down a detailed specification or write complicated temporal logic expressions. Pthread Model Checker automatically translates a model into a labelled transition system and checks the states exhaustively.
Pthread Model Checker performs checks in parallel. You can check large scale models fast by utilizing multicore CPUs and cloud computing power.
Please see the reference manual and related documents.
|[*1]||Recursive mutexes are not supported.|
|[*2]||All threads must be PTHREAD_CREATE_JOINABLE.|
|How many threads can be used in checking||1||4||Unlimied|
|Available Memory Size||Limited||Unlimited||Unlimied|
|Commercial Use||Not permitted||Not permitted||Permitted|
|One-year License (without tax)||—||6,000 JPY||90,000 JPY|
|OS||Linux, macOS (64 bit)*1|
|CPU||Intel or AMD, x86_64 compatible processor (48 bit logical address space)|
|Memory||4 GiB or more*2|
|Storage||at least 100 MiB|
|[*1]||In the case of Microsoft Windows 10 (64bit), Linux version is available on Windows Subsystem for Linux.|
|[*2]||The required memory depends on the size of a model.|