Search for: All records

We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used an explicit source of randomness to reason about higher-order probabilistic programs. 

In many networking scenarios, long-lived flows can be rerouted to free up resources and accommodate new flows, but doing so comes at a cost in terms of disruption. An archetypical example is the transmission of live streams in a content delivery network: audio and video encoders (clients) generate live streams and connect to a server which rebroadcasts their stream to the rest of the network. Reconnecting a client to a different server mid-stream is very disruptive. We abstract these scenarios in the setting of a capacitated network where clients arrive one by one and request to send a unit of flow to a designated set of servers subject to edge/vertex capacity constraints. An online algorithm maintains a sequence of flows that route the clients present so far to the set of servers. The cost of a sequence of flows is defined as the net switching cost, i.e. total length of all augmenting paths used to transform each flow into its successor. We prove that for unit-vertex-capacitated networks, the algorithm that successively updates the flow using the shortest augmenting path from the new client to a free server incurs a total switching cost of O(n log2 n), where n is the number of vertices in the network. This result is obtained by reducing to the online bipartite matching problem studied in prior work and applying their result. Finally, we identify a slightly more general class of networks for which essentially the same reduction idea can be applied to get the same bound. 

This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT's scalability using real-world topologies, compare its performance against state-of-the-art tools, and develop an extended case study on a recently proposed data center network design.