SSS Abstracts  Fall 2014

Presented by Arbob Ahmad, CSD

Noninterference (NI) defines a program to be secure if changes to high-security inputs cannot alter low-security outputs. NI indirectly states the epistemic property that the low-security outputs do not include knowledge obtained from the high-security inputs. However, NI is too restrictive a property to incorporate declassification of some high-security inputs and not others. By reasoning about declassification in epistemic logic, we express what knowledge is obtained through the execution of a program by the declassifications. Therefore, as a consequence of the adequacy of the epistemic logic for modeling the program behavior, we can still derive some NI-like properties for those high inputs that have not been declassified. Moreover, the epistemic logic we choose can also express authorization policies for when a declassification may occur. When knowledge reasoning is combined with authorization in a single logic, we can derive properties of knowledge flows such as the lemma that the derivation that knowledge is declassified must include the proof that the declassification is authorized. In this talk, I will present our formulation of declassification and authorization and outline how we prove interesting epistemic properties of programs that go beyond NI.

Joint work with Robert Harper

In partial fulfillment of the Speaking Requirement

Forward-Chaining Linear Logic Programming for Parallel Programming Over Graph Structures

Monday, October 27^th, 2014 from 12-1 pm in GHC 7101.

Presented by Flavio Cruz, CSD

Forward-chaining logic programming has been popularized by the Datalog language and has been extensively used in the field of deductive databases. Given that Datalog is based on first order logic, logical facts are persistent since derivation rules do not model fact retraction.

We propose LM (Linear Meld), a new forward-chaining logic programming language that integrates both linear and classical logic and allows logical facts to be asserted and retracted declaratively. In addition, LM is naturally concurrent since facts are partitioned across the nodes of a graph, enabling concurrent rule derivation throughout the program. In a nutshell, LM allows us to write concise algorithms over graph structures that can be compiled and executed on parallel architectures without any modifications.

We present the LM language through a number of examples. We first show how to implement basic graph algorithms and then more complex programs such as the Mini-Max algorithm and a novel way to solve the N-Queens problem.

Finally, we briefly show how to prove the correctness of a few programs.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Formal Verification of Distributed Aircraft Controllers

Tuesday, November 4^th, 2014 from 12-1 pm in GHC 6501.

Presented by Sarah Loos, CSD

Formal verification and theorem proving have been used successfully in many discrete applications, such as chip design and verification. However, computation is not confined to the discrete world of desktop computing. Increasingly, we depend on discrete software to control safety-critical components of continuous physical systems (for example, adaptive cruise control in cars and collision avoidance in aircraft). It is vital that these hybrid (discrete and continuous) systems behave as designed, or they will cause more damage than they intend to fix. In this talk, I will present several challenges associated with verifying hybrid systems and how we can use differential dynamic logic and its proof calculus to ensure safety for hybrid systems under a continuously infinite range of circumstances.

In addition to covering the theoretical foundations for deductive verification of hybrid systems, I will discuss some of the practical uses of our verification tools:KeYmaera and KeYmaeraD. These tools have been used to verify a class of distributed collision avoidance controllers designed to work in environments with arbitrarily many aircraft. We prove that the controllers never allow the aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver that the new plane may not be aware of. Because these safety guarantees always hold, the aircraft are protected against unexpected emergent behavior, which simulation and testing may miss.

This is joint work with André Platzer and David Renshaw.

In Partial Fulfillment of the Speaking Requirement.

vTube: Efficient Streaming of Virtual Appliances over Wide Area Networks

Friday, November 7^th, 2014 from 12-1 pm in GHC 4303.

Presented by Yoshihisa Abe, CSD

Formal verification and theorem proving have been used successfully in many discrete applications, such as chip design and verification. However, computation is not confined to the discrete world of desktop computing. Increasingly, we depend on discrete software to control safety-critical components of continuous physical systems (for example, adaptive cruise control in cars and collision avoidance in aircraft). It is vital that these hybrid (discrete and continuous) systems behave as designed, or they will cause more damage than they intend to fix. In this talk, I will present several challenges associated with verifying hybrid systems and how we can use differential dynamic logic and its proof calculus to ensure safety for hybrid systems under a continuously infinite range of circumstances.

