Development of Synchronization Objects verifier for Linux Device Drivers Based on Process Semantics

Yu. P. Korablin , e-mail: y.p.k@mail.ru, E. G. Pavlov , e-mail: lucenticus@gmail.com

This article describes the tool for finding problem with synchronization of drivers in Linux. This tool uses a method of detecting error basis on semantic models and allows you to detect such synchronization errors as infinity loops, deadlocks, and double locks. In addition, describe the process semantics of synchronization objects of Linux kernel in the language of asynchronous functional schemes

Keywords: verification, device drivers, communicating sequential processes, equational characterization, algebraic semantics

pp. 2–9