The MadSystems Seminar aims to connect faculties and students interested in computer systems research.
We are interested in all aspects of computer systems, including Distributed and Cloud computing, Operating Systems, File and Storage systems, Formal methods (e.g. modeling, verification), Networked Systems and Machine Learning Systems.
The seminar takes two formats:
Time: Tuesday 4-5 pm Location: Room 4310, CS building (or hybrid for remote invited talks) Calendar: Google Calendar
Invited Talk: Flexible Privacy via Disguising and Revealing (Lily Tsai)
Time: 4-5 pm, Nov 5th, 2024 Location: CS 3310
Abstract: Many users today have tens to hundreds of accounts with web services that store sensitive data, from social media to tax preparation and e-commerce sites. While users have the right to delete their data (via e.g., the GDPR or CCPA), users want and deserve more nuanced controls over their data that don't exist today. For example, a user might wish to hide and protect data of an e-commerce or dating app profile when inactive, but also want their data to be present should they return to use the application. Today, however, services often provide only coarse-grained, blunt tools that result in all-or-nothing exposure of users' private information.
This thesis introduces the notion of disguised data, a reversible state of data in which sensitive data is selectively hidden. To demonstrate the feasibility of disguised data, this thesis also presents Edna—the first system for disguised data—which helps database-backed web applications allow users to remove their data without permanently losing their accounts, anonymize their old data, and selectively dissociate personal data from public profiles. Edna helps developers support these features while maintaining application functionality and referential integrity in the database via disguising and revealing transformations. Disguising selectively renders user data inaccessible via encryption, and revealing enables the user to restore their data to the application. Edna's techniques allow transformations to compose in any order, e.g., deleting a previously anonymized user's account, or restoring an account back to an anonymized state.
With Edna, web applications can enable flexible privacy features with reasonable developer effort and moderate performance impact on application operation throughput. In the Lobsters social media application—a 160k LoC web application with >16k users—adding Edna and its features takes less than 1k LoC, and decreases throughput 1-7% in the common case and up to 28% in the worst case (when the user owning 1% of all application data continuously disguises and reveals their account).
Bio: Lily Tsai currently works as part of SystemsResearch@Google (SRG), researching systematic ways to achieve better data privacy and security in data warehouses, ML frameworks, and more. She just graduated with her PhD at MIT in the PDOS group in 2024, where her research with Malte Schwarzkopf and Frans Kaashoek aimed to design systems for better data protections and security in web applications. Besides research, Lily loves to play violin, read sci-fi, hike, climb, and explore the world around her.
We primarily use UW-Madison Systems Group Slack for communication, and in particular the #seminar channel. To join Systems Group Slack, click this invitation link.
#seminar
Meanwhile, we will also use a mailing list to broadcast announcements (e.g., each week's talk topic): sys-seminar@cs.wisc.edu. You can join the email list here.
sys-seminar@cs.wisc.edu
Thanks to our generous sponsors, we will have refreshments for the weekly meeting this semester!
Date: Oct 29, 2024
Sujay Yadalam will lead the discussion on cloud platforms and workloads. The discussion will focus on this recent paper from Microsoft: Workload Intelligence: Punching Holes Through the Cloud Abstraction
He will also briefly talk about resource harvesting:
Date: Oct 22nd, 2024
Abstract: Cluster managers, such as Kubernetes, are among the most critical systems in modern clouds. Modern cluster managers are architected as a fleet of controllers that manage all the applications, services, and resources in the cloud, thus making controller correctness paramount. We have developed several testing techniques (including Acto for functional testing and Sieve for fault-tolerance testing) for cluster management controllers in the past few years. Besides many serious controller bugs we discovered through testing, we learned valuable lessons that controller bugs have diverse causes such as concurrency, asynchrony, and failures, and often lead to liveness violations. Formal verification is promising for avoiding bugs in system software, but most work so far focused on safety, instead of liveness.
In this talk, I will present Anvil, our effort for building provably correct cluster managers. Anvil is a framework for developing practical controller implementations and verifying that the controllers correctly implement liveness and safety properties. One key challenge is to develop a formal specification that precludes a broad range of controller bugs and is generally applicable to diverse controllers. I will present how we address this challenge with Eventually Stable Reconciliation, a general and powerful specification written as a concise temporal logic liveness property. I will also present how to use Anvil to verify three Kubernetes controllers for managing ZooKeeper, RabbitMQ, and FluentBit, which can readily be deployed in Kubernetes platforms and achieve feature parity and the same performance compared to widely used unverified controllers. The proof effort is reasonable compared to previous work due to Anvil's rich features for assisting temporal reasoning. Lastly, I will talk about our ongoing work on extending Anvil to verify cross-controller interactions compositionally and reducing the trusted computing base by verifying Kubernetes core controllers using Anvil.
Bio: Xudong Sun is a final year CS PhD student at the University of Illinois Urbana-Champaign, advised by Prof. Tianyin Xu. Xudong's research focuses on improving system reliability using formal verification, systematic testing, fault injection, and model checking. Xudong's research was recognized with the Jay Lepreau Best Paper Award at OSDI'2024, Mavis Future Faculty Fellowship, and Yunni and Maxine Pao Memorial Fellowship. Xudong is on the job market looking for research positions in academia and industry in the 2024 - 2025 cycle.
Date: Oct 15, 2024
Prof. Tej Chajed will give a discussion/tutorial on systems verification. Reading list:
Date: Oct 8, 2024
Abstract: Serverless computing enables scalable, cost-efficient, and simple to program applications by allowing users to develop their workloads as compositions of lightweight functions, while the cloud provider manages the underlying infrastructure. However, serverless workloads differ significantly from traditional cloud applications—they are short-lived, have smaller data and instruction footprints, experience bursty request arrival patterns, involve high I/O activity, and undergo frequent context switches. These characteristics result in performance, energy, and resource inefficiencies when run on conventional server-class processors.
To address these challenges, I introduce μManycore (ISCA '23), a processor architecture optimized for serverless environments. Unlike traditional processors, μManycore focuses on minimizing tail latency, the key performance metric in cloud environments. It achieves this goal by removing the main contention points in the system. First, instead of having a chip-wide cache coherence, μManycore organizes its cores into small cache-coherent villages. Then, it connects the villages via a leaf-spine network topology that provides low-latency, redundant paths between clusters of villages. Finally, μManycore is augmented with a hardware support for request scheduling and context switching.
Building on μManycore, I propose Mosaic (MICRO '24), a core micro-architecture optimized for serverless workloads. Mosaic slices micro-architectural structures, such as caches and branch predictors, into small chunks and assigns tiles of such chunks to functions. The processor retains the state of functions in their tiles across context switches, thereby improving performance. Furthermore, currently inactive tiles are set to a low power mode, thereby reducing energy consumption. Together, μManycore and Mosaic deliver significant improvements in tail latency, throughput, and power efficiency for serverless environments.
Date: Oct 1st, 2024
Anjali will lead the topic discussion on serverless computing. Reading list:
Date: Sept 24th, 2024
Abstract: Cloud providers seek to deploy CXL-based memory to increase aggregate memory capacity, reduce costs, and lower carbon emissions. However, CXL accesses incur higher latency than local DRAM. Existing systems use software to manage data placement across memory tiers at page granularity. Cloud providers are reluctant to deploy software-based tiering due to high overheads in virtualized environments. Hardware-based memory tiering could place data at cacheline granularity, mitigating these drawbacks. However, hardware is oblivious to application-level performance.
We propose combining hardware-managed tiering with software-managed performance isolation to overcome the pitfalls of either approach. We introduce Intel Flat Memory Mode, the first hardware-managed tiering system for CXL. Our evaluation on a full-system prototype demonstrates that it provides performance close to regular DRAM, with no more than 5% degradation for more than 82% of workloads. Despite such small slowdowns, we identify two challenges that can still degrade performance by up to 34% for “outlier” workloads: (1) memory contention across tenants, and (2) intra-tenant contention due to conflicting access patterns.
To address these challenges, we introduce Memstrata, a lightweight multi-tenant memory allocator. Memstrata employs page coloring to eliminate inter-VM contention. It improves performance for VMs with access patterns that are sensitive to hardware tiering by allocating them more local DRAM using an online slowdown estimator. In multi-VM experiments on prototype hardware, Memstrata is able to identify performance outliers and reduce their degradation from above 30% to below 6%, providing consistent performance across a wide range of workloads.
