“Towards Synthesis of Application-Specific Forward Error Correction (FEC) Codes”

Jedidiah McClurg, Lauren Zoe Baker, Ronaldo Canizales, Dilochan Karki

(HotNets 2024)

Forward error correction (FEC) is a key component of modern high-bandwidth networks. Typically implemented at the physical layer, FEC attaches error-correcting codes to blocks of transmitted data, allowing some corrupted blocks to be repaired without retransmission. We outline a synthesis-based approach for automatic exploration of the FEC-code design space, focusing on Hamming codes. We formally verify the correctness of a Hamming (128,120) code used for FEC in the recent 802.3df Ethernet standard, and provide preliminary evidence that our prototype synthesizer can leverage user-provided formal properties to generate FEC codes that are highly robust, efficiently implementable, and tuned to support specific data formats such as IEEE floating points.

• Location: Irvine
• Date: Nov 2024

“Parallelizing Accelerographic Records Processing”

Ronaldo Canizales, Luis Mixco, Jedidiah McClurg

(ParSocial@IPDPS 2024)

Strong-motion processing holds paramount importance in earthquake engineering and disaster risk management systems. By leveraging parallel loops and task-parallelism techniques, we address computational challenges posed by large-scale accelerographic datasets. Through experimentation with more than one million data points from six real-world seismic events, our approach achieved speedups of up to 2.9x, demonstrating the effectiveness of parallel programming in accelerating seismic data processing. Our findings highlight the significance of parallel programming techniques in advancing seismological research and enhancing earthquake mitigation strategies.

• Location: San Diego
• Date: May 2024

“Optimizing Regular Expressions via Rewrite-Guided Synthesis”

Jedidiah McClurg, Miles Claver, Jackson Garner, Jake Vossen, Jordan Schmerge, Mehmet E. Belviranli

(PACT 2022)

Regular expressions are pervasive in modern systems. Many real-world regular expressions are inefficient, sometimes to the extent that they are vulnerable to complexity-based attacks, and while much research has focused on detecting inefficient regular expressions or accelerating regular expression matching at the hardware level, we investigate automatically transforming regular expressions to remove inefficiencies. We reduce this problem to general expression optimization, an important task necessary in a variety of domains even beyond compilers, e.g., digital logic design, etc. Syntax-guided synthesis (SyGuS) with a cost function can be used for this purpose, but ordered enumeration through a large space of candidate expressions can be prohibitively expensive. Equality saturation is an alternative approach which allows efficient construction and maintenance of expression equivalence classes generated by rewrite rules, but the procedure may not reach saturation, meaning global minimality cannot be confirmed. We present a new approach called rewrite-guided synthesis (ReGiS), in which a unique interplay between SyGuS and equality saturation-based rewriting helps to overcome these problems, resulting in an efficient, scalable framework for expression optimization.

• Location: Chicago
• Date: October 2022

“AxoNN: Energy-Aware Execution of Neural Network Inference on Multi-Accelerator Heterogeneous SoCs”

Ismet Dagli, Alexander Cieslewicz, Jedidiah McClurg, Mehmet Belviranli

(DAC 2022)

The energy and latency demands of critical workload execution, such as object detection, in embedded systems vary based on the physical system state and other external factors. Many recent mobile and autonomous system-on-chips embed a diverse range of accelerators with unique power and performance characteristics. The execution flow of the critical workloads can be adjusted to span multiple accelerators so that the trade-off between performance and energy fits to the dynamically changing physical factors. In this study, we propose running neural network (NN) inference on multiple accelerators. Our goal is to provide an energy-performance trade-off by distributing layers in the NN between a performance- and a power-efficient accelerator. We first provide an empirical modeling methodology to characterize execution and inter-layer transition times. We then find an optimal layer-to-accelerator mapping, by representing the trade-off as a linear programming optimization constraint. We evaluate our approach on the NVIDIA Xavier AGX System-on-Chip with commonly used NN models. We use the Z3 SMT solver to find schedules for different energy consumption targets, with up to 98% prediction accuracy.

• Location: San Francisco
• Date: July 2022

“Correct-by-Construction Network Programming for Stateful Data-Planes”

Jedidiah McClurg

(SOSR 2021)

