Optimizing Declarative Power Sequencing

Managing a modern computing platform’s power and clock infrastructure is an increasingly complex task. Failure to manage it correctly can result in grave consequences, up to the destruction of vital components. The increasing complexity, coupled with a desire for remote monitoring and management, has led to the task of managing power moving away from hard-wired solutions or simple hardware controllers, and on to baseboard management controllers (BMCs). These are fully-fledged computers in their own right, often running commodity software and connected to a network. Given the importance of their tasks, it is desirable that the BMC software be able to provide high assurance that it will operate correctly. One avenue to improve confidence is to have power sequences generated from a declarative platform model, instead of having humans write them. This thesis aims to improve on previous work in the area of declarative power sequencing by introducing optimization capabilities into the process, allowing us to automatically generate power states that optimize objectives such as power usage