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...
Main Authors: | , , |
---|---|
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 |