Static Analysis of Lockless Microcontroller C Programs

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

Full description

Bibliographic Details
Main Authors: Eva Beckschulze, Stefan Kowalewski, Sebastian Biallas
Format: Article
Language:English
Published: Open Publishing Association 2012-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1211.6192v1
id doaj-075bc8abb6e747499c63421b2e59bbb6
record_format Article
spelling doaj-075bc8abb6e747499c63421b2e59bbb62020-11-24T21:03:44ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-11-01102Proc. SSV 201210311410.4204/EPTCS.102.10Static Analysis of Lockless Microcontroller C ProgramsEva BeckschulzeStefan KowalewskiSebastian BiallasConcurrently 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.http://arxiv.org/pdf/1211.6192v1
collection DOAJ
language English
format Article
sources DOAJ
author Eva Beckschulze
Stefan Kowalewski
Sebastian Biallas
spellingShingle Eva Beckschulze
Stefan Kowalewski
Sebastian Biallas
Static Analysis of Lockless Microcontroller C Programs
Electronic Proceedings in Theoretical Computer Science
author_facet Eva Beckschulze
Stefan Kowalewski
Sebastian Biallas
author_sort Eva Beckschulze
title Static Analysis of Lockless Microcontroller C Programs
title_short Static Analysis of Lockless Microcontroller C Programs
title_full Static Analysis of Lockless Microcontroller C Programs
title_fullStr Static Analysis of Lockless Microcontroller C Programs
title_full_unstemmed Static Analysis of Lockless Microcontroller C Programs
title_sort static analysis of lockless microcontroller c programs
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2012-11-01
description 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.
url http://arxiv.org/pdf/1211.6192v1
work_keys_str_mv AT evabeckschulze staticanalysisoflocklessmicrocontrollercprograms
AT stefankowalewski staticanalysisoflocklessmicrocontrollercprograms
AT sebastianbiallas staticanalysisoflocklessmicrocontrollercprograms
_version_ 1716773223208583168