Analyzing Code Stability Using Control Theoretic Techniques

You must register and request HCSS Community Membership to view the slides.

Abstract: Controller-Oriented Programming (COP) is a new programming language paradigm designed to enable the creation of software that is efficient and adaptable simultaneously. COP introduces two new programming language concepts: 1) partitions, which capture setsof implementation options that are extensionally rather than intensionally equivalent, and 2) controllers, which dynamically select among these options and manage side effects and other couplings to enable systems to act like they are decoupled. Because theycapture and dynamically reinforce invariants, we hypothesize that partitions and controllers will facilitate formal analysis, and weare working with SRI toaugmentYices with the concept of partitionsto create a SymSolverandto understand the implications theymay have for scalable formal analysis of invariantsmore generally. This talk will explore how techniques adopted from control theory can be applied to analyze the stability of software and, specifically, code written in SymLang, the first instance of a COP language. We define stability as bounded input bounded output, a standard definition in control theory. As our working example, we use a simple data store problem: given an unbounded stream of integer values, return within a bounded period whether a particular value has been seen previously. To analyze stability of a SymLang solution, we first derive a control theory style block diagram that captures the dynamics of the implementation. Next, we take the Laplace transform and derive the transfer function that describes the number of available stores (output) as a function of inserted values (input). Finally, we solve for the poles of the transfer function and show they are all in the left half plane (have real part less than zero), indicating the implementation is stable. These techniques can also be used to show that implementations are not stable, and we analyze two real bugs introduced by junior engineers and show the resulting (buggy) implementations are not stableto demonstrate the practical benefit of this approach.

Jessa Lee is the Chief Technology Officer of Apogee Research. She holds a B.S. in physics and an M.S. in Electrical Engineering, both from Stanford University. Jessa started her career in Silicon Valley, before transitioning to the DoD to focus on solving hard problems that impact National Security. In her time at Apogee, she has served as software lead for STITCHES and led the development of Controller-Oriented Programming, a new programming language paradigm designed to facilitate the creation of software implementations that are adaptable and efficient simultaneously, under DARPA's IDAS program.