Detecting Atomicity Races in ARINC 653 Applications

Atomicity races in ARINC 653 applications are a kind of concurrency bugs which causes nondeterministic behaviors by parallel processes. This paper presents a tool, called AR653, to dynamically detect atomicity races. The tool monitors only synchronization operations and access to shared resources, and analyzes the relation of synchronizations to report atomicity races through a locking discipline of semaphores. We compared the accuracy of AR653 with CodeSonar using synthetic programs on a simulation system for integrated modular avionics. The empirical results show that our tool correctly reports atomicity races, while CodeSonar only locates atomicity races in cases of using shared variables.