Dev:Partial Program Admission

Warning: This page is still in placeholder form and shouldn't even have external links yet. However you found it, you shouldn't have. Read at own risk to sanity and hygiene.

Partial Program Admission (PPA) is a graph transformation technique for Control Flow Graphs (CFGs), used to statically bound program execution time to safely support untrusted, 3rd-party software on event-driven, real-time, non-preemptive systems. Given a program and a cycle budget, we view the program as a collection of execution paths. Those paths which complete under the cycle budget are retained. Those paths which would take longer than the budget are excluded by intercepting and redirecting them to a “time-exceeded” exception handler. The process avoids adding any runtime overhead to programs by substituting code duplication for semantic knowledge.

Problem Context

We developed the PPA technique for high-speed virtual networking, but the technique is useful anywhere untrusted code needs to share non-preemptive systems with other code while meeting real-time guarantees.

PPA is useful when:

• preemption is impractical
• the execution time of instructions can be determined locally. This usually means:
  • no cache
  • no branch prediction
• cycle budgets are small
• runtime overhead is unacceptable
• instruction store is under-populated.

Programs are submitted by a developer, along with a “time-exceeded” exception handler (X) and a cycle budget B. X is written to very restrictive rules that make it easy to determine X’s execution time.

In traditional admission control, we would examine the program to determine if it can exceed the budget B. If so, we reject it; otherwise, we can accept it. This requires computing the Worst-Case Execution Time (WCET) of the program, a hard problem. This hard problem is made even worse by the fact that we can't trust the developer to tell us anything about the program. For example, we can’t determine loop iteration bounds, which means we can’t tell the difference between a loop with 2 iterations and an infinite loop.

We side-step the hard problem of WCET analysis by enforcing the limit instead of determining whether it is exceeded.

Concept Overview

Instead of computing the real WCET of a program, we can transform it so that we reject all paths that exceed the budget while retaining the safe paths. Consider ...continue from here...

Formal Treatment

All of these things can be expressed formally, in first-order logic. (To Be Done)

Algorithm Introduction

Here's how we do it in practice. (To Be Done)

Branch Constraints

All of this is a bit lacking when it comes to subroutines and loops. (To Be Done)