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 safely support untrusted, 3rd-party software on event-driven, real-time, non-preemptive systems.

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.

Concept Overview

What is this PPA thing, anyway?

Formal Treatment

All of these things can be expressed formally, in first-order logic.

Algorithm Introduction

Here's how we do it in practice.

Branch Constraints

All of this is a bit lacking when it comes to subroutines and loops.