Lock Optimization for Hoare Monitors in Real-Time Systems
2017 17th International Conference on Application of Concurrency to System Design (ACSD)(2017)
摘要
Hoare monitors are a safe concurrency abstraction built around a monitor with shared state and methods that operate on the shared state. While well-known, they have been little used as a concurrency framework in real-time systems. We describe a Hoare monitor framework called Tower developed for real-time systems programming that targets multiple real-time operating systems. Hoare monitors use coarse-grained locking across all of the methods in a monitor. In a real-time setting, this coarse-grained locking can be too restrictive, but it is difficult and tedious for a programmer to reason about which methods may safely execute in parallel. Therefore, we present an automated compiler optimization for refining locks in Hoare monitors using partially-weighted MAXSAT. We formalize Tower semantics using Petri nets and show that safe concurrency is preserved under the optimization. Finally, we present a number of empirical benchmarks for our optimization as well as a case-study of a real-time autopilot built and optimized with our approach.
更多查看译文
关键词
concurrency framework,Hoare monitor framework,real-time operating systems,real-time setting,lock optimization,safe concurrency abstraction,shared state,real-time systems,Hoare monitors,automated compiler optimization,lock refining,real-time systems programming,coarse-grained locking,partially-weighted MAXSAT,Tower semantics,Petri nets,real-time autopilot
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络