Analyzable Publish-Subcribe Communication Through a Wait-Free FIFO Channel for MPSoC Real-Time Applications

摘要

As a transparent communication protocol for concurrent distributed applications, the Publish-Subscribe (Pub-Sub) paradigm is a trending programming model in many recent industrial use-cases in robotics and avionics. To apply the Pub-Sub programming model for safety-critical concurrent realtime applications in Multi-Processor Systems on Chip (MPSoC) environments, a non-blocking wait-free First-In-First-Out (FIFO) channel is a fundamental requirement. However, the proposed approaches in the literature have no proven real-time guarantees. In this paper, we propose a novel wait-free FIFO approach for single-producer-single-consumer core-to-core communication through shared memory. By analyzing the execution paths of each involved process, we prove that the execution time of each read/write operation is bounded by a Worst Case Execution Time (WCET). Moreover, we define a Timed Automata model of our approach. Using the UPPAAL model checker, we prove freedom of deadlock and starvation. For the performance evaluation of the proposed approach, we apply a stochastic analysis technique on the defined UPPAAL model. Finally, we implement the proposed approach on the CompSOC platform as the underlying realtime MPSoC to show that the implementation conforms to the proposed formal model and to experimentally validate the formal properties. The experimental evaluation on an instance of CompSOC that works at 40 MHz has a throughput of 109K tokens per second.