[PROPL'24] Formal Methods to Save the Earth

Hongyi Huang, Jialin Li, Umang Mathur

With the rise of power demands for energy-greedy applications, such as large-scale data centers, machine learning models, and block-chain computation, higher proportion of energy consumption and carbon emissions can be attributed to computing machines [Manyika et al . 2011] [Liu 2013]. It is crucial to make computing more sustainable and environment-friendly. In a race with time, enabling regulatory bodies to enforce strict energy budgets on computing applications may fast track the progress towards the goal of green computing. Towards this, we revisit some approaches to analyzing the energy consumption of software and hardware applications, and analyze their strengths and weaknesses. We then turn to deductive methods and propose the operational semantics behind a program logic, which we call Power Logic, that can be used to formally specify and verify energy consumption. This set of operational semantics is abstracted from real-world computer systems and aims to reflect the ground truths about energy consumption in a system during small steps of computation. On top of these small-step rules, we hope to prove or specify the energy consumption of a certain program. Finally, we discuss potential directions in which Power Logic can further evolve.