In the context of data center computing, the carbon emission incurred during the manufacturing of solid-state drives (SSDs), called embodied carbon, is increasingly overtaking the emissions caused by powering these drives throughout their operational lifetime. Out of an abundance of caution, current SSDs are designed to fail long before the internal flash components are completely unusable. Although this choice may be appropriate for single-disk systems, distributed storage systems can already tolerate individual SSD failures through redundancy. We propose Salamander, a new design for SSD servers where SSDs expose multiple logical minidisks, which match the granularity of hardware failures, so that: (1) as minidisks fail, distributed storage systems can continue using the remaining good capacity; and (2) SSDs may recycle portions of failed minidisks that still have some usable life. Salamander increases the lifespan of SSDs, and therefore amortizes embodied carbon, by incrementally exposing hardware deterioration to the system and leveraging existing, end-to-end redundancy mechanisms to recover from this deterioration.
Granular resource heterogeneity refers to the phenomenon in which small computational units within or across applications exhibit distinct resource usage patterns. Traditional resource management in shared clusters lumps monolithic applications into coarse categories, overlooking smaller execution phases that differ in resource demands. We introduce hiresperf, an extensible profiler that investigates resource usage at 10-microsecond intervals attributed to each function invocation, with a low overhead. We show that using hiresperf for either offline analysis or real-time monitoring can exhibit the granular resource heterogeneity without manually decomposing applications for profiling. Armed with the fine-grained insights, resource managers, batch schedulers, and serverless runtimes can proactively schedule and migrate tasks to minimize interference and boost utilization at the same time.
Large language models (LLMs) have demonstrated remarkable coding capabilities. They excel in code synthesis benchmarks across diverse domains and have become ubiquitous in coding tools. Recently, they have also shown promise in generating mathematical proofs and small software programs. In this paper, we explore their potential to produce proofs for complex system software (e.g., file systems), where verification typically requires substantial manual effort. By automating parts of this process, LLMs could reduce the verification burden and make rigorous proofs for system software more accessible. To evaluate LLMs for system software verification, we use FSCQ, a verified file system, as our benchmark. Our results confirm the promise of this approach: with appropriate proof context and a straightforward best-first tree search, off-the-shelf LLMs achieve 38% proof coverage for theorems sampled from FSCQ. Moreover, for simpler theorems-those with human proofs under 64 tokens, which make up about 60% of all FSCQ theorems-LLMs achieve over 57% coverage. These findings are preliminary, and we anticipate that various techniques can further improve proof coverage.
Current memory tiering systems mitigate asymmetric latency through page migration between tiers. While this approach effectively hides latency, it overlooks scenarios where latency could potentially be tolerated. We propose that an efficient system should integrate both latency reduction (migration) and latency tolerance strategies. Our research demonstrates the effectiveness of prefetchers in tolerating latency within such systems, highlighting their importance in the design of high-performance memory tiering solutions.
The rapid expansion of cloud computing, especially machine learning, is leading to a significant increase in the global energy footprint of computing. Improvements in the energy efficiency of hardware and infrastructure are nearing the point of diminishing returns, and system developers will soon be compelled to drastically improve the energy efficiency of their software. For that, it is essential to have energy clarity: developers/operators must be able to accurately and productively understand how the energy usage of their hardware and software is influenced by workload, configuration, and other factors. We propose energy interfaces as a way to achieve that clarity: an energy interface provides concise, accurate, actionable information about the "energy behavior" of a system, much like a functional interface does for its semantic behavior. Preliminary experimentation suggests that obtaining and using such energy interfaces is feasible. We believe that some form of energy interfaces will one day become as central to system building as functional interfaces.
