SafeMC: A system for the design and evaluation of mode-change protocols

Real-time systems with multiple modes require mode-change protocols (MCPs) to ensure safety during mode transitions. A variety of MCPs are available in the literature; however, it can be difficult to tell which of them is the most suitable for a given application. This is because 1) existing work often evaluates MCPs analytically, without considering platform-specific overheads in a real deployment; 2) experimental evaluations, where available, tend to make very different choices in run-time environments and workloads, which hinders a direct comparison; and 3) practical applications often require at least some customization, which can completely invalidate the analysis and/or experimental evaluation of the underlying MCP. In this paper, we take a first step towards more principled comparisons. We identify a set of fundamental primitives that most MCPs tend to be built on, and we show that a variety of existing MCPs can be formulated by composing these primitives in different ways. We then present SafeMC, a system for specifying and evaluating current and new MCPs. SafeMC provides an easy-to-use specification language, a library of existing MCPs that can be customized by the user, as well as several tools for test generation, automatic evaluation, tracing, and performance analysis. To demonstrate the utlity of SafeMC, we use it to compare the performance of five classical MCPs in Xen. SafeMC is designed to be extensible and reusable, and we hope that it can serve as a building block for future research in this area.