As switch hardware becomes faster, stateful, and more programmable, functionality that was once confined to end hosts or the control plane is being pushed into the data plane. For example, recent work on adaptive congestion control and heavy hitter detection has used stateful switches to implement sophisticated functionality with only minor controller involvement. In applications where correctness depends on individual switches making coherent decisions, it is important that the switches have a consistent view of the global state. However, such a consistency requirement makes it difficult to maintain efficiency (high throughput), as shown by the CAP theorem. Moreover, previous work on data-plane programming provides little to no built-in support for addressing this difficulty. We propose a new approach: a flexible intermediate representation (IR) called TAPIR that natively supports stateful data plane functionality, as well as a compiler to generate device-specific code such as P4 from TAPIR code. Using a sequence of IR-to-IR translation stages, we show how to leverage TAPIR to build a compiler for a new declarative network programming abstraction Callback State Machines (CSMs), allowing operators to write data-plane programs against global state. In CSMs, programmers do not specify how the global state is updated on individual switches, which greatly simplifies the development process. Our key insight is that this simplification can be done without taking away the (crucial) ability to write programs with asynchronous control flow: CSMs have a callback mechanism for specifying how networks react to events such as congestion or an attempted intrusion. Additionally, we demonstrate the power of TAPIR by using it to build a working implementation of the CONGA adaptive congestion control system.

• Location: Virtual
• Date: September 2021

“ELIΧR: Eliminating Computation Redundancy in CNN-Based Video Processing”

Jordan Schmerge, Daniel Mawhirter, Connor Holmes, Jedidiah McClurg, Bo Wu

(RSDHA@SC 2021)

Video processing frequently relies on applying convolutional neural networks (CNNs) for various tasks, including object tracking, real-time action classification, and image recognition. Due to complicated network design, processing even a single frame requires many operations, leading to low throughput and high latency. This process can be parallelized, but since consecutive images have similar content, most of these operations produce identical results, leading to inefficient usage of parallel hardware accelerators. In this paper, we present ELIXR, a software system that systematically addresses this computation redundancy problem in an architecture-independent way, using two key techniques. First, ELIXR implements a lightweight change propagation algorithm to automatically determine which data to recompute for each new frame based on changes in the input. Second, ELIXR implements a dynamic check to further reduce needed computations by leveraging special operators in the model (e.g., ReLU), and trading off accuracy for performance. We evaluate ELIXR on two real-world models, Inception V3 and Resnet-50, and two video streams. We show that ELIXR running on the CPU produces up to 3.49X speedup (1.76X on average) compared with frame sampling, given the same accuracy and real-time processing requirements, and we describe how our approach can be applied in an architecture-independent way to improve CNN performance in heterogeneous systems.

• Location: Virtual
• Date: November 2021

“Dryadic: Flexible and Fast Graph Pattern Matching at Scale”

Daniel Mawhirter, Samuel Reinehr, Wei Han, Noah Fields, Miles Claver, Connor Holmes, Jedidiah McClurg, Tongping Liu, Bo Wu

(PACT 2021)

Graph pattern matching searches a data graph for all instances of one or more query patterns. Since it is one of the most fundamental problems in graph analytics, many graph pattern matching systems have been proposed with distinct features to provide a mix of flexibility and performance. It is generally accepted that distinct use cases may necessitate the use of different systems. In this paper, we propose Dryadic, a system which integrates comprehensive flexibility features, yet can still outperform five state-of-the-art graph pattern matching systems on the use cases they optimize for. Unlike existing systems that employ a case-by-case design strategy, all functionalities of Dryadic are centered around a powerful intermediate representation, the computation tree structure, which encodes the matching algorithms for arbitrary patterns. Dryadic implements novel techniques to optimize the computation tree and maps it to different backends to perform compiled, interpreted, or distributed graph pattern matching. Extensive experiments on nine real-world graphs of different scales show that Dryadic, despite its all-in-one nature, is often one to three orders of magnitude faster than other systems in three common usage scenarios.

• Location: Virtual
• Date: September 2021

“Synchronization Synthesis for Network Programs”

Jedidiah McClurg, Hossein Hojjat, Pavol Cerny

(CAV 2017)

In software-defined networking (SDN), a controller program updates the forwarding rules installed on network packet-processing devices in response to events. Such programs are often physically distributed, running on several nodes of the network, and this distributed setting makes programming and debugging especially difficult. Furthermore, bugs in these programs can lead to serious problems such as packet loss and security violations. In this paper, we propose a program synthesis approach that makes it easier to write distributed controller programs. The programmer can specify each sequential process, and add a declarative specification of paths that packets are allowed to take. The synthesizer then inserts enough synchronization among the distributed controller processes such that the declarative specification will be satisfied by all packets traversing the network. Our key technical contribution is a counterexample-guided synthesis algorithm that furnishes network controller processes with the synchronization constructs required to prevent any races causing specification violations. Our programming model is based on Petri nets, and generalizes several models from the networking literature. Importantly, our programs can be implemented in a way that prevents races between updates to individual switches and in-flight packets. To our knowledge, this is the first counterexample-guided technique that automatically adds synchronization constructs to Petri-net-based programs. We demonstrate that our prototype implementation can fix realistic concurrency bugs described previously in the literature, and that our tool can readily scale to network topologies with 1000+ nodes.

