Static Analysis of Lockless Microcontroller C Programs

Eva Beckschulze
(Embedded Software Laboratory RWTH Aachen University, Germany)
Sebastian Biallas
(Embedded Software Laboratory RWTH Aachen University, Germany)
Stefan Kowalewski
(Embedded Software Laboratory RWTH Aachen University, Germany)

Concurrently accessing shared data without locking is usually a subject to race conditions resulting in inconsistent or corrupted data. However, there are programs operating correctly without locking by exploiting the atomicity of certain operations on a specific hardware. In this paper, we describe how to precisely analyze lockless microcontroller C programs with interrupts by taking the hardware architecture into account. We evaluate this technique in an octagon-based value range analysis using access-based localization to increase efficiency.

In Franck Cassez, Ralf Huuck, Gerwin Klein and Bastian Schlich: Proceedings Seventh Conference on Systems Software Verification (SSV 2012), Sydney, Australia, 28-30 November 2012, Electronic Proceedings in Theoretical Computer Science 102, pp. 103–114.
Published: 26th November 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.102.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org