Static Analysis of Interrupt-driven Programs Synchronized via the Priority Ceiling Protocol

被引：0
|
作者：
Schwarz, Martin D. [1 ]
Seidl, Helmut [1 ]
Vojdani, Vesal [1 ]
Lammich, Peter [2 ]
Mueller-Olm, Markus [2 ]
机构：
[1] Tech Univ Munich, D-85748 Garching, Germany
[2] Univ Munster, D-48149 Munster, Germany
来源：
ACM SIGPLAN NOTICES | 2011年 / 46卷 / 01期
关键词：
Algorithms; Theory; Verification; inter-procedural analysis; abstract domains; interrupt-driven concurrency; INHERITANCE PROTOCOLS; ATOMICITY; NETWORKS; SYSTEMS; STACK; LOCKS;
D O I：
10.1145/1925844.1926398
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We consider programs for embedded real-time systems which use priority-driven preemptive scheduling with task priorities adjusted dynamically according to the immediate ceiling priority protocol. For these programs, we provide static analyses for detecting data races between tasks running at different priorities as well as methods to guarantee transactional execution of procedures. Beyond that, we demonstrate how general techniques for value analyses can be adapted to this setting by developing a precise analysis of affine equalities.
引用
收藏
页码：93 / 104
页数：12
相关论文
共 43 条
  • [1] Static Analysis of Interrupt-driven Programs Synchronized via the Priority Ceiling Protocol
    Schwarz, Martin D.
    Seidl, Helmut
    Vojdani, Vesal
    Lammich, Peter
    Mueller-Olm, Markus
    POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2011, : 93 - 104
  • [2] Numerical Static Analysis of Interrupt-Driven Programs via Sequentialization
    Wu, Xueguang
    Chen, Liqian
    Mine, Antoine
    Dong, Wei
    Wang, Ji
    2015 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT), 2015, : 55 - 64
  • [3] Static Analysis of Runtime Errors in Interrupt-Driven Programs via Sequentialization
    Wu, Xueguang
    Chen, Liqian
    Mine, Antoine
    Dong, Wei
    Wang, Ji
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2016, 15 (04)
  • [4] Static race detection of interrupt-driven programs
    Huo, Wei
    Yu, Hongtao
    Feng, Xiaobing
    Zhang, Zhaoqing
    Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2011, 48 (12): : 2290 - 2299
  • [5] Stack size analysis for interrupt-driven programs
    Chatterjee, K
    Ma, D
    Majumdar, R
    Zhao, T
    Henzinger, TA
    Palsberg, J
    STATIC ANALYSIS, PROCEEDINGS, 2003, 2694 : 109 - 126
  • [6] Stack size analysis for interrupt-driven programs
    Chatterjee, K
    Ma, D
    Majumdar, R
    Zhao, T
    Henzinger, TA
    Palsberg, J
    INFORMATION AND COMPUTATION, 2004, 194 (02) : 144 - 174
  • [7] Data Races and Static Analysis for Interrupt-Driven Kernels
    Chopra, Nikita
    Pai, Rekha
    D'Souza, Deepak
    PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2019: 28TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2019, 11423 : 697 - 723
  • [8] A Denotational Model for Interrupt-Driven Programs
    Huang, Yanhong
    Zhao, Yongxin
    Shi, Jianqi
    Zhu, Huibiao
    IEEE SIXTH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW 2013), 2013, : 15 - 20
  • [9] Static checking of interrupt-driven software
    Brylow, D
    Damgaard, N
    Palsberg, J
    PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2001, : 47 - 56
  • [10] Efficient data race detection for interrupt-driven programs via path feasibility analysis
    Zhao, Jingwen
    Wu, Yanxia
    Dong, Jibin
    JOURNAL OF SUPERCOMPUTING, 2024, 80 (15): : 21699 - 21725
12345