Static Analysis of Lockless Microcontroller C Programs

被引:3
|
作者
Beckschulze, Eva [1 ]
Biallas, Sebastian [1 ]
Kowalewski, Stefan [1 ]
机构
[1] Rhein Westfal TH Aachen, Embedded Software Lab, Aachen, Germany
关键词
D O I
10.4204/EPTCS.102.10
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:103 / 114
页数:12
相关论文
共 50 条
  • [1] A Memory Model for Static Analysis of C Programs
    Xu, Zhongxing
    Kremenek, Ted
    Zhang, Jian
    [J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT I, 2010, 6415 : 535 - +
  • [2] A Library Modeling Language for the Static Analysis of C Programs
    Ouadjaout, Abdelraouf
    Mine, Antoine
    [J]. STATIC ANALYSIS (SAS 2020), 2020, 12389 : 223 - 247
  • [3] SharpChecker: Static analysis tool for C# programs
    Koshelev, V. K.
    Ignatiev, V. N.
    Borzilov, A. I.
    Belevantsev, A. A.
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2017, 43 (04) : 268 - 276
  • [4] Modular Static Analysis of String Manipulations in C Programs
    Journault, Matthieu
    Mine, Antoine
    Ouadjaout, Abdelraouf
    [J]. STATIC ANALYSIS (SAS 2018), 2018, 11002 : 243 - 262
  • [5] SharpChecker: Static analysis tool for C# programs
    V. K. Koshelev
    V. N. Ignatiev
    A. I. Borzilov
    A. A. Belevantsev
    [J]. Programming and Computer Software, 2017, 43 : 268 - 276
  • [6] Inferring Effective Types for Static Analysis of C Programs
    Jeannet, Bertrand
    Sotin, Pascal
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 288 : 37 - 47
  • [7] Type Inference for C: Applications to the Static Analysis of Incomplete Programs
    Melo, Leandro T. C.
    Ribeiro, Rodrigo G.
    Guimaraes, Breno C. F.
    Quintao Pereira, Fernando Magno
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2020, 42 (03):
  • [8] Static Bound Analysis of Dynamically Allocated Resources for C Programs
    Fan, Guangsheng
    Chen, Taoqing
    Yin, Banghu
    Chen, Liqian
    Wang, Tengbin
    Wang, Ji
    [J]. 2021 IEEE 32ND INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING (ISSRE 2021), 2021, : 390 - 400
  • [9] Static analysis of string manipulations in critical embedded C programs
    Allamigeon, Xavier
    Godard, Wenceslas
    Hymans, Charles
    [J]. STATIC ANALYSIS, PROCEEDINGS, 2006, 4134 : 35 - 51
  • [10] LLVM based approach to static analysis of C programs in SAPFOR
    Kataev, Nikita
    [J]. 2018 IVANNIKOV MEMORIAL WORKSHOP (IVMEM 2018), 2018, : 19 - 23