In addition to covering the theoretical foundations for deductive verification of hybrid systems, I will discuss some of the practical uses of our verification tools:KeYmaera and KeYmaeraD. These tools have been used to verify a class of distributed collision avoidance controllers designed to work in environments with arbitrarily many aircraft. We prove that the controllers never allow the aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver that the new plane may not be aware of. Because these safety guarantees always hold, the aircraft are protected against unexpected emergent behavior, which simulation and testing may miss.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Adaptive Sampling with Matrices

Tuesday, November 11^th, 2014 from 12-1 pm in GHC 6501.

Presented by Akshay Krishnamurthy, CSD

I will present two adaptive sampling algorithms for the matrix completion and matrix approximation problems. For the matrix completion problem (exact recovery of a low rank matrix), the algorithm enjoys a near-optimal sample complexity that outperforms all existing algorithms. This algorithm also succeeds on matrices with highly coherent row-spaces, where all passive algorithms provably fail. Finally it is simple to implement, runs in nearly linear time and has minimal space requirements. For the matrix approximation problem, I will describe an algorithm that computes an approximation that is nearly as good as the best rank-r approximation to the input matrix, using only a few samples. As before, this algorithm does not require incoherence assumptions on the row-space of the matrix, and thus operates in more general settings than other algorithms. Again this algorithm enjoys strong statistical and computational properties.

In Partial Fulfillment of the Speaking Requirement.

PriorityMeister: Tail Latency QoS for Shared Networked Storage

Friday, November 14^th, 2014 from 12-1 pm in GHC 4303.

Presented by Timothy Zhu, CSD

Meeting service level objectives (SLOs) for tail latency is an important and challenging open problem in cloud computing infrastructures. The challenges are exacerbated by burstiness in the workloads. This talk describes PriorityMeister - a system that employs a combination of per-workload priorities and rate limits to provide tail latency QoS for shared networked storage, even with bursty workloads. PriorityMeister automatically and proactively configures workload priorities and rate limits across multiple stages (e.g., a shared storage stage followed by a shared network stage) to meet end-to-end tail latency SLOs. In real system experiments and under production trace workloads, PriorityMeister outperforms most recent reactive request scheduling approaches, with more workloads satisfying latency SLOs at higher latency percentiles. PriorityMeister is also robust to mis-estimation of underlying storage device performance and contains the effect of misbehaving workloads.

Joint work with Alexey Tumanov, Michael A. Kozuch, Mor Harchol-Balter, Gregory R. Ganger

In Partial Fulfillment of the Speaking Requirement

ShardFS: Sharded Files with Replicated Directories

Friday, November 21^st, 2014 from 12-1 pm in GHC 4303.

Presented by Lin Xiao, CSD

The rapid growth of cloud storage systems calls for fast and scalable namespace processing.We propose a new scalable file system metadata service design named ShardFS, and compare it with two existing scalable solutions, IndexFS and Giraffa. Both IndexFS and Giraffa use table-based metadata representations, each with a different namespace partitioning scheme. ShardFS also partitions directory entries but instead fully replicates directory tree structure information on all metadata servers. This allows ShardFS to provide fast concurrent access to file metadata and individual directory entries, at the cost of more replication overhead for strew structure changes. The three systems are systematically evaluated on a 128-node cluster using a set of micro-benchmarks and several metadata traces extracted from real-world large-scale HDFS clusters.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Extending the Graphics Pipeline with Adaptive, Multi-rate Shading

Monday, November 24^th, 2014 from 12-1 pm in GHC 6501.

Presented by Yong He, CSD

