Lock Optimization for Hoare Monitors in Real-Time Systems

• ABSTRACT:
  
  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 \emph{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.

• BIBTEX:
  

  @inproceedings{axel:acsd17,
    author    = {Georges-Axel Jaloyan and Lee Pike},
    title     = {Lock Optimization for Hoare Monitors in Real-Time Systems},
    booktitle = {Proceedings of the 17th International Conference on Application of Concurrency to System Design} (ACSD)},
    year      = {2017},
    publisher = {IEEE},
    note      = {Available at \url{https://leepike.github.io/pub_pages/acsd17.html}.}
  }

• PAPER DOWNLOAD: pdf