Foundational Verification of Running-Time Bounds for Interactive Programs

Thought this was interesting, as I haven't seen work I'm this area before (I don't keep with the research that much). Some gotchas before people get too excited:

Most importantly, our measurement of time is coarse-grained, and we expose a source-level cost model that could be said to leak details of compilation. For the former, our semantics (of source, intermediate, and target languages) track such high-level metrics as numbers of assembly instructions, numbers of memory accesses, and numbers of jumps. For any real processor, those counters allow us to conclude conservative upper bounds on wall-clock time, but those bounds may be very pessimistic. While we are concerned here with microcontrollers where these simple bounds actually do let us derive relatively precise wall-clock bounds (e.g. processors with very minimal use of memory caches), we look forward to future work tracking metrics to support greater precision.

We also ask that source programs be proved against a cost semantics that somewhat telegraphs how the compiler expects to work, revealing costs motivated by the expected mixes of assembly instructions. Indeed, it is an inherent challenge in this domain to allow precise bounds to be proved at the source level without dependence on compiler details, since often compiler optimizations are crucial to meeting deadlines (or, often enough, engineers or certification agencies distrust higher compiler optimization levels and just force system design with laxer deadlines). A common flow is to use source-level analysis to annotate loops with information on how many times they run, which can then be pushed down to assembly code, where detailed worst-case execution time (WCET) analysis is carried out. A downside of that approach is the difficulty of debugging timing issues at the assembly level, whereas we allow timing problems to be found while stepping through Hoare-logic proofs of source files