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