The One Page Model Checker

TL;DR

This paper presents a compact, one-page C implementation of a model checker that uses standard IPC mechanisms and fork() to verify deadlocks and race conditions in multithreaded programs, demonstrating simplicity and broad applicability.

Contribution

It introduces a minimal, easy-to-implement model checking approach leveraging standard IPC and fork(), suitable for checking concurrency issues in multithreaded applications.

Findings

Effective detection of deadlocks and race conditions.

Minimal code implementation fits in one page.

Applicable to multiple programming languages.

Abstract

We show how standard IPC mechanisms can be used with the fork() system call to perform explicit state model checking on all interleavings of a multithreaded application. We specifically show how to check for deadlock and race conditions in programs with two threads. Our techniques are easy to apply to other languages, and require only the most rudimentary parsing of the target language. Our fundamental system fits in one page of C code.