A model-based approach to platform-level power and clock management

Abstract

The correct management of a platform’s power and clock resources is vital for the correct operation of the platform’s hardware, which in turn forms the cornerstone of any assurances provided by software. In light of this, the firmware implementing such a power and clock management solution should ideally provide strong correctness guarantees. However, to the extent of our knowledge, the current state of the art does not go beyond manually-coded point solutions. This thesis approaches the problem of power and clock management in a more principled fashion: It proposes a model that captures the behaviour of the platform in this management context. Additionally, a set of mechanisms are presented that, if applied to any model instance, generate management solutions for the platform described by that instance. If the correctness of these mechanisms were formally verified, which was not possible within the time constraints of this thesis, provably correct management solutions could be generated for any platform whose behaviour can be expressed by the model.