• Location: Heidelberg, Germany
• Date: July 2017

“Optimizing Horn Solvers for Network Repair”

Hossein Hojjat, Philipp Ruemmer, Jedidiah McClurg, Pavol Cerny, Nate Foster

(FMCAD 2016)

Automatic program repair modifies a faulty program to make it correct with respect to a specification. Previous approaches have typically been restricted to specific programming languages and a fixed set of syntactical mutation techniques -- e.g., changing the conditions of if statements. We present a more general technique based on repairing sets of unsolvable Horn clauses. Working with Horn clauses enables repairing programs from many different source languages, but also introduces challenges, such as navigating the large space of possible repairs. We propose a conservative semantic repair technique that only removes incorrect behaviors and does not introduce new behaviors. Our proposed framework allows the user to request the best repairs -- it constructs an optimization lattice representing the space of possible repairs, and uses a novel local search technique that exploits heuristics to avoid searching through sub-lattices with no feasible repairs. To illustrate the applicability of our approach, we apply it to problems in software-defined networking (SDN), and illustrate how it is able to help network operators fix buggy configurations by properly filtering undesired traffic. We show that interval and Boolean lattices are effective choices of optimization lattices in this domain, and we enable optimization objectives such as modifying the minimal number of switches. We have implemented a prototype repair tool, and present preliminary experimental results on several benchmarks using real topologies and realistic repair scenarios in data centers and congested networks.

• Location: Mountain View, CA, USA
• Date: October 2016

“Optimal Consistent Network Updates in Polynomial Time”

Pavol Cerny, Nate Foster, Nilesh Jagnik, Jedidiah McClurg

(DISC 2016)

Software-defined networking (SDN) enables controlling the behavior of a network in software, by managing the the forwarding rules installed on switches. However, it can be difficult to ensure that certain properties are preserved during periods of reconfiguration. The widely-accepted notion of per-packet consistency requires every packet to be forwarded using the new configuration or the old configuration, but not a mixture of the two. A (partial) order on switches is a consistent order update if updating the switches in that order guarantees per-packet consistency. A consistent order update is optimal if it allows maximal parallelism, where switches may be updated in parallel if they are incomparable in the order. This paper presents a polynomial-time algorithm for computing optimal consistent order updates. This contrasts with other recent results, which show that for other properties (e.g., loop-freedom and waypoint enforcement), the optimal update problem is NP-complete.

• Location: Paris, France
• Date: September 2016

“Event-Driven Network Programming”

Jedidiah McClurg, Hossein Hojjat, Nate Foster, Pavol Cerny

(PLDI 2016)

Software-defined networking (SDN) programs must simultaneously describe static forwarding behavior and dynamic updates in response to events. Event-driven updates are critical to get right, but difficult to implement correctly due to the high degree of concurrency in networks. Existing SDN platforms offer weak guarantees that can break application invariants, leading to problems such as dropped packets, degraded performance, security violations, etc. This paper introduces EVENT-DRIVEN CONSISTENT UPDATES that are guaranteed to preserve well-defined behaviors when transitioning between configurations in response to events. We propose NETWORK EVENT STRUCTURES (NESs) to model constraints on updates, such as which events can be enabled simultaneously and causal dependencies between events. We define an extension of the NetKAT language with mutable state, give semantics to stateful programs using NESs, and discuss provably-correct strategies for implementing NESs in SDNs. Finally, we evaluate our approach empirically, demonstrating that it gives well-defined consistency guarantees while avoiding expensive synchronization and packet buffering.

• Location: Santa Barbara, CA, USA
• Date: June 2016

“Implementing Real-time Collaboration in TouchDevelop using AST Merges”

Jonathan Protzenko, Sebastian Burckhardt, Michal Moskal, Jedidiah McClurg

(MobileDeLi@SPLASH 2015)

Collaborating on a piece of code is notoriously difficult when the number of people involved goes above 1. In particular, every computer programmer dreads the "merge conflict", a brutal, unforgiving experience, where they must reconcile their changes with someone else's. If offline collaboration is already so painful, real-time collaboration seems even less of an option. It turns out, though, that by reasoning on changes at the level of the program AST, rather than the program text, we can devise a new conflict-free merge algorithm. The algorithm is particularly well-suited to real-time collaboration - we implemented it in the TouchDevelop web programming environment and dub the algorithm diffTree.

