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.

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.

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 (SoC) embed a diverse range of accelerators with unique power and performance characteristics. The execution flow of the critical workloads can be adjusted to span into multiple accelerators so that the trade-off between performance and energy fits to the dynamically changing physical factors.

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, and 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 four state-of-the-art graph pattern matching systems on the primary use cases they target. 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.

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.

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.

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.

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.