Due to complex shaders and high-resolution displays (particularly on mobile graphics platforms), fragment shading often dominates the cost of rendering in games. To improve the efficiency of shading on GPUs, we extend the graphics pipeline to natively support techniques that adaptively sample components of the shading function more sparsely than per-pixel rates. We perform an extensive study of the challenges of integrating adaptive, multi-rate shading into the graphics pipeline, and evaluate two- and three-rate implementations that we believe are practical evolutions of modern GPU designs. We design new shading language abstractions that simplify development of shaders for this system, and design adaptive techniques that use these mechanisms to reduce the number of instructions performed during shading by more than a factor of three while maintaining high image quality.

Joint work with Yan Gu and Kayvon Fatahalian

In Partial Fulfillment of the Speaking Requirement

Logic Programming for Social Networking Sites

Tuesday, December 2^nd, 2014 from 12-1 pm in GHC 6501.

Presented by Kuen-Bang Hou (Favonia), CSD

Logic programming makes it possible to execute or experiment specifications directly without having programmers implement them. However, while modeling social networking sites, I realized that several common concepts, like global counters, were still not conveniently expressible in a typical logic programming language. To address this issue, I created a new logic programming language with extensions to handle information dependency, name generation and list comprehension. Moreover, these extensions are general in the sense that they are not limited to the case of social networking sites. Finally, I showed that there is a sound and complete compilation from the new language to a known linear logic programming language. This talk will focus on the definition of the new language and the usage of it.

MICA: A Holistic Approach to Fast In-Memory Key-Value Storage

Friday, December 5^th, 2014 from 12-1 pm in GHC 4303.

Presented by Hyeontaek Lim, CSD

MICA is a scalable in-memory key-value store that handles 65.6 to 76.9 million key-value operations per second using a single general-purpose multi-core system. MICA is over 4--13.5x faster than current state-of-the-art systems, while providing consistently high throughput over a variety of mixed read and write workloads.

MICA takes a holistic approach that encompasses all aspects of request handling, including parallel data access, network request handling, and data structure design, but makes unconventional choices in each of the three domains. First, MICA optimizes for multi-core architectures by enabling parallel access to partitioned data. Second, for efficient parallel data access, MICA maps client requests directly to specific CPU cores at the server NIC level by using client-supplied information and adopts a light-weight networking stack that bypasses the kernel. Finally, MICA's new data structures---circular logs, lossy concurrent hash indexes, and bulk chaining---handle both read- and write-intensive workloads at low overhead.

Joint work with Dongsu Han, David G. Andersen, and Michael Kaminsky

In Partial Fulfillment of the Speaking Requirement

Utilizing Real World Knowledge for Fine Grained Estimation Tasks

Monday, December 8^th, 2014 from 12-1 pm in GHC 7101.

Presented by Yair Movshovitz-Attias, CSD

Computer Vision has seen great advances recently in a number of complex tasks such as object detection, fine grained classification, and image segmentation. A key ingredient in such success stories was the use of large amounts of labeled data. In many cases, the limiting factor becomes the ability to create high quality, labeled, training sets. In this talk I will describe two recent projects in which we were able to achieve state of the art performance by "grounding" images to real world concepts which automated the labeling task. For the task of object viewpoint estimation, we show how 3D CAD models can be used to generate training data with precise labels, and describe a discriminatively reduced ensemble of correlation filters, which optimally utilizes this data. I will also describe our work on storefront classification from Street View imagery in which, by matching images to an ontology of geographical concepts we were able to create a large scale data set with rich labels. Our storefront classification system, which was trained on this data, has human level accuracy.

In Partial Fulfillment of the Speaking Requirement

Event-based Automated Refereeing of a Robot Game

Friday, December 12^th, 2014 from 12-1 pm in GHC 4303.

Presented by Danny Zhu, CSD

Abstract: Most effort in the RoboCup Small Size League (SSL), a worldwide robot soccer league, is focused on creating teams that can play the game autonomously; however, human referees are still essential for actual running of games, since refereeing is not yet handled autonomously. In this talk, I will present an automated referee for the SSL which interprets information from the robots according to the rules of the game and transmits the appropriate commands to the teams. I will describe an initial explicit FSM-based design, as well as a decentralized event-based design, which is currently under development.

In Partial Fulfillment of the Speaking Requirement

Web contact: sss+www@cs