• Location: Pittsburgh, Pennsylvania
• Date: October 2015

“Uranine: Real-time Privacy Leakage Monitoring without System Modification for Android”

Vaibhav Rastogi, Zhengyang Qu, Jedidiah McClurg, Yinzhi Cao, Yan Chen

(SecureComm 2015)

Mobile devices are becoming increasingly popular. One reason for their popularity is the availability of a wide range of third-party applications, which enrich the environment and increase usability. There are however privacy concerns centered around these applications – users do not know what private data is leaked by the applications. Previous works to detect privacy leakages are either not accurate enough or require operating system changes, which may not be possible due to users’ lack of skills or locked devices. We present Uranine (Uranine is a dye, which finds applications as a flow tracer in medicine and environmental studies.), a system that instruments Android applications to detect privacy leakages in real-time. Uranine does not require any platform modification nor does it need the application source code. We designed several mechanisms to overcome the challenges of tracking information flow across framework code, handling callback functions, and expressing all information-flow tracking at the bytecode level. Our evaluation of Uranine shows that it is accurate at detecting privacy leaks and has acceptable performance overhead.

• Location: Dallas, TX, USA
• Date: October 2015

“Efficient Synthesis of Network Updates”

Jedidiah McClurg, Hossein Hojjat, Pavol Cerny, Nate Foster

(PLDI 2015)

Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes.

• Location: Portland, OR, USA
• Date: June 2015

“Network Updates for the Impatient: Eliminating Unneccessary Waits”

Hossein Hojjat, Jedidiah McClurg, Pavol Cerny, Nate Foster

(PLVNET@POPL 2015)

• Location: Mumbai, India
• Date: January 2015

“Development of a Translator from LLVM to ACL2”

David Hardin, Jennifer Davis, David Greve, Jedidiah McClurg

(ACL2@VSL 2014)

In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystems whose top-level assurance relies on the assurance of the individual components. We have thus undertaken a project to build a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover. Our translator produces executable ACL2 formal models, allowing us to both prove theorems about the translated models as well as validate those models by testing. The resulting models can be translated and certified without user intervention, even for code with loops, thanks to the use of the def::ung macro which allows us to defer the question of termination. Initial measurements of concrete execution for translated LLVM functions indicate that performance is nearly 2.4 million LLVM instructions per second on a typical laptop computer. In this paper we overview the translation process and illustrate the translator’s capabilities by way of a concrete example, including both a functional correctness theorem as well as a validation test for that example.

• Location: Vienna, Austria
• Date: July 2014

“Creating Formally Verified Components for Layered Assurance with an LLVM to ACL2 Translator”

David Hardin, Jedidiah McClurg, Jennifer Davis

(LAW@ACSAC 2013)

In our current work, we need to create a library of formally verified software component models from code that has been compiled (or decompiled) using the Low-Level Virtual Machine (LLVM) intermediate form; these components, in turn, are to be assembled into subsystems whose top-level assurance relies on the assurance of the individual components. Thus, we have undertaken a project to build a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover. Our translator produces executable ACL2 specifications featuring tail recursion, as well as in-place updates via ACL2’s single-threaded object (stobj) mechanism. This allows us to efficiently support validation of our models by executing production tests for the original artifacts against those models. Unfortunately, features that make a formal model executable are often at odds with efficient reasoning. Thus, we also present a technique for reasoning about tail-recursive ACL2 functions that execute in-place, utilizing a formally proven "bridge" to primitive-recursive versions of those functions operating on lists.

• Location: New Orleans, Louisiana
• Date: December 2013

“Collaborative Reactive Behavior in Heterogeneous Wireless Sensor Networks”

Jedidiah McClurg, Goce Trajcevski, Jesse Yanutola

(SenSys 2012 (Poster))

Wireless Sensor Networks (WSN) which contain heterogeneous nodes and monitor multiple phenomena present a unique set of challenges in regards to efficient management of reactive behavior. The ECA (on Event if Condition then Action) paradigm from Active Databases offers a solution via event-based synchronization which provides reduced energy consumption compared to continuous monitoring. In our demo, we show how to utilize this approach via compilation of system-level ECA triggers to mote-specific trigger code. We also demonstrate the practicality of the approach by constructing a heterogeneous WSN of TelosB/SunSPOT motes and using our tools to implement reactive behaviors based on temperature/luminance data.

• Location: Toronto, Ontario, Canada
• Date